Functions-as-a-Service (FaaS) is a Serverless Cloud paradigm where a platform manages the execution (e.g., scheduling, runtime environments) of stateless functions. Recently, domain-specific languages like APP and aAPP have been developed to express per-function scheduling policies, e.g., enforcing the allocation of functions on nodes that enjoy low data-access latencies thanks to proximity and connection pooling. Reachability analysis of FaaS scheduling policies is fundamental to check quality-of-service properties, like preventing the scheduling of functions on workers which cannot sustain expected performance levels, or verifying security properties, e.g., that safety-critical functions cannot run on nodes with untrusted ones. We investigate the complexity of reachability analysis for APP and aAPP– the latter extends APP with constraints for placing functions according to the absence/presence of other (anti-)affine functions on workers. We show that reachability analysis has linear time complexity in APP, while the addition of affinities (in aAPP) makes reachability PSPACE. Given the computational complexity correspondence between reachability analysis in aAPP and automatic planning problems (both are in PSPACE), we investigate the exploitability of planners, i.e., tools specialised for solving planning problems for the realisation of static analysers of reachability-like problems for aAPP.
This paper presents a case study in the design and formal verification of a safe controller for the generic two-element lumped-capacitance model of temperature regulation, using formal cyber-physical system (CPS) theorem proving. The coupled dynamics and the absence of a fallback state reflect the complexities of real-world control systems and make it a representative challenge for theorem proving. A controller is developed by a design-by-invariant methodology. Verification using the axiomatic theorem prover KeYmaera X revealed critical assumptions for safety and pushes the frontier of CPS theorem proving. The parametric, general and provably safe controller can be applied to a wide range of temperature regulation tasks and is validated by deploying an instance of the verified controller on a physical system, demonstrating its robustness under model inaccuracies and confirming its real-world usability.
Message parsing represents a complex security-critical problem. It has been demonstrated by numerous real-world exploits on parsers, e.g. on PKCS#1 (Public-Key Cryptography Standard) v1.5 signature, X.509 certificate chain, or infamously on a TLS extension during the Heartbleed attack. In this case study, we perform formal verification of a PKCS#1 v1.5 signature parser using Frama-C, where the verification of the parser is realized for the first time directly over the actual implementation in C. This brings highest guarantees of security and functional properties, while leaving developers the flexibility to adapt the code to the project’s specific requirements. We present the proven properties, our verification approach and results. In particular, this work rules out applications of any variants of Bleichenbacher’s signature forgery and ensures that we are able to detect potential parser incompatibilities. This work opens the door to future extensions to other protocols, for example, for parsing DER ASN.1 encoding of X.509 certificates and CRLs (Certificate Revocation Lists).
We present an approach to theory exploration, i.e., a lemma synthesis procedure which discovers algebraic laws over recursive functions over Algebraic Data Types (ADTs). The approach, LemmaCalc, builds on, adapts and extends program calculation techniques known from optimization of functional programs (fusion and accumulator removal). Our approach avoids exponential search space of term enumeration (SyGuS) that can render state-of-the-art techniques prohibitively expensive or even useless on large theories with more than a handful of function symbols. In this paper we describe how this approach can be realized and contribute a robust implementation. The evaluation shows that different methods have complementary strengths and that each can produce lemmas not found by the other, but LemmaCalc scales much better to larger theories.
We introduce the notion of a distributed timed scenario (DTS) and define the semantics of a DTS as a set of distributed behaviours. We define the notion of consistency of a DTS in terms of its semantics and develop a constructive method for determining the consistency. We define the semantic equivalence of two distributed scenarios and develop two different, but related, canonical representations for an equivalence class of distributed scenarios. Equipped with these results we tackle the problem of realisability of sets of sequential scenarios as distributed scenarios. We develop an algorithm that determines whether a set of sequential scenarios can be realised by a DTS, i.e., whether there is a DTS whose semantics is identical to the union of the behaviours allowed by the members of the set. If so, we produce such a DTS.
