# 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.