Publications - Publications

An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture

Hammond, A., Liu, Z., Pérami, T., Sewell, P., Birkedal, L., Pichon-Pharabod, J. — Fri, 05 Jan 2024 15:13:41 +0100

Very relaxed concurrency memory models, like those of the Arm-A, RISC-V, and IBM Power hardware architectures, underpin much of computing but break a fundamental intuition about programs, namely that syntactic program order and the reads-from relation always both induce order in the execution. Instead, out-of-order execution is allowed except where prevented by certain pairwise dependencies, barriers, or other synchronisation. This means that there is no notion of the 'current' state of the program, making it challenging to design (and prove sound) syntax-directed, modular reasoning methods like Hoare logics, as usable resources cannot implicitly flow from one program point to the next. We present AxSL, a separation logic for the relaxed memory model of Arm-A, that captures the fine-grained reasoning underpinning the low-overhead synchronisation mechanisms used by high-performance systems code. In particular, AxSL allows transferring arbitrary resources using relaxed reads and writes when they induce inter-thread ordering. We mechanise AxSL in the Iris separation logic framework, illustrate it on key examples, and prove it sound with respect to the axiomatic memory model of Arm-A. Our approach is largely generic in the axiomatic model and in the instruction-set semantics, offering a potential way forward for compositional reasoning for other similar models, and for the combination of production concurrency models and full-scale ISAs.

Towards Univalent Reference Types

Sterling, J., Gratzer, D., Birkedal, L. — Thu, 01 Feb 2024 15:13:41 +0100

We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voevodsky’s univalent foundations. We observe for the first time the profound impact of univalence on the denotational semantics of mutable state. Univalence automatically ensures that all computations are invariant under symmetries of the heap – a bountiful source of program equivalences. In particular, even the most simplistic univalent model enjoys many new equations that do not hold when the same constructions are carried out in the universes of traditional set-level (extensional) type theory.

The Essence of Generalized Algebraic Data Types

Sieczkowski, F., Stepanenko, S., Sterling, J., Birkedal, L. — Mon, 01 Jan 2024 15:13:41 +0100

This paper considers direct encodings of generalized algebraic data types (GADTs) in a minimal suitable lambda-calculus. To this end, we develop an extension of System F_ω with recursive types and internalized type equalities with injective constant type constructors. We show how GADTs and associated pattern-matching constructs can be directly expressed in the calculus, thus showing that it may be treated as a highly idealized modern functional programming language. We prove that the internalized type equalities in conjunction with injectivity rules increase the expressive power of the calculus by establishing a non-macro-expressibility result in F_ω, and prove the system type-sound via a syntactic argument. Finally, we build two relational models of our calculus: a simple, unary model that illustrates a novel, two-stage interpretation technique, necessary to account for the equational constraints; and a more sophisticated, binary model that relaxes the construction to allow, for the first time, formal reasoning about data-abstraction in a calculus equipped with GADTs.

Asynchronous Probabilistic Couplings in Higher-Order Separation Logic

Gregersen, S. O., Aguirre, A., Haselwarter, P. G., Tassarotti, J., Birkedal, L. — Mon, 01 Jan 2024 15:13:41 +0100

Probabilistic couplings are the foundation for many probabilistic relational program logics and arise when relating random sampling statements across two programs. In relational program logics, this manifests as dedicated coupling rules that, e.g., say we may reason as if two sampling statements return the same value. However, this approach fundamentally requires aligning or "synchronizing"the sampling statements of the two programs which is not always possible. In this paper, we develop Clutch, a higher-order probabilistic relational separation logic that addresses this issue by supporting asynchronous probabilistic couplings. We use Clutch to develop a logical step-indexed logical relation to reason about contextual refinement and equivalence of higher-order programs written in a rich language with a probabilistic choice operator, higher-order local state, and impredicative polymorphism. Finally, we demonstrate our approach on a number of case studies. All the results that appear in the paper have been formalized in the Coq proof assistant using the Coquelicot library and the Iris separation logic framework.

Welcome from the Chairs

Pientka, B., Blazy, S., Traytel, D., Timany, A. — Tue, 09 Jan 2024 15:13:41 +0100

Modular Denotational Semantics for Effects with Guarded Interaction Trees

Frumin, D., Timany, A., Birkedal, L. — Mon, 01 Jan 2024 15:13:41 +0100

We present guarded interaction trees - a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq, inspired by domain theory and the recently proposed interaction trees. We also present an accompanying separation logic for reasoning about guarded interaction trees. To demonstrate that guarded interaction trees provide a convenient domain for interpreting higher-order languages with effects, we define an interpretation of a PCF-like language with effects and show that this interpretation is sound and computationally adequate; we prove the latter using a logical relation defined using the separation logic. Guarded interaction trees also allow us to combine different effects and reason about them modularly. To illustrate this point, we give a modular proof of type soundness of cross-language interactions for safe interoperability of different higher-order languages with different effects. All results in the paper are formalized in Coq using the Iris logic over guarded type theory.

Modular Verification of State-Based CRDTs in Separation Logic

Nieto, A., Daby-Seesaram, A., Gondelman, L., Timany, A., Birkedal, L. — Sat, 01 Jul 2023 15:13:41 +0200

Conflict-free Replicated Datatypes (CRDTs) are a class of distributed data structures that are highly-available and weakly consistent. The CRDT taxonomy is further divided into two subclasses: state-based and operation-based (op-based). Recent prior work showed how to use separation logic to verify convergence and functional correctness of op-based CRDTs while (a) verifying implementations (as opposed to high-level protocols), (b) giving high level specifications that abstract from low-level implementation details, and (c) providing specifications that are modular (i.e. allow client code to use the CRDT like an abstract data type). We extend this separation logic approach to verification of CRDTs to handle state-based CRDTs, while respecting the desiderata (a)–(c). The key idea is to track the state of a CRDT as a function of the set of operations that produced that state. Using the observation that state-based CRDTs are automatically causally-consistent, we obtain CRDT specifications that are agnostic to whether a CRDT is state- or op-based. When taken together with prior work, our technique thus provides a unified approach to specification and verification of op- and state-based CRDTs. We have tested our approach by verifying StateLib, a library for building state-based CRDTs. Using StateLib, we have further verified convergence and functional correctness of multiple example CRDTs from the literature. Our proofs are written in the Aneris distributed separation logic and are mechanized in Coq.

The Last Yard

Mon, 01 Jan 2024 15:13:41 +0100

The field of high-assurance cryptography is quickly maturing, yet a unified foundational framework for end-to-end formal verification of efficient cryptographic implementations is still missing. To address this gap, we use the Coq proof assistant to formally connect three existing tools: (1) the Hacspec emergent cryptographic specification language; (2) the Jasmin language for efficient, high-assurance cryptographic implementations; and (3) the SSProve foundational verification framework for modular cryptographic proofs. We first connect Hacspec with SSProve by devising a new translation from Hacspec specifications to imperative SSProve code. We validate this translation by considering a second, more standard translation from Hacspec to purely functional Coq code and generate a proof of the equivalence between the code produced by the two translations. We further define a translation from Jasmin to SSProve, which allows us to formally reason in SSProve about efficient cryptographic implementations in Jasmin. We prove this translation correct in Coq with respect to Jasmin's operational semantics. Finally, we demonstrate the usefulness of our approach by giving a foundational end-to-end Coq proof of an efficient AES implementation. For this case study, we start from an existing Jasmin implementation of AES that makes use of hardware acceleration and prove that it conforms to a specification of the AES standard written in Hacspec. We use SSProve to formalize the security of the encryption scheme based on the Jasmin implementation of AES.

A manifesto for applicable formal methods

Gleirscher, M., van de Pol, J., Woodcock, J. — Fri, 01 Dec 2023 15:13:41 +0100

Recently, formal methods have been used in large industrial organisations (including AWS, Facebook/Meta, and Microsoft) and have proved to be an effective part of a software engineering process finding important bugs. Perhaps because of that, practitioners are interested in using them more often. Nevertheless, formal methods are far less applied than expected, particularly for safety-critical systems where they are strongly recommended and have the most significant potential. We hypothesise that formal methods still seem not applicable enough or ready for their intended use in such areas. In critical software engineering, what do we mean when we speak of a formal method? And what does it mean for such a method to be applicable both from a scientific and practical viewpoint? Based on what the literature tells about the first question, with this manifesto, we identify key challenges and lay out a set of guiding principles that, when followed by a formal method, give rise to its mature applicability in a given scope. Rather than exercising criticism of past developments, this manifesto strives to foster increased use of formal methods in any appropriate context to the maximum benefit.

Cerise

Georges, A. L., Guéneau, A., Van Strydonck, T., et al. — Mon, 12 Feb 2024 15:13:41 +0100

A capability machine is a type of CPU allowing fine-grained privilege separation using capabilities, machine words that represent certain kinds of authority. We present a mathematical model and accompanying proof methods that can be used for formal verification of functional correctness of programs running on a capability machine, even when they invoke and are invoked by unknown (and possibly malicious) code. We use a program logic called Cerise for reasoning about known code, and an associated logical relation, for reasoning about unknown code. The logical relation formally captures the capability safety guarantees provided by the capability machine. The Cerise program logic, logical relation, and all the examples considered in the paper have been mechanized using the Iris program logic framework in the Coq proof assistant. The methodology we present underlies recent work of the authors on formal reasoning about capability machines [15, 33, 37], but was left somewhat implicit in those publications. In this paper we present a pedagogical introduction to the methodology, in a simpler setting (no exotic capabilities), and starting from minimal examples. We work our way up to new results about a heap-based calling convention and implementations of sophisticated object-capability patterns of the kind previously studied for high-level languages with object-capabilities, demonstrating that the methodology scales to such reasoning.

A denotationally-based program logic for higher-order store

Aagaard, F. L., Sterling, J., Birkedal, L. — Sun, 01 Jan 2023 15:13:41 +0100

Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice

Aguirre, A., Birkedal, L. — Mon, 09 Jan 2023 15:13:41 +0100

Developing denotational models for higher-order languages that combine probabilistic and nondeterministic choice is known to be very challenging. In this paper, we propose an alternative approach based on operational techniques. We study a higher-order language combining parametric polymorphism, recursive types, discrete probabilistic choice and countable nondeterminism. We define probabilistic generalizations of may- and must-termination as the optimal and pessimal probabilities of termination. Then we define step-indexed logical relations and show that they are sound and complete with respect to the induced contextual preorders. For may-equivalence we use step-indexing over the natural numbers whereas for must-equivalence we index over the countable ordinals. We then show than the probabilities of may- and must-termination coincide with the maximal and minimal probabilities of termination under all schedulers. Finally we derive the equational theory induced by contextual equivalence and show that it validates the distributive combination of the algebraic theories for probabilistic and nondeterministic choice.

Melocoton

Guéneau, A., Hostert, J., Spies, S., Sammler, M., Birkedal, L., Dreyer, D. — Sun, 01 Oct 2023 15:13:41 +0200

In recent years, there has been tremendous progress on developing program logics for verifying the correctness of programs in a rich and diverse array of languages. Thus far, however, such logics have assumed that programs are written entirely in a single programming language. In practice, this assumption rarely holds since programs are often composed of components written in different programming languages, which interact with one another via some kind of foreign function interface (FFI). In this paper, we take the first steps towards the goal of developing program logics for multi-language verification. Specifically, we present Melocoton, a multi-language program verification system for reasoning about OCaml, C, and their interactions through the OCaml FFI. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI - previously only described in prose in the OCaml manual - as well as the first program logic to reason about the interactions of program components written in OCaml and C. Melocoton is fully mechanized in Coq on top of the Iris separation logic framework.

Spirea

Vindum, S. F., Birkedal, L. — Sun, 01 Oct 2023 15:13:41 +0200

Weak persistent memory (a.k.a. non-volatile memory) is an emerging technology that offers fast byte-addressable durable main memory. A wealth of algorithms and libraries has been developed to explore this exciting technology. As noted by others, this has led to a significant verification gap. Towards closing this gap, we present Spirea, the first concurrent separation logic for verification of programs under a weak persistent memory model. Spirea is based on the Iris and Perennial verification frameworks, and by combining features from these logics with novel techniques it supports high-level modular reasoning about crash-safe and thread-safe programs and libraries. Spirea is fully mechanized in the Coq proof assistant and allows for interactive development of proofs with the Iris Proof Mode. We use Spirea to verify several challenging examples with modular specifications. We show how our logic can verify thread-safety and crash-safety of non-blocking durable data structures with null-recovery, in particular the Treiber stack and the Michael-Scott queue adapted to persistent memory. This is the first time durable data structures have been verified with a program logic.

Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems

Madsen, M., Van De Pol, J., Henriksen, T. — Sun, 01 Oct 2023 15:13:41 +0200

As type and effect systems become more expressive there is an increasing need for efficient type inference. We consider a polymorphic effect system based on Boolean formulas where inference requires Boolean unification. Since Boolean unification involves semantic equivalence, conventional syntax-driven unification is insufficient. At the same time, existing Boolean unification techniques are ill-suited for type inference. We propose a hybrid algorithm for solving Boolean unification queries based on Boole's Successive Variable Elimination (SVE) algorithm. The proposed approach builds on several key observations regarding the Boolean unification queries encountered in practice, including: (i) most queries are simple, (ii) most queries involve a few flexible variables, (iii) queries are likely to repeat due similar programming patterns, and (iv) there is a long tail of complex queries. We exploit these observations to implement several strategies for formula minimization, including ones based on tabling and binary decision diagrams. We implement the new hybrid approach in the Flix programming language. Experimental results show that by reducing the overhead of Boolean unification, the compilation throughput increases from 8,580 lines/sec to 15,917 lines/sec corresponding to a 1.8x speed-up. Further, the overhead on type and effect inference time is only 16% which corresponds to an overhead of less than 7% on total compilation time. We study the hybrid approach and demonstrate that each design choice improves performance.

Finitary Type Theories With and Without Contexts

Haselwarter, P. G., Bauer, A. — Fri, 01 Dec 2023 15:13:41 +0100

We give a definition of finitary type theories that subsumes many examples of dependent type theories, such as variants of Martin–Löf type theory, simple type theories, first-order and higher-order logics, and homotopy type theory. We prove several general meta-theorems about finitary type theories: weakening, admissibility of substitution and instantiation of metavariables, derivability of presuppositions, uniqueness of typing, and inversion principles. We then give a second formulation of finitary type theories in which there are no explicit contexts. Instead, free variables are explicitly annotated with their types. We provide translations between finitary type theories with and without contexts, thereby showing that they have the same expressive power. The context-free type theory is implemented in the nucleus of the Andromeda 2 proof assistant.

SSProve

Haselwarter, P. G., Rivas, E., Van Muylder, A., et al. — Sat, 01 Jul 2023 15:13:41 +0200

State-separating proofs (SSP) is a recent methodology for structuring game-based cryptographic proofs in a modular way, by using algebraic laws to exploit the modular structure of composed protocols. While promising, this methodology was previously not fully formalized and came with little tool support. We address this by introducing SSProve, the first general verification framework for machine-checked state-separating proofs. SSProve combines high-level modular proofs about composed protocols, as proposed in SSP, with a probabilistic relational program logic for formalizing the lower-level details, which together enable constructing machine-checked cryptographic proofs in the Coq proof assistant. Moreover, SSProve is itself fully formalized in Coq, including the algebraic laws of SSP, the soundness of the program logic, and the connection between these two verification styles.To illustrate SSProve, we use it to mechanize the simple security proofs of ElGamal and pseudo-random-function-based encryption. We also validate the SSProve approach by conducting two more substantial case studies: First, we mechanize an SSP security proof of the key encapsulation mechanism-data encryption mechanism (KEM-DEM) public key encryption scheme, which led to the discovery of an error in the original paper proof that has since been fixed. Second, we use SSProve to formally prove security of the sigma-protocol zero-knowledge construction, and we moreover construct a commitment scheme from a sigma-protocol to compare with a similar development in CryptHOL. We instantiate the security proof for sigma-protocols to give concrete security bounds for Schnorr's sigma-protocol.

Predicting Memory Demands of BDD Operations using Maximum Graph Cuts

Sølvsten, S., van de Pol, J. — Sun, 01 Oct 2023 15:13:41 +0200

The BDD package Adiar manipulates Binary Decision Diagrams (BDDs) in external memory. This enables handling big BDDs, but the performance suffers when dealing with moderate-sized BDDs. This is mostly due to initializing expensive external memory data structures, even if their contents can fit entirely inside internal memory.

The contents of these auxiliary data structures always correspond to a graph cut in an input or output BDD. Specifically, these cuts respect the levels of the BDD. We formalise the shape of these cuts and prove sound upper bounds on their maximum size for each BDD operation.

We have implemented these upper bounds within Adiar. With these bounds, it can predict whether a faster internal memory variant of the auxiliary data structures can be used. In practice, this improves Adiar’s running time across the board. Specifically for the moderate-sized BDDs, this results in an average reduction of the computation time by 86.1% (median of 89.7%). In some cases, the difference is even 99.9%. When checking equivalence of hardware circuits from the EPFL Benchmark Suite, for one of the instances the time was decreased by 52 h.

Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols

Gondelman, L., Hinrichsen, J. K., Pereira, M., Timany, A., Birkedal, L. — Tue, 01 Aug 2023 15:13:41 +0200

We present a foundationally verified implementation of a reliable communication library for asynchronous client-server communication, and a stack of formally verified components on top thereof. Our library is implemented in an OCaml-like language on top of UDP and features characteristic traits of existing protocols, such as a simple handshaking protocol, bidirectional channels, and retransmission/acknowledgement mechanisms. We verify the library in the Aneris distributed separation logic using a novel proof pattern - -dubbed the session escrow pattern - -based on the existing escrow proof pattern and the so-called dependent separation protocols, which hitherto have only been used in a non-distributed concurrent setting. We demonstrate how our specification of the reliable communication library simplifies formal reasoning about applications, such as a remote procedure call library, which we in turn use to verify a lazily replicated key-value store with leader-followers and clients thereof. Our development is highly modular - -each component is verified relative to specifications of the components it uses (not the implementation). All our results are formalized in the Coq proof assistant.

VMSL

Thu, 01 Jun 2023 15:13:41 +0200

Thin hypervisors make it possible to isolate key security components like keychains, fingerprint readers, and digital wallets from the easily-compromised operating system. To work together, virtual machines running on top of the hypervisor can make hypercalls to the hypervisor to share pages between each other in a controlled way. However, the design of such hypercall ABIs remains a delicate balancing task between conflicting needs for expressivity, performance, and security. In particular, it raises the question of what makes the specification of a hypervisor, and of its hypercall ABIs, good enough for the virtual machines. In this paper, we validate the expressivity and security of the design of the hypercall ABIs of Arm's FF-A. We formalise a substantial fragment of FF-A as a machine with a simplified ISA in which hypercalls are steps of the machine. We then develop VMSL, a novel separation logic, which we prove sound with respect to the machine execution model, and use it to reason modularly about virtual machines which communicate through the hypercall ABIs, demonstrating the hypercall ABIs' expressivity. Moreover, we use the logic to prove robust safety of communicating virtual machines, that is, the guarantee that even if some of the virtual machines are compromised and execute unknown code, they cannot break the safety properties of other virtual machines running known code. This demonstrates the intended security guarantees of the hypercall ABIs. All the results in the paper have been formalised in Coq using the Iris framework.

Iris-Wasm

Rao, X., Georges, A. L., Legoupil, M., et al. — Thu, 01 Jun 2023 15:13:41 +0200

WebAssembly makes it possible to run C/C++ applications on the web with near-native performance. A WebAssembly program is expressed as a collection of higher-order ML-like modules, which are composed together through a system of explicit imports and exports using a host language, enabling a form of higher-order modular programming. We present Iris-Wasm, a mechanized higher-order separation logic building on a specification of Wasm 1.0 mechanized in Coq and the Iris framework. Using Iris-Wasm, we are able to specify and verify individual modules separately, and then compose them modularly in a simple host language featuring the core operations of the WebAssembly JavaScript Interface. Building on Iris-Wasm, we develop a logical relation that enforces robust safety: unknown, adversarial code can only affect other modules through the functions that they explicitly export. Together, the program logic and the logical relation allow us to formally verify functional correctness of WebAssembly programs, even when they invoke and are invoked by unknown code, thereby demonstrating that WebAssembly enforces strong isolation between modules.

Optimal Layout Synthesis for Quantum Circuits as Classical Planning

Shaik, I., van de Pol, J. — Sun, 01 Jan 2023 15:13:41 +0100

Implicit State and Goals in QBF Encodings for Positional Games (extended version)

Shaik, I., Mayer-Eichberger, V., van de Pol, J., Saffidine, A. — Sun, 01 Jan 2023 15:13:41 +0100

Concise QBF Encodings for Games on a Grid (extended version)

Shaik, I., van de Pol, J. — Sun, 01 Jan 2023 15:13:41 +0100

Syntax and semantics of modal type theory

Gratzer, D. — Sun, 01 Oct 2023 15:13:41 +0200

One idiosyncratic framing of type theory is as the study of operations invariant
under substitution. Modal type theory, by contrast, concerns the controlled inte-
gration of operations—modalities—into type theory which violate this discipline,
so-called non-fibered connectives. Modal type theory is therefore built around a
fundamental tension: the desire to include modalities and powerful principles for
reasoning with them on one hand, and the need to maintain the conveniences and
character of Martin-Löf type theory which stem from substitution invariance.

In this thesis we thoroughly explore and discuss this contradiction. We discuss
several different formulations of modal type theory, explore their various syntactic
properties, and relate them through their categorical semantics. In particular, we
show that most modal type theories that have arisen in the last two decades can be
understood through the abstraction of weak dependent right adjoints. We also put
forward a new general modal type theory, MTT, based around this abstraction.

The generality of MTT means that, without any additional work, it can be
specialized to an arbitrary collection of type theories related by modalities and
natural transformations between them. It is therefore easy to obtain a type theory
for a comonad, an adjunction, a local topos, or any other number of complex and
realistic scenarios. In addition to showing that many modal type theories are closely
related to specific instantiations of MTT, we thoroughly explore the syntax and
semantics of MTT itself. We prove that MTT enjoys an unconditional normalization
result and decidable type-checking under mild assumptions. We show how MTT
may be interpreted into a wide variety of structured categories and use this to study
the expressive power of the type theory and various extensions thereof.

Finally, we explore several concrete applications of MTT in the context of
guarded type theory and guarded denotational semantics. We propose a highly usable
language for guarded recursion and explore its particular models and metatheorems.
We show a relatively sharp result bounding the extent to which classical guarded
recursion can be added to any type theory with decidable type-checking and propose
a system to mitigate this issue. Finally, we conduct an in-depth case study using
guarded MTT to obtain a fully synthetic account of the Iris program logic, proving
adequacy in a fully internal manner.

Under Lock and Key

Kavvos, G. A., Gratzer, D. — Thu, 01 Jun 2023 15:13:41 +0200

We present a proof system for a multimodal logic, based on our previous work on a multimodal Martin-Loef type theory. The specification of modes, modalities, and implications between them is given as a mode theory, i.e. a small 2-category. The logic is extended to a lambda calculus, establishing a Curry-Howard correspondence.

mitten

Stassen, P. J. A., Gratzer, D., Birkedal, L. — Tue, 01 Aug 2023 15:13:41 +0200

Recently, there has been a growing interest in type theories which include modalities, unary type constructors which need not commute with substitution. Here we focus on MTT [15], a general modal type theory which can internalize arbitrary collections of (dependent) right adjoints [7]. These modalities are specified by mode theories [20], 2-categories whose objects corresponds to modes, morphisms to modalities, and 2-cells to natural transformations between modalities. We contribute a defunctionalized NbE algorithm which reduces the type-checking problem for MTT to deciding the word problem for the mode theory. The algorithm is restricted to the class of preordered mode theories – mode theories with at most one 2-cell between any pair of modalities. Crucially, the normalization algorithm does not depend on the particulars of the mode theory and can be applied without change to any preordered collection of modalities. Furthermore, we specify a bidirectional syntax for MTT together with a type-checking algorithm. We further contribute mitten, a flexible experimental proof assistant implementing these algorithms which supports all decidable preordered mode theories without alteration.

Programming with Purity Reflection

Madsen, M., Pol, J. v. d. — Sat, 01 Jul 2023 15:13:41 +0200

We present purity reflection, a programming language feature that enables higher-order functions to inspect the purity of their function arguments and to vary their behavior based on this information. The upshot is that operations on data structures can selectively use lazy and/or parallel evaluation while ensuring that side effects are never lost or re-ordered. The technique builds on a recent Hindley-Milner style type and effect system based on Boolean unification which supports both effect polymorphism and complete type inference. We illustrate that avoiding the so-called 'poisoning problem' is crucial to support purity reflection.
We propose several new data structures that use purity reflection to switch between eager and lazy, sequential and parallel evaluation. We propose a DelayList, which is maximally lazy but switches to eager evaluation for impure operations. We also propose a DelayMap which is maximally lazy in its values, but also exploits eager and parallel evaluation.
We implement purity reflection as an extension of the Flix programming language. We present a new effect-aware form of monomorphization that eliminates purity reflection at compile-time. And finally, we evaluate the cost of this new monomorphization on compilation time and on code size, and determine that it is minimal.

A Truly Symbolic Linear-Time Algorithm for SCC Decomposition

Sat, 01 Apr 2023 15:13:41 +0200

Decomposing a directed graph to its strongly connected components (SCCs) is a fundamental task in model checking. To deal with the state-space explosion problem, graphs are often represented symbolically using binary decision diagrams (BDDs), which have exponential compression capabilities. The theoretically-best symbolic algorithm for SCC decomposition is Gentilini et al’s SKELETON algorithm, that uses O(n) symbolic steps on a graph of n nodes. However, SKELETON uses Θ(n) symbolic objects, as opposed to (poly-)logarithmically many, which is the norm for symbolic algorithms, thereby relinquishing its symbolic nature. Here we present CHAIN, a new symbolic algorithm for SCC decomposition that also makes O(n) symbolic steps, but further uses logarithmic space, and is thus truly symbolic. We then extend CHAIN to COLOREDCHAIN, an algorithm for SCC decomposition on edge-colored graphs, which arise naturally in model-checking a family of systems. Finally, we perform an experimental evaluation of CHAIN among other standard symbolic SCC algorithms in the literature. The results show that CHAIN is competitive on almost all benchmarks, and often faster, while it clearly outperforms all other algorithms on challenging inputs.

Validation of QBF Encodings with Winning Strategies

Shaik, I., Heisinger, M., Seidl, M., Pol, J. v. d. — Tue, 01 Aug 2023 15:13:41 +0200

When using a QBF solver for solving application problems encoded to quantified Boolean formulas (QBFs), mainly two things can potentially go wrong: (1) the solver could be buggy and return a wrong result or (2) the encoding could be incorrect. To ensure the correctness of solvers, sophisticated fuzzing and testing techniques have been presented. To ultimately trust a solving result, solvers have to provide a proof certificate that can be independently checked. Much less attention, however, has been paid to the question how to ensure the correctness of encodings.
The validation of QBF encodings is particularly challenging because of the variable dependencies introduced by the quantifiers. In contrast to SAT, the solution of a true QBF is not simply a variable assignment, but a winning strategy. For each existential variable x, a winning strategy provides a function that defines how to set x based on the values of the universal variables that precede x in the quantifier prefix. Winning strategies for false formulas are defined dually.
In this paper, we provide a tool for validating encodings using winning strategies and interactive game play with a QBF solver. As the representation of winning strategies can get huge, we also introduce validation based on partial winning strategies. Finally, we employ winning strategies for testing if two different encodings of one problem have the same solutions.

Adiar 1.1

Sølvsten, S., van de Pol, J. — Thu, 01 Jun 2023 15:13:41 +0200

We outline how support for Zero-suppressed Decision Diagrams (ZDDs) has been achieved for the external memory BDD package Adiar. This allows one to use ZDDs to solve various problems despite their size exceed the machine’s limit of internal memory.

Faster constant-time evaluation of the Kronecker symbol with application to elliptic curve hashing

Aranha, D. F., Hvass, B. S., Spitters, B., Tibouchi, M. — Wed, 01 Nov 2023 15:13:41 +0100

Formalising Decentralised Exchanges in Coq

Nielsen, E. H., Annenkov, D., Spitters, B. — Sun, 01 Jan 2023 15:13:41 +0100

The number of attacks and accidents leading to significant losses of crypto-assets is growing. According to Chainalysis, in 2021, approx. $14 billion has been lost due to various incidents, and this number is dominated by Decentralized Finance (DeFi) applications. To address these issues, one can use a collection of tools ranging from auditing to formal methods. We use formal verification and provide the first formalisation of a DeFi contract in a foundational proof assistant capturing contract interactions. We focus on Dexter2, a decentralized, non-custodial exchange for the Tezos network similar to Uniswap on Ethereum. The Dexter implementation consists of several smart contracts. This poses unique challenges for formalisation due to the complex contract interactions. Our formalisation includes proofs of functional correctness with respect to an informal specification for the contracts involved in Dexter's implementation. Moreover, our formalisation is the first to feature proofs of safety properties of the interacting smart contracts of a decentralized exchange. We have extracted our contract from Coq into CameLIGO code, so it can be deployed on the Tezos blockchain. Uniswap and Dexter are paradigmatic for a collection of similar contracts. Our methodology thus allows us to implement and verify DeFi applications featuring similar interaction patterns.

OblivIO:

Blaabjerg, J. F., Askarov, A. — Sun, 01 Jan 2023 15:13:41 +0100

Traffic analysis attacks remain a significant problem for online security. Communication between nodes can be observed by network level attackers as it inherently takes place in the open. Despite online services increasingly using encrypted traffic, the shape of the traffic is not hidden.
To prevent traffic analysis, the shape of a system's traffic must be independent of secrets.

We investigate adapting the data-oblivious approach the reactive setting and present OblivIO, a secure language for writing reactive programs driven by network events. Our approach pads with dummy messages to hide which program sends are genuinely executed. We use an information-flow type system to provably enforce timing-sensitive noninterference. The type system is extended with potentials to bound the overhead in traffic introduced by our approach.
We address challenges that arise from joining data-oblivious and reactive programming and demonstrate the feasibility of our resulting language by developing an interpreter that implements security critical operations as constant-time algorithms.

Efficient Convex Zone Merging in Parametric Timed Automata

André, É., Marinho, D., Petrucci, L., van de Pol, J. — Sat, 01 Jan 2022 15:13:41 +0100

Parametric timed automata are a powerful formalism for reasoning on concurrent real-time systems with unknown or uncertain timing constants. Reducing their state space is a significant way to reduce the inherently large analysis times. We present here different merging reduction techniques based on convex union of constraints (parametric zones), allowing to decrease the number of states while preserving the correctness of verification and synthesis results. We perform extensive experiments, and identify the best heuristics in practice, bringing a significant decrease in the computation time on a benchmarks library.

Exploring a Parallel SCC Algorithm

van de Pol, J. — Sat, 01 Oct 2022 15:13:41 +0200

We explore a parallel SCC-decomposition algorithm based on a concurrent Union-Find data structure. In order to increase confidence in the algorithm, it is modelled in TLA ⁺. The TLC model checker is used to demonstrate that it works correctly for all possible interleavings of two workers on a number of small input graphs. To increase the understanding of the algorithm, we investigate some potential invariants. Some of these are refuted, revealing that the algorithm allows suboptimal (but still correct) executions. Finally, we investigate some modifications of the algorithm. It turns out that most modifications lead to an incorrect algorithm, as revealed by the TLC model checker. We view this exploration as a first step to a full understanding and a rigorous correctness proof based on invariants or step-wise refinement.

Safe and Secure Future AI-Driven Railway Technologies

Seisenberger, M., ter Beek, M. H., Fan, X., et al. — Sat, 01 Jan 2022 15:13:42 +0100

In 2020, the EU launched its sustainable and smart mobility strategy, outlining how it plans to have a 90% reduction in transport emission by 2050. Central to achieving this goal will be the improvement of rail technology, with many new data-driven visionary systems being proposed. AI will be the enabling technology for many of those systems. However, safety and security guarantees will be key for wide-spread acceptance and uptake by Industry and Society. Therefore, suitable verification and validation techniques are needed. In this article, we argue how formal methods research can contribute to the development of modern Railway systems—which may or may not make use of AI techniques—and present several research problems and techniques worth to be further considered.

Classical Planning as QBF without Grounding

Shaik, I., van de Pol, J. — Wed, 01 Jun 2022 15:13:42 +0200

Most classical planners use grounding as a preprocessing step, essentially reducing planning to propositional logic. However, grounding involves instantiating all action rules with concrete object combinations, and results in large encodings for SAT/QBF-based planners. This severe cost in memory becomes a main bottleneck when actions have many parameters, such as in the Organic Synthesis problems from the IPC 2018 competition. We provide a compact QBF encoding that is logarithmic in the number of objects and avoids grounding completely, by using universal quantification for object combinations. We show that we can solve some of the Organic Synthesis problems, which could not be handled before by any SAT/QBF based planners due to grounding.

Unifying Cubical and Multimodal Type Theory

Aagaard, F. L., Kristensen, M., Gratzer, D., Birkedal, L. — Sat, 01 Jan 2022 15:13:42 +0100

Modular verification of op-based CRDTs in separation logic

Nieto, A., Gondelman, L., Reynaud, A., Timany, A., Birkedal, L. — Sat, 01 Oct 2022 15:13:42 +0200

Operation-based Conflict-free Replicated Data Types (op-based CRDTs) are a family of distributed data structures where all operations are designed to commute, so that replica states eventually converge. Additionally, op-based CRDTs require that operations be propagated between replicas in causal order. This paper presents a framework for verifying safety properties of CRDT implementations using separation logic. The framework consists of two libraries. One implements a Reliable Causal Broadcast (RCB) protocol so that replicas can exchange messages in causal order. A second "OpLib"library then uses RCB to simplify the creation and correctness proofs of op-based CRDTs. OpLib allows clients to implement new CRDTs as purely-functional data structures, without having to reason about network operations, concurrency control and mutable state, and without having to each time re-implement causal broadcast. Using OpLib, we have implemented 12 example CRDTs from the literature, including multiple versions of replicated registers and sets, two CRDT combinators for products and maps, and two example use cases of the map combinator. Our proofs are conducted in the Aneris distributed separation logic and are formalized in Coq. Our technique is the first work on verification of op-based CRDTs that satisfies both of the following properties: it is modular and targets executable implementations, as opposed to high-level protocols.

Proving full-system security properties under multiple attacker models on capability machines

Strydonck, T. V., Georges, A. L., Guéneau, A., et al. — Sat, 01 Oct 2022 15:13:42 +0200

Assembly-level protection mechanisms (virtual mem-ory, trusted execution environments, virtualization) make it possible to guarantee security properties of a full system in the presence of arbitrary attacker provided code. However, they typically only support a single trust boundary: code is either trusted or untrusted, and protection cannot be nested. Capability machines provide protection mechanisms that are more fine-grained and that do support arbitrary nesting of protection. We show in this paper how this enables the formal verification of full-system security properties under multiple attacker models: differ-ent security objectives of the full system can be verified under a different choice of trust boundary (i.e. under a different attacker model). The verification approach we propose is modular, and is robust: code outside the trust boundary for a given security objective can be arbitrary, unverified attacker-provided code. It is based on the use of universal contracts for untrusted adversarial code: sound, conservative contracts which can be combined with manual verification of trusted components in a compositional program logic. Compositionality of the program logic also allows us to reuse common parts in the analyses for different attacker models. We instantiate the approach concretely by extending an existing capability machine model with support for memory-mapped 1/0 and we obtain full system, machine-verified security properties about external effect traces while limiting the manual verification effort to a small trusted computing base relevant for the specific property under study.

Verification and synthesis of co-simulation algorithms subject to algebraic loops and adaptive steps

Hansen, S. T., Thule, C., Gomes, C., et al. — Thu, 01 Dec 2022 15:13:42 +0100

Simulation-based analyses are becoming increasingly vital for the development of cyber-physical systems. Co-simulation is one such technique, enabling the coupling of specialized simulation tools through an orchestration algorithm. The orchestrator describes how to coordinate the simulation of multiple simulation tools. The simulation result depends on the orchestration algorithm that must stabilize algebraic loops, choose the simulation resolution, and adhere to each simulation tool’s implementation. This paper describes how to verify that an orchestration algorithm respects all contracts related to the simulation tool’s implementation and how to synthesize such tailored orchestration algorithms. The approaches work for complex and adaptive co-simulation scenarios and have been applied to several real-world case studies.

Normalization for Multimodal Type Theory

Daniel, G. — Mon, 01 Aug 2022 15:13:42 +0200

We prove normalization for MTT, a general multimodal dependent type theory capable of expressing modal type theories for guarded recursion, internalized parametricity, and various other prototypical modal situations. We prove that deciding type checking and conversion in MTT can be reduced to deciding the equality of modalities in the underlying modal situation, immediately yielding a type checking algorithm for all instantiations of MTT in the literature. This proof follows from a generalization of synthetic Tait computability-an abstract approach to gluing proofs-to account for modalities. This extension is based on MTT itself, so that this proof also constitutes a signifcant case study of MTT.

Modalities and Parametric Adjoints

Gratzer, D., Cavallo, E., Kavvos, G. A., Guatto, A., Birkedal, L. — Fri, 01 Jul 2022 15:13:42 +0200

Birkedal et al. recently introduced dependent right adjoints as an important class of (non-fibered) modalities in type theory. We observe that several aspects of their calculus are left underdeveloped and that it cannot serve as an internal language. We resolve these problems by assuming that the modal context operator is a parametric right adjoint. We show that this hitherto unrecognized structure is common. Based on these discoveries we present a new well-behaved Fitch-style multimodal type theory, which can be used as an internal language. Finally, we apply this syntax to guarded recursion and parametricity.

Later credits

Spies, S., Gäher, L., Tassarotti, J., et al. — Mon, 29 Aug 2022 15:13:42 +0200

In the past two decades, step-indexed logical relations and separation logics have both come to play a major role in semantics and verification research. More recently, they have been married together in the form of step-indexed separation logics like VST, iCAP, and Iris, which provide powerful tools for (among other things) building semantic models of richly typed languages like Rust. In these logics, propositions are given semantics using a step-indexed model, and step-indexed reasoning is reflected into the logic through the so-called "later"modality. On the one hand, this modality provides an elegant, high-level account of step-indexed reasoning; on the other hand, when used in sufficiently sophisticated ways, it can become a nuisance, turning perfectly natural proof strategies into dead ends. In this work, we introduce later credits, a new technique for escaping later-modality quagmires. By leveraging the second ancestor of these logics - separation logic - later credits turn "the right to eliminate a later"into an ownable resource, which is subject to all the traditional modular reasoning principles of separation logic. We develop the theory of later credits in the context of Iris, and present several challenging examples of proofs and proof patterns which were previously not possible in Iris but are now possible due to later credits.

Finding Smart Contract Vulnerabilities with ConCert's Property-Based Testing Framework

Milo, M., Nielsen, E. H., Annenkov, D., Spitters, B. — Sat, 01 Oct 2022 15:13:42 +0200

We provide three detailed case studies of vulnerabilities in smart contracts, and show how property based testing would have found them: 1. the Dexter1 token exchange; 2. the iToken; 3. the ICO of Brave's BAT token. The last example is, in fact, new, and was missed in the auditing process. We have implemented this testing in ConCert, a general executable model/specification of smart contract execution in the Coq proof assistant. ConCert contracts can be used to generate verified smart contracts in Tezos' LIGO and Concordium's rust language. We thus show the effectiveness of combining formal verification and property-based testing of smart contracts.

Extracting functional programs from Coq, in Coq

Annenkov, D., Milo, M., Nielsen, J. B., Spitters, B. A.S. — Mon, 01 Aug 2022 15:13:42 +0200

We implement extraction of Coq programs to functional languages based on MetaCoq's certified erasure. We extend the MetaCoq erasure output language with typing information and use it as an intermediate representation, which we call. We complement the extraction functionality with a full pipeline that includes several standard transformations (e.g. eta-expansion and inlining) implemented in a proof-generating manner along with a verified optimisation pass removing unused arguments. We prove the pass correct wrt. a conventional call-by-value operational semantics of functional languages. From the optimised representation, we obtain code in two functional smart contract languages, Liquidity and CameLIGO, the functional language Elm, and a subset of the multi-paradigm language for systems programming Rust. Rust is currently gaining popularity as a language for smart contracts, and we demonstrate how our extraction can be used to extract smart contract code for the Concordium network. The development is done in the context of the ConCert framework that enables smart contract verification. We contribute with two verified real-world smart contracts (boardroom voting and escrow), which we use, among other examples, to exemplify the applicability of the pipeline. In addition, we develop a verified web application and extract it to fully functional Elm code. In total, this gives us a way to write dependently typed programs in Coq, verify, and then extract them to several target languages while retaining a small trusted computing base of only MetaCoq and the pretty-printers into these languages.

A cubical language for bishop sets

Sterling, J., Angiuli, C., Gratzer, D. — Tue, 01 Mar 2022 15:13:42 +0100

We present XTT, a version of Cartesian cubical type theory specialized for Bishop sets à la Coquand, in which every type enjoys a definitional version of the uniqueness of identity proofs. Using cubical notions, XTT reconstructs many of the ideas underlying Observational Type Theory, a version of intensional type theory that supports function extensionality. We prove the canonicity property of XTT (that every closed boolean is definitionally equal to a constant) using Artin gluing.

Symbolic Synthesis of Indifferentiability Attacks

Rakotonirina, I., Ambrona, M., Aguirre, A., Barthe, G. — Sun, 01 May 2022 15:13:42 +0200

We propose automated methods for synthesising attacks against indifferentiability, a powerful simulation-based notion of security commonly used to reason about symmetric-key constructions. Our methods are inspired from symbolic cryptography which is popular to reason about, e.g., cryptographic protocols. For that, we introduce a core programming language for algebraic distinguishers and study the class of universal distinguishers, who win the indifferentiability game against every simulator; then, we show that the universality of algebraic distinguishers can be reduced to solving systems of algebraic, deducibility and static-equivalence constraints. Our approach is implemented in a tool, AutoDiff, which solves these constraint systems, and applies heuristics to automate the cryptanalysis (i.e., to search automatically for universal distinguishers). We evaluate the tool with many non-trivial attacks from the literature on Feistel networks and Even-Mansour blockciphers among others. Our tool is able to check the validity these attacks, and in many cases to synthesise them without guidance. To our knowledge, AutoDiff is the first practical tool for indifferentiability attacks.

A Stratified Approach to Löb Induction

Gratzer, D., Birkedal, L. — Wed, 01 Jun 2022 15:13:42 +0200

Guarded type theory extends type theory with a handful of modalities and constants to encode productive recursion. While these theories have seen widespread use, the metatheory of guarded type theories, particularly guarded dependent type theories remains underdeveloped. We show that integrating Löb induction is the key obstruction to unifying guarded recursion and dependence in a well-behaved type theory and prove a no-go theorem sharply bounding such type theories. Based on these results, we introduce GuTT: a stratified guarded type theory. GuTT is properly two type theories, sGuTT and dGuTT. The former contains only propositional rules governing Löb induction but enjoys decidable type-checking while the latter extends the former with definitional equalities. Accordingly, dGuTT does not have decidable type-checking. We prove, however, a novel guarded canonicity theorem for dGuTT, showing that programs in dGuTT can be run. These two type theories work in concert, with users writing programs in sGuTT and running them in dGuTT.