LogSem Seminar talks in 2022

05-12-2022: Relaxed virtual memory

Speaker: Ben Simner, University of Cambridge

Time: 13:00-14:00

Location: Ada-333

Abstract: Our modern systems rely heavily on the hardware implementations of virtual memory for security, for isolating processes within an operating system and multiple systems within a hypervisor. To make these implementations efficient, the hardware contains many optimisations, some of which affect the programmer-visible behaviour of our programs. We focus on Armv8-A, a ubiquitous hardware architecture found in most smartphones, many laptops, desktop machines, and servers. We seek to clarify these programmer-visible behaviours, create precise formal specifications of the architecture, create tooling to help users understand those specifications and to check the behaviours of their own programs, and to use these specifications and tools to reason about real-world code.

14-11-2022: Compact QBF encodings for planning and 2-player games

Speaker: Irfansha Shaik

Time: 13:00-14:00

Location: Ada-333

Abstract: Finding winning strategies for 2-player games is of great interest. Quantifier alternations in Quantified Boolean Formulas (QBF) can naturally express existence of a winning strategy of bounded depth. In this talk, I will present some of our ideas on encoding classical planning problems and 2-player games in QBF. We also propose a general input format GDDL for modelling several interesting games and an encoder into QBF for finding winning strategies. I will show a small demo of our tool and how to use QBF certificates for interactive game playing and encoding testing.

08-11-2022: Session Types for Information Flow Control and a Logical Relation for Noninterference

Speaker: Stephanie Balzer

Time: 15:00-16:00

Location: Zoom

Abstract: Noninterference guarantees that an attacker cannot infer secrets by interacting with a program. An information flow control (IFC) type system asserts noninterference by tracking the level of information learned and disallowing leakage to parties of lesser or unrelated level. In this talk, I explore session types as an enabler for tracking the flow of information. Session types stipulate according to which protocol messages must be exchanged along channels connecting concurrently executing processes (or threads). I develop an IFC type system for linear session-typed process calculus that employs possible worlds from hybrid logic to reason about security levels. To prove that well-typed programs in the resulting language ensure noninterference, I develop a logical relation. I survey what the main challenges in the development are — non-termination (because of general recursive types) and non-determinism (because of concurrency) — and explain how to address them. Distinguishing features of the resulting logical relation are its interactive nature (the program interacts with its context) and the use of an observation index (as opposed to a step index or later modality). The latter ensures compositionality despite concurrency.

31-10-2022: A Formal and Foundational Approach to Program Verification for Safety and Security

Speaker: Amin Timany

Time: 13:00-15:00

Location: Nygaard-395

Abstract: Formal program verification is an important approach to verifying safety and security of software systems. In this approach we define the semantics (i.e., the mathematical description of the behavior) of the program and specify programs' desirable properties, e.g., safety and security guarantees, in terms of their semantics. Program logics are formal mathematical tools (based on mathematical logic) which are used to establish that programs do indeed enjoy the aforementioned desirable properties. In this course, we will introduce the Iris program logic (https://www.iris-project.org) and discuss how it is used to specify and prove safety and security properties of software systems.

24-10-2022: Modelling and verifying distributed systems

Speaker: Jonas Kastberg Hinrichsen

Time: 13:00-14:00

Location: Nygaard-395

Abstract: The reliance on the well behaviour of interactions in a distributed systems is becoming increasingly important, especially in the unreliable setting, where messages can be duplicated, dropped, and reordered. As such, it is crucial that we have a way of formally describing the semantics of such a system, as well as reasoning about its safety – that any of its nodes do not crash – preferably in a modular approach. The Aneris framework – consisting of the AnerisLang semantics and the associated Aneris program logic – is asystem that addresses exactly that.

In this talk, I will provide some exposition to the Aneris framework, including some of the thoughts behind its semantics, and proof constructs. I will do so by presenting simple distributed programs, demonstrating the subtleties that can arise when writing a client for even such simple services. I will additionally go through a full verification of the programs, to give an impression on the usability of the Aneris framework.

10-10-2022: Concurrent Cerise - A Program Logic for Multi-core Capability Machine

Speaker: Bastien Rousseau

Time: 13:00-14:00

Location: Ada-333

Abstract: Memory safety is a major source of vulnerabilities in computer systems. To prevent these memory safety issues, capability machine are a type of security-oriented CPU that offer a fine-grained compartmentalization of memory using hardware capabilities, a machine word that include a form of authority over the memory. Cerise is a program logic built on top of the Iris separation logic framework, and is able to prove strong properties of capability machine, e.g., the safety of a stack-based calling convention. In particular, it can verify programs involving interactions between known code and unknown, arbitrary code. Because real-world capability machines are complex, Cerise uses a model of a simplified single-core capability machine, with a small set of instructions. In order to lift these simplifying instructions, we propose Concurrent Cerise, a program logic for multi-core capability machine, with a sequentially consistent memory model. In addition to the extension of the model, we show that reasoning about the security properties already defined in Cerise is orthogonal to the concurrent behaviors. We design different scenarios targeting different threats, involving concurrency and synchronization mechanism, and prove safety properties using Concurrent Cerise

19-09-2022: Liveness properties under weak memory

Speaker: Egor Namakonov

Time: 13:00-14:00

Location: Nygaard-395

Abstract: A lot of concurrent algorithms are expected to satisfy certain liveness properties - for example, each thread waiting for access to the critical section should eventually obtain it. Usually, the finiteness of such waiting can be derived from the fact that each thread is eventually ordered for execution. But these arguments usually imply that the shared memory is represented simply as an array of values. This is not the case for modern programming languages and CPU architectures which rely on more complicated memory structures designed for efficient execution. During the talk, we’ll see what is required from a shared memory implementation to support usual liveness arguments. We’ll overview a few formalisms, unify them and use the unified definition to prove the termination and progress properties of multiple lock implementations. The talk is based on the “Making Weak Memory Models Fair” paper written by Ori Lahav, Jonas Oberhauser, Anton Podkopaev, Viktor Vafeiadis, and me.

27-06-2022: The Essence of Generalised Algebraic Data Types

Speaker: Sergei Stepanenko

Time: 13:30-14:00

Location: Ada-333

Abstract: Since their introduction twenty years ago, Generalised Algebraic Data Types, commonly referred to as GADTs, have become a staple of modern functional programming languages. First introduced as an extension of Glasgow Haskell Compiler, they were since adopted by OCaml, Scala and many other programming languages, due to their ability to establish more precise specifications for algebraic type constructors. These implementations, and the attendant difficulties, have also resulted in a rich literature that tackles the problems of type inference in the languages with ML-style polymorphism and GADTs. However, one feature that remains somewhat understudied is the semantics of GADTs and the nature and expressivity of these types. In this work, we intend to shed more light on these aspects of GADTs by introducing what we believe to be the first calculus that does not rely on the notion of a datatype constructor to express GADTs, study soundness and expressive power of the calculus, as well as provide some interesting and difficult open problems.

27-06-2022: High-assurance synthesis of cryptographic primitives - The BLS12 pairing groups

Speaker: Rasmus Holdsbjerg-Larsen

Time: 13:00-13:30

Location: Ada-333

Abstract: I will present our formal verification project, in which we develop implementations of the pairing groups used in the BLS12 digital signature scheme. By means of interactive theorem proving we provide formal guarantees of arithmetic and security properties of functions written in a low-level language, ExprImp, embedded in Coq. I will discuss benefits and drawbacks of our approach, as well as how we reason about stateful code making use of loops and function calls.

20-06-2022: Formalising Decentralised Exchanges in Coq

Speaker: Eske Nielsen

Time: 14:00-15:00

Location: Ada-333

Abstract: 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. In order 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.

20-06-2022: Type theory for critical applications: cryptography and smart contracts

Speaker: Bas Spitters

Time: 13:00-14:00

Location: Ada-333

Abstract: I will give a general overview of the work we have been doing with my group on using type theory for smart contracts and high assurance cryptography. For example, in the ConCert and SSProve frameworks

13-06-2022: A Flexible Multimodal Proof Assistant

Speaker: Philipp Stassen

Time: 13:00-13:30

Location: Ada-333

Abstract: 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, a general modal type theory which can internalize arbitrary collections of (dependent) right adjoints. These modalities are specified by mode theories, 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.

23-05-2022: Optimizing Relational Symbolic Execution over Cryptographic Code

Speaker: Bastien Rousseau

Time: 13:00-14:00

Location: Nygaard-295

Abstract: The constant-time property is a cryptographic property efficient to counter-measure timing attacks, a side-channel attack. Yet, constant-time programming is complex and is not always preserved by the compiler, therefore source code analysis is not sufficient. A solution is to analyze constant-time at binary level. Current state-of-the-art tools as Relational Symbolic Execution suffer of scaling issues at binary level. We propose an optimization of Relational Symbolic Execution which allows to spare SMT-solver calls for cryptographic code, and a prototype implementation on the top of Binsec/Rel. Our optimization, named RelABV, performs the analysis of AES (2 rounds) in less than 1 second, resulting in ×2100 speedup compared to Binsec/Rel, and successfully analyzes the AES (14 rounds) when Binsec/Rel failed after 1 hour.

25-04-2022: A Separation Logic for Communicating Virtual Machines

Speaker: Zongyuan Liu

Time: 13:00-14:00

Location: Nygaard-295

Abstract: A hypervisor is a piece of software that allows one host machine to support multiple guest virtual machines (VMs). Hypervisors are used extensively for virtualization in cloud computing and more. A hypervisor ensures that each VM runs as if on bare metal, and at the same time provides isolation, to separate untrusted code from security-critical code. We study the Hafnium hypervisor initially developed at Google. Hafnium implements hypercalls for communication among VMs, both via memory sharing and via message passing, following the FF-A specification of ARM, and Hafnium is claimed to provide memory isolation for those parts of the memory that are not shared via communication. We present an operational semantics which models the essential behavior of Hafnium, with fairly realistic hypercall interfaces. We further develop a program logic for modular formal verification of client VM programs that can communicate with other VMs via hypercalls, and a logical relation that captures the extent to which unknown code running on a VM is isolated from other VMs. Using the program logic and the logical relation, we reason about known VM programs that interact with VMs running arbitrary unknown code, and show robust safety: no matter what the unknown code does, it cannot violate specifications proved for the known code. This captures key aspects of the desired memory isolation properties of the hypervisor. All of the work has been mechanized using the Iris separation logic framework in Coq.

Joint work with Sergei Stepanenko, Aslan Askarov, Jean Pichon-Pharabod, Amin Timany, Lars Birkedal.

(It is a practice of the 20-minute talk for the Iris Workshop.)

04-04-2022: Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities

Speaker: Aina Linn Georges

Time: 13:00-14:00

Location: Ada-333

Abstract: Capability machines are a type of CPUs that support fine-grained privilege separation using capabilities, memory pointers that include forms of authority. So far, formal models of capability machines and associated calling conventions have focused on establishing two forms of stack safety properties, namely local state encapsulation and well-bracketed control flow. In this joint work with Alix Trieu and Lars Birkedal, we present a novel kind of directed capability and show how to use them to make an earlier suggested calling convention more efficient. We define unary and binary logical relations, expressive enough to reason about temporal stack safety (in addition to local state encapsulation and well-bracketed control flow). We use these logical relations to verify concrete examples, all mechanised in Iris.

14-03-22: Adiar: Binary Decision Diagrams in External Memory

Speaker: Steffan Sølvsten

Time: 13:00-14:00

Location: Nygaard-295

Abstract: Binary Decision Diagrams (BDDs) is a data structure widely used in the field of verification; especially within symbolic model checkers where they can heavily compress the representation of a model. Yet, since usual implementations of BDDs use recursion they heavily suffer from cache-misses and so only work until they grow bigger than the computer’s available main memory.

We apply the time-forwarding processing technique to the domain of BDDs with which we obtain an I/O-efficient variant of this data structure. These algorithms are implemented in our new a BDD package named Adiar. Due to the design of these algorithms Adiar is able to efficiently manipulate BDDs that outgrow main memory and so surpasses the limits of conventional BDD implementations.

At the seminar, I will present Adiar as I plan to do Thursday morning at the TACAS 22 conference. After these 12-15 minutes I will, based on your interests, present other key results we obtained in the past year and sketch our current and future plans for this project.

This work is co-authored with Jaco van de Pol, Anna Blume Jakobsen, and Mathias Weller Berg Thomasen.

21-02-22: A DSL of Combinators for Vellvm

Speaker: Bastien Rousseau

Time: 13:00-14:00

Location: Ada-333

Abstract: Vellvm is a formalization in the Coq proof assistant of the LLVM IR. As such, it is used to prove correct compilation passes, front-ends in particular. While reasoning semantically about generated code is a complex task per se, a significant overhead is entailed simply to ensure that the produced code is well-formed. In particular, LLVM IR requires that the labels of the blocks of code constituting the CFG be unique. To simplify the code generation in Vellvm and optimizations on the control flow graph, we present a design-specific language, CFLang, which ensures by construction the well-formedness of the generated graph. To guarantee the usability of these combinators in the context of verified compilation performed by equational reasoning — as is done in Vellvm —, we provide for each combinator their characteristic semantic equation. Finally, we illustrate the usability of our DSL by writing a compiler from IMP to VIR and validate the well-formedness of the generated code as well as its correctness.