ABSTRACT. A fundamental problem in concurrent system design is to identify flexible programming disciplines under which weak memory models provide sequential consistency. For x86-TSO, a suitable reduction theorem for threads that communicate only through shared memory was given by Cohen and Schirmer [ITP2010]. However, this theorem cannot handle programs that edit their own page tables (e.g. memory mangers, hypervisors, and some device drivers). The problem lies in the interaction between a program thread and the hardware MMU that provides its address translation: the MMU cannot be treated as a separate thread (since it implicitly communicates with the program thread), nor as part of the program thread itself (since MMU reads do not snoop the store buffer of the program thread). We generalize the Cohen-Schirmer reduction theorem to handle programs that edit their page tables. The added conditions prevent the MMU of a thread from walking page table entries owned by other threads.

ABSTRACT. The separation kernel concept was developed as an architecture to simplify formal kernel security verification, and is the basis for many implementations of integrated modular avionics in the aerospace domain. This paper reports on a feasibility study conducted for the European Space Agency, to explore the resources required to formally verify the correctness of such a kernel, given a reference specification and a implementation of same. The study was part of an activity called Methods and Tools for On-Board Software Engineering (MTOBSE) which produced a natural language Reference Specification for a Time-Space Partitioning (TSP) kernel, describing partition functional properties such as health monitoring, inter-partition communication, partition control, resource access, and separation security properties, such as the security policy and authorisation control. An abstract security model, and the reference specification were both formalised using Isabelle/HOL. The C sources of the open-source XtratuM kernel were obtained, and a Isabelle/HOL model of the code was semi-automatically produced. Refinement relations were written manually and some proofs were explored. We describe some of the details of what has been modelled and report on the current state of this work. We also make a comparison between our verification explorations, and the circumstances of NICTA's successful verification of the sel4 kernel.

ABSTRACT. Separation algebras are a well-known abstraction to capture common structure of both permissions and memories in programming languages, and form the basis of models of separation logic. As part of the development of a formal version of an operational and axiomatic semantics of the C11 standard, we present a variant of separation algebras that is well suited for C verification.

Our variant of separation algebras has been fully formalized using the Coq proof assistant, together with a library of concrete implementations. These instances are used to build a complex permission model, and a memory model that captures the strict aliasing restrictions of C.

ABSTRACT. I propose verified implementations of several data structures, including random-access lists and ordered maps. They are derived from a common parametric implementation of self-balancing binary trees in the style of Adelson-Velskii and Landis trees. The development of the specifications, implementations and proofs is carried out using the Why3 environment. The originality of this approach is the genericity of the specifications and code combined with a high level of proof automation.

ABSTRACT. Complex systems are hierarchically constructed in layers, and systems are often constructed middle-out rather than top-down; compatibility with existing systems and availability of specific components influences high-level requirements.  This approach leads to an interplay between requirements and design: design choices made at higher levels of abstraction levy requirements on system components at lower levels of abstraction, and design choices restrict the set of possible requirements and acceptable deployment environments.   A consequence is that the designation of a "design choice" or "requirement" depends largely on one’s vantage point within the hierarchy of system components.  To support iterative design, requirements and architectural design should be more closely aligned: requirements models must account for hierarchical system construction, and architectural design notations must better support specification of requirements for system components.

In this presentation, I describe tools supporting iterative development of architecture and verification based on software models.  We represent the hierarchical composition of the system in the Architecture Analysis & Design Language (AADL), and use an extension to the AADL language to describe requirements at different levels of abstraction for compositional verification.  To describe and verify component-level behavior, we use Simulink and Stateflow and multiple analysis tools.

ABSTRACT. For specifying and reasoning about object-based programs it is often attractive for contracts to be expressed using calls to pure methods. It is useful for pure methods to have contracts, including read effects to support local reasoning based on frame conditions. This leads to puzzles such as the use of a pure method in its own contract. These ideas have been explored in connection with verification tools based on axiomatic semantics, guided by the need to avoid logical inconsistency, and focusing on encodings that cater for first order automated provers. This paper adds pure methods and read effects to region logic, a first-order program logic that features frame-based local reasoning and a proof rule for linking of clients with modules to achieve end-to-end correctness by modular reasoning. Soundness is proved with respect to a conventional operational semantics and using the extensional ---i.e., relational---interpretation of read effects. The developments in this paper (a) potentially could guide the implementations of linking as used in modular verifiers and (b) should serve as basis for studying observationally pure methods and encapsulation in the setting of relational region logic.

ABSTRACT. Convex polyhedra provide a relational abstraction of numerical properties for static analysis of programs by abstract interpretation. We describe a lightweight certification of polyhedral abstract domains using the Coq proof assistant. Our approach consists in delegating most computations to an untrusted backend and checking its outputs with a certified frontend. The backend is free to implement relaxations of domain operators (i.e. a subpolyhedral abstract domain) in order to trade some precision for more efficiency, but must produce hints about the soundness of its results. Previously published experimental results show that the certification overhead with a full-precision backend is small and that the resulting certified abstract domain has comparable performance to non-certifying state-of-the-art implementations.

ABSTRACT. The development of sophisticated termination criteria for term rewrite systems has led to powerful, complex tools to automatically obtain (non)termination proofs. While many techniques to establish termination have already been formalized, allowing to certify such proofs, this is not the case for nontermination. In particular, the proof checker CeTA was so far limited to (innermost) loops. In this paper we present an Isabelle/HOL formalization of an extended repertoire of nontermination techniques. Firstly, we formalized techniques for nonlooping nontermination. Secondly, the available strategies include (an extended version of) forbidden patterns, which does in particular cover outermost and context-sensitive rewriting. Finally, a mechanism to support partial nontermination proofs allows to further extend the applicability of our proof checker.

ABSTRACT. In this work we extend the Emerson and Kahlon’s cutoff theorems for process skeletons with conjunctive guards to Parameterized Networks of Timed Automata, i.e. systems obtained by an unbounded number of Timed Automata instantiated from a finite set (U_1 , ..., U_n) of Timed Automata templates. In this way we aim at giving a first tool for universally verifying software systems where an unknown number of software components (i.e. processes) interact with temporal constraints. It is often the case, indeed, that distributed algorithms show an heterogeneous nature, combining dynamic aspects with real-time aspects. In the paper we will also show how to model check a protocol that uses special variables storing identifiers of the participating processes (i.e. PIDs) in Timed Automata with conjunctive guards. This is non-trivial, since solutions to the parameterized verification problem often relies on the processes to be symmetric, i.e. indistinguishable. On the other side, many popular distribute algorithms make use of PIDs and thus cannot directly apply those solutions.

ABSTRACT. We introduce a refinement-based notion of correctness for verification of interrupt driven real-time object code programs, called timed refinements. The notion of timed refinements is targeted at verification of low-level object code against high-level specification models. For timed refinements, both the object code (implementation) and the specification are encoded as timed transition systems. Hence, timed refinements can be construed as a notion of equivalence between two timed transition systems that allows for stuttering between the implementation and specification, and also allows for the use of refinement maps. Stuttering is the phenomenon where multiple but finite transitions of the implementation can match a single transition of the specification. Refinement maps allow low-level implementations to be verified against high-level specification models. We also present a procedure for checking timed refinements. The proposed techniques are demonstrated with the verification of object code programs of six case studies from electric motor control applications.

ABSTRACT. Services running in the cloud face threats from several parties, including malicious clients, administrators, and external attackers. CloudProxy is a recently-proposed framework for secure deployment of cloud applications. In this work, we present the first formal model of CloudProxy, including a formal specification of desired security properties. We model CloudProxy as a transition system in the UCLID modeling language, using term-level abstraction. Our formal specification includes both safety and non-interference properties. We use induction to prove these properties, employing a back-end SMT-based verification engine. Furthermore, we structure our proof as an "assurance case", showing how we decompose the proof into various lemmas, and listing all assumptions and axioms employed. We also perform some limited model validation to gain assurance that the formal model correctly captures all behaviors of the implementation.