Certifying derivation of state machines from coroutines

One of the biggest implementation challenges in security-critical network protocols is nested state machines. In practice today, state machines are either implemented manually at a low level, risking bugs easily missed in audits; or are written using higher-level abstractions like threads, depending on runtime systems that may sacrifice performance or compatibility with the ABIs of important platforms (e.g., resource-constrained IoT systems). We present a compiler-based technique allowing the best of both worlds, coding protocols in a natural high-level form, using freer monads to represent nested coroutines , which are then compiled automatically to lower-level code with explicit state. In fact, our compiler is implemented as a tactic in the Coq proof assistant, structuring compilation as search for an equivalence proof for source and target programs. As such, it is straightforwardly (and soundly) extensible with new hints, for instance regarding new data structures that may be used for efficient lookup of coroutines. As a case study, we implemented a core of TLS sufficient for use with popular Web browsers, and our experiments show that the extracted Haskell code achieves reasonable performance.

Ownership and Immutability in Coq

<p>A significant issue in modern programming languages is unsafe aliasing. Modern type systems have attempted to address this in two prominent ways; immutability and ownership, and often a combination of the two [4][17]. The goal of this thesis is to formalise Immutability and Ownership using the Coq Proof Assistant, a formal proof management system [13]. We encode three type systems using Coq; Featherweight Immutable Java, Featherweight Generic Java and Featherweight Ownership Generic Java, and prove them sound. We describe the challenges presented in encoding immutability, ownership and type systems in general in Coq.</p>

Ownership and Immutability in Coq

<p>A significant issue in modern programming languages is unsafe aliasing. Modern type systems have attempted to address this in two prominent ways; immutability and ownership, and often a combination of the two [4][17]. The goal of this thesis is to formalise Immutability and Ownership using the Coq Proof Assistant, a formal proof management system [13]. We encode three type systems using Coq; Featherweight Immutable Java, Featherweight Generic Java and Featherweight Ownership Generic Java, and prove them sound. We describe the challenges presented in encoding immutability, ownership and type systems in general in Coq.</p>

Verification of MILS Partition Scheduling Module Using Layered Methods

MILS partition scheduling module ensures isolation of data between different domains completely by enforcing secure strategies. Although small in size, it involves complicated data structures and algorithms that make monolithic verification of the scheduling module difficult using traditional verification logic (e.g., separation logic). In this paper, we simplify the verification task by dividing data representation and data operation into different layers and then to link them together by composing a series of abstraction layers. The layered method also supports function calls from higher implementation layers into lower abstraction layers, allowing us to ignore implementation details in the lower implementation layers. Using this methodology, we have verified a realistic MILS partition scheduling module that can schedule operating systems (Ubuntu 14.04, VxWorks 6.8 and RTEMS 11.0) located in different domains. The entire verification has been mechanized in the Coq Proof Assistant.

Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)

Rigorous reasoning about programs calls for some amount of bureaucracy in managing details like variable binding, but, in guiding students through big ideas in semantics, we might hope to minimize the overhead. We describe our experiment introducing a range of such ideas, using the Coq proof assistant, without any explicit representation of variables, instead using a higher-order syntax encoding that we dub "mixed embedding": it is neither the fully explicit syntax of deep embeddings nor the syntax-free programming of shallow embeddings. Marquee examples include different takes on concurrency reasoning, including in the traditions of model checking (partial-order reduction), program logics (concurrent separation logic), and type checking (session types) -- all presented without any side conditions on variables.

Theorems for free from separation logic specifications

Separation logic specifications with abstract predicates intuitively enforce a discipline that constrains when and how calls may be made between a client and a library. Thus a separation logic specification of a library intuitively enforces a protocol on the trace of interactions between a client and the library. We show how to formalize this intuition and demonstrate how to derive "free theorems" about such interaction traces from abstract separation logic specifications. We present several examples of free theorems. In particular, we prove that a so-called logically atomic concurrent separation logic specification of a concurrent module operation implies that the operation is linearizable. All the results presented in this paper have been mechanized and formally proved in the Coq proof assistant using the Iris higher-order concurrent separation logic framework.

The Marriage of Univalence and Parametricity

Reasoning modulo equivalences is natural for everyone, including mathematicians. Unfortunately, in proof assistants based on type theory, which are frequently used to mechanize mathematical results and carry out program verification efforts, equality is appallingly syntactic, and as a result, exploiting equivalences is cumbersome at best. Parametricity and univalence are two major concepts that have been explored in the literature to transport programs and proofs across type equivalences, but they fall short of achieving seamless, automatic transport. This work first clarifies the limitations of these two concepts when considered in isolation and then devises a fruitful marriage between both. The resulting concept, called univalent parametricity , is an extension of parametricity strengthened with univalence that fully realizes programming and proving modulo equivalences. Our approach handles both type and term dependency, as well as type-level computation. In addition to the theory of univalent parametricity, we present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal. For instance, this makes it possible to conveniently switch between an easy-to-reason-about representation and a computationally efficient representation as soon as they are proven equivalent. The combination of parametricity and univalence supports transport à la carte : basic univalent transport, which stems from a type equivalence, can be complemented with additional proofs of equivalences between functions over these types, in order to be able to transport more programs and proofs, as well as to yield more efficient terms. We illustrate the use of univalent parametricity on several examples, including a recent integration of native integers in Coq. This work paves the way to easier-to-use proof assistants by supporting seamless programming and proving modulo equivalences.

Mechanized Theory of Event Structures: A Case of Parallel Register Machine

The true concurrency models, and in particular event structures, have been introduced in the 1980s as an alternative to operational interleaving semantics of concurrency, and nowadays they are regaining popularity. Event structures represent the causal dependency and conflict between the individual atomic actions of the system directly. This property leads to a more compact and concise representation of semantics. In this work-in-progress report, we present a theory of event structures mechanized in the COQ proof assistant and demonstrate how it can be applied to define certified executable semantics of a simple parallel register machine with shared memory.

Formalizing the Institution for Event-B in the Coq Proof Assistant

We formalize a fragment of the theory of institutions sufficient to establish basic facts about the institution "Image missing" for Event-B, and its relationship with the institution "Image missing" for first-order predicate logic. We prove the satisfaction condition for "Image missing" and encode the institution comorphism "Image missing" embedding "Image missing" in "Image missing" .