LogSem Seminar talks in 2022


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.