Iris Workshop 2024

The fourth edition of the Iris workshop will be held in Zurich and it will be focused on Iris-related research to allow for in-depth talks and discussions. There will be a three-day long program with talks from Monday 3 June until Wednesday 5 June. Participants are encouraged to stay 1-2 days longer if they can, for more informal discussions and interaction.

Program

Monday (3 June)

• 09:00-09:30: Coffee
• 09:30-10:30: Invited talk: Christopher Pulte (University of Cambridge): CN: Verifying Systems C Code with Separation-Logic Refinement Types [abstract] [slides]
  Despite significant progress in the verification of hypervisors, operating systems, and compilers, and in verification tooling, there exists a wide gap between the approaches used in verification projects and conventional development of systems software. We see two main challenges in bringing these closer together: verification handling the complexity of code and semantics of conventional systems software, and verification usability. CN is an experiment in verification tool design aimed at addressing some aspects of both: a separation-logic refinement type system for C systems software, aimed at predictable proof automation, based on a realistic semantics of ISO C. CN reduces refinement typing to decidable SMT solving (with some user assistance), uses first-class resource types to support pointer aliasing and pointer arithmetic, and uses a novel syntactic restriction of ghost variables in specifications to guarantee their successful inference. In ongoing work we are applying CN to verifying components of Google's pKVM hypervisor for Android.
• 10:30-11:00: Coffee, Snacks
• 11:00-11:30: Maxime Legoupil (Aarhus University): Iris-MSWasm: elucidating and mechanising the security invariants of Memory-Safe WebAssembly [abstract] [slides]
  WebAssembly offers coarse-grained encapsulation guarantees via its module system, but does not support fine-grained sharing of its linear memory. MSWasm is a recent proposal which extends WebAssembly with fine-grained memory sharing via handles, a type of capability that guarantee spatial and temporal safety, and thus enables an expressive yet safe style of programming with flexible sharing. In this talk, I explain how we formally validated the pen-and-paper design of MSWasm. To do so, we first defined MSWasmCert, a mechanisation of MSWasm that makes it a fully-defined, conservative extension of WebAssembly 1.0, including the module system. We then developped Iris-MSWasm, a foundational reasoning framework for MSWasm composed of a separation logic to reason about know code, and a logical relation to reason about unknown, potentially adversarial code. Iris-MSWasm thereby makes explicit a key aspect of the implicit universal contract of MSWasm: robust capability safety. We have applied Iris-MSWasm to reason about key use cases of handles, in which the effect of calling an unknown function is bounded by robust capability safety. Iris-MSWasm thus works as a framework to prove complex security properties of MSWasm programs, and provides a foundation to evaluate the language-level guarantees of MSWasm.
• 11:30-12:00: Travis Hance (Carnegie Mellon University): Verifying Rust code with ghost state and invariants [abstract] [slides]
  Recently, there has been significant interest in verifying safe Rust code by taking advantage of Rust’s type system to produce efficient encodings into first-order logic (FOL). However, it is less obvious how to do the same for unsafe code. On the other hand, there has been plenty of work on verifying unsafe Rust code using Iris and other separation logic frameworks. In particular, separation logic features like invariants and resource algebra-based ghost state have proved invaluable for nontrivial unsafe code. Is it possible to use these ideas to verify unsafe code while still utilizing efficient, highly-abstracted FOL encodings? In order to do just that, our Rust verification tool Verus introduces special ‘primitive’ types that capture the power and flexibility of invariants and ghost state, making it possible to execute Iris-like proofs at a high level of abstraction. In this talk, I will explain how we embed these two fundamental concepts as primitive Verus types and how Rust’s type system can enhance them even further. I will explain how they can be used to verify nontrivial unsafe code, and I will summarize my ongoing work using Iris to validate the correctness of this embedding.
• 12:00-12:30: Aina Linn Georges (MPI-SWS): Formalizing Jane Street's modal OCaml [abstract]
  Jane Street has recently proposed a design that aims to bring Rust-style resource management to OCaml. The design features a collection of modes, that together allows users to express stack allocation, ownership tracking, and the safe use of mutable data structures in the presence of concurrency. In this talk, I will present the key ideas of the design, and discuss how we have verified it in Iris.
• 12:30-14:30: Lunch
• 14:30-15:30: Invited talk: Irene Yoon (Inria): Velliris: A Relational Program Logic for LLVM IR [abstract]
  This talk introduces Velliris, a relational separation logic for LLVM IR in Coq. The VIR formal semantics, using Interaction Trees (ITrees), provides a modular and executable semantics for LLVM IR. It is equipped with a relational program logic well-suited for control flow reasoning about possibly diverging programs. However, most LLVM IR transformation passes not only modify the control flow; their correctness also depends on invariants over state, using information derived either from analysis passes or user annotations. In such context, the pre-existing program logic of Interaction Trees falls short. In contrast, the Iris framework offers a flexible way to construct language-specific separation logics, which provide localized reasoning principles over state. Velliris merges these approaches, defining a relational program logic in Iris for the ITrees-defined VIR semantics. While typical Iris models build on small-step operational semantics, we define a new weakest-precondition model for stateful Interaction Trees to reconcile this approach. Moreover, we develop a robust theory over LLVM IR resources, providing a novel way of specifying LLVM IR’s attribute specifications, which record the compiler’s assumptions about function calls.
• 15:30-16:00: Coffee
• 16:00-16:30: Peter Sewell (University of Cambridge): Open problems from system software verification [abstract]
  In the last few years, a number of us have been looking at what it would take to prove correctness of critical systems, as developed and used in conventional industry. We're targetting Google's pKVM hypervisor, intended to protect sensitive resources and the Android kernel from each other, and the Arm Morello CHERI prototype architecture. There's been much progress (Arm semantics, AxSL, Islaris, CN, Refined C, VIP, etc.), but there are many really interesting open problems. This talk will give a quick introduction to some of them, ranging from the fundamental challenge of reasoning compositionally about intrinsically non-compositional semantics, to the engineering and human-interface challenges of making proof tools that let us develop and maintain substantial verifications. The pKVM verification project and Morello proofs are joint work with lots of people in Cambridge, Edinburgh, Aarhus, MPI-SWS, Radboud, and SNU.
• 16:30-17:00: Hai Dang (BedRock Systems Inc.): A Lightweight Framework for Decomposing Logical Atomicity of LTS Composition [abstract] [slides]
  Modern computer systems can be naturally modeled as a parallel composition of multiple concurrent processes communicating through events (e.g., as labeled transition systems or LTSes). At BedRock Systems, we prove that our virtualization stack implementation refines such an LTS composition model of a computer system (the specification). When using separation logic to decompose such a refinement proof, we need separation logic analogs of standard process calculi reasoning principles: while the separating conjunction can naturally reflect the parallel composition of states of constituent LTSes, reflecting the communication among those LTSes requires clever uses of invariants and more generally, logical atomicity (atomic updates in Iris). We have developed an Iris library called the refinement framework to provide separation logic decomposition along a parallel composition, process bi-simulation, and communication. We have applied our refinement framework in several large verification efforts including on a virtual machine monitor and virtual network switch.

Tuesday (4 June)

• 09:00-09:30: Coffee
• 09:30-10:30: Invited talk: Jonas Kastberg Hinrichsen (Aarhus University): Multris: Functional Verification of Multiparty Message Passing in Separation Logic [abstract] [slides]
  Message passing is an attractive concurrency paradigm due to its simplicity and expressiveness. Formal verification of message-passing programs has thus received a lot of attention. In particular, multiparty message passing---where communication between parties can depend on communication between others---exhibit intricate behaviours which benefits greatly from a formal interpretation. A prominent approach for verifying message-passing programs, is the discipline of session types, which is built around local protocols consisting of sequences of send (!𝜏) and receive (?𝜏) actions that specify what operations should be performed in what order on a channel. While session types have been used to guarantee desirable properties of multiparty systems such as memory safety and deadlock freedom through type checking, they do not guarantee functional correctness. In this talk I introduce Multris, a separation logic for verifying the functional correctness of programs that combine multiparty message-passing communication with shared-memory concurrency. The foundation of this work is a novel notion of multiparty protocol consistency, which guarantees safe communication among a set of parties, provided each party adheres to its prescribed protocol. To ensure the reliability of our work, we prove soundness of Multris w.r.t. a low-level channel semantics using the Iris framework in Coq, drawing inspirations from prior work on the Actris extension of Iris, for session type-based reasoning in separation logic.
• 10:30-11:00: Coffee, Snacks
• 11:00-11:30: Alejandro Aguirre (Aarhus University): Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs [abstract] [slides]
  Probabilistic programs often trade accuracy for efficiency, and are thus only correct up to some probability. It is important to obtain precise bounds for the probability of these errors happening, but existing approaches rely on simplifications that make the error bounds excessively coarse, or only apply to first-order programs. In this talk I will present Eris, a higher-order separation logic for reasoning about probabilities of errors in higher-order probabilistic programs. Our key novelty is the introduction of error credits, a separation logic resource that tracks a bound on the error probability of a program. By representing error bounds as a resource, we recover the benefits of separation logic, including compositionality, modularity, and dependency between errors and program terms, allowing for more precise specifications. Moreover, we enable novel reasoning principles such as expectation-preserving error composition, amortized error reasoning, and induction on the error.
• 11:30-12:00: Philipp Haselwarter (Aarhus University): Compositional Reasoning about Expected Costs for Higher-Order Probabilistic Programs [abstract] [slides]
  I will present Tachis, a higher-order separation logic to reason about the expected cost of probabilistic programs. Inspired by the uses of time credits for reasoning about the running time of deterministic programs, we introduce a novel notion of probabilistic cost credit. Probabilistic cost credits are a separation logic resource that can be used to pay for the cost of operations in programs, and that can be distributed across all possible branches of sampling instructions according to their weight, thus enabling us to reason about expected cost. The representation of cost credits as separation logic resources gives Tachis a great deal of flexibility and expressivity. In particular, it permits reasoning about amortized expected cost by storing excess credits as potential into data structures to pay for future operations. Tachis further supports a range of cost models, including running time and entropy usage. We showcase the versatility of this approach by applying our techniques to prove upper bounds on the expected cost of a variety of probabilistic algorithms and data structures, including randomized quicksort, hash tables, and meldable heaps.
• 12:00-12:30: Emanuele D’Osualdo (University of Konstanz): Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning [abstract]
  We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behaviour like *independence* and *conditioning*. The relational style of reasoning, on the other hand, naturally shines when the properties of interest *compare* the behaviour of similar programs (e.g. when proving differential privacy) managing to avoid having to characterize the output distributions of the individual programs. So far, the two styles of reasoning have largely remained separate in the many program logics designed for the deductive verification of probabilistic programs. In Bluebell, we unify these styles of reasoning through the introduction of a new modality called "joint conditioning" that can encode and illuminate the rich interaction between *conditional independence* and *relational liftings*; the two powerhouses from the two styles of reasoning.
• 12:30-14:00: Lunch
• 15:00-18:00: Excursion to the top of Uetliberg [details]
  This hill right next to the city lies at about 400m elevation above Zurich and provides a great panoramic view of the city, the lake, and the alps. Two options exist for getting up the hill: either a hike the entire way, or taking the S-Bahn followed by a short stroll for the last few meters. After enjoying the view with some drinks, we will have dinner at the restaurant Uto Staffel, just a few minutes walk from the top.
• 18:30-21:00: Dinner at Uto Staffel

Wednesday (5 June)

• 09:00-09:30: Coffee
• 09:30-10:30: Invited talk: Guido Martínez (Microsoft Research): The Pulse programming language [abstract] [slides]
  I will present Pulse, a new programming language based on dependent types and separation logic for verified imperative programming. Pulse is built over PulseCore, a fully verified separation logic implemented in F*. While Pulse programs elaborate to PulseCore definitions, working with PulseCore directly is not very convenient. For this reason, Pulse provides a full-fledged frontend with its own syntax, typing rules, and typechecker, all of which are embedded in F*. The typing judgment and typechecker are also verified to preserve the correctness of programs. Pulse programs can be run by extracting into OCaml, C or Rust (with different restrictions). I will also show how to verify some task-parallel programs with Pulse, and some (very) recent work in verified GPU kernel programming.
• 10:30-11:00: Coffee, Snacks
• 11:00-11:30: Justus Fasse (KU Leuven): Block on! (WIP) [abstract] [slides]
  Obligations are an established approach to prove deadlock-freedom of blocking programs: blocking threads justify their blocking by proving that another thread is obligated to unblock them eventually. Traditionally, the API of primitive locks enforces that lock acquisition burdens the acquiring thread with an obligation to release the lock. Blocked threads can therefore be certain that their blocking is justified by the thread holding the lock. Consequently the program is (globally) deadlock-free. We argue that blocking APIs need not fix their clients' usage patterns! In our approach, clients can create and destroy obligations freely. The specification of a blocking operation simply imposes a proof obligation on clients to show that while the operation is blocked, some thread holds a justifying obligation. That is, an obligation which is ordered below the obligations held by the blocked thread in the wait order. We present this client-empowering specification style in the context of primitive locks. Afterwards, we will discuss our ideas to apply these same ideas to the lower level futex API (i.e. primitive "compare-and-sleep" and wake operations). Finally, we will sketch how higher-level blocking constructs could be verified against this API.
• 11:30-12:00: Clément Allain (Inria Paris): Verifying Tail Modulo Cons using Relational Separation Logic [abstract] [slides]
  Tail-call optimization (TCO), a well-known optimization performed by many compilers for functional programming languages, optimizes tail calls by deallocating the stack frame of the caller before jumping to the callee. Tail-call optimization modulo constructors (TMC) improves upon TCO by also optimizing the situation where a function call is not a tail call because it is followed by the application of a constructor. A canonical example appears in the most natural implementation of the map function on lists. TMC has been implemented in the OCaml compiler by Frédéric Bour, Basile Clément and Gabriel Scherer. Based on this work, we have formalized and verified TMC for an untyped sequential calculus equipped with mutable heap cells. The correctness of the transformation is expressed as a termination-preserving behavioral program refinement. The proof relies on a relational separation logic that is constructed on top of Iris, drawing inspiration from Simuliris. An independent contribution is an extension of the Simuliris approach to define simulation relations that support different calling conventions.
• 12:00-12:30: Markus Larsen (IT University of Copenhagen): Mechanizing state separation for modular cryptographic proofs [abstract] [slides]
  The goal of this work has been to mechanize the security proofs of cryptographic algorithms. A security definition is expressed in terms of a game pair capturing the distinguishability between real and ideal functionality. A security proof is then expressed as a sequence of game hops in-between these games.  When mechanizing security proofs using modules (see Brzuska et al. work on state-separating proofs), which introduce sets of module-specific global state-variables, compositionality becomes an issue, because the two modules may inadvertently use the same state-variable names. Thus, state-variables must be renamed when composing modules as had already been observed. In my talk, I demonstrate how the theory of nominal sets can be used to solve this problem by introducing a notion of separated module composition, which ensures separation of state-variables by applying permutations of names. Separation is defined constructively, so that it can be easily expressed in a proof assistant, such as Coq, Lean, or Iris. I show, in particular, how alpha-equivalence implies perfect indistinguishability and how game-hopping through an intermediate module that uses extra state-variables does not complicate the formulation of security theorems.
• 12:30-14:30: Lunch
• 14:30-15:00: Simon Spies (MPI-SWS): Making Adequacy of Iris Satisfying [abstract] [slides]
  The adequacy theorem of Iris ensures that proofs about programs in Iris can be turned into meaningful statements about these programs in the Coq meta logic (i.e., outside of Iris). As such, it allows projects building on Iris to remove their custom Iris constructions (e.g., custom weakest preconditions, simulation relations, or logical relations)—and even Iris itself—from the trusted code base. Unfortunately, while adequacy is an essential part of Iris, it is one of the darker corners of Iris that users often shy away from. The reason is that, traditionally, adequacy is proven using one of several monolithic and somewhat inaccessible lemmas—making it challenging for novices to instantiate adequacy and for experts to adapt existing adequacy proofs. In this talk, I will present a different, more modular approach to proving adequacy, the "satisfiable"-approach. Instead of monolithic adequacy lemmas, it is based on a predicate called "satisfiable", which decomposes adequacy proofs into several, smaller proof steps—one modality at a time. The approach has already been applied in several Iris projects, but has so far eluded the spotlight. I will explain how it works and how others can use it to prove adequacy of their own, custom program logics.
• 15:00-15:30: Max Vistrup (ETH Zürich): Compositional program logics for interaction trees [abstract]
  While program logics have made tremendous progress in recent years, defining and formalizing a program logic for realistic programming languages such as Rust remains difficult. A major issue is the sheer scale of these languages, making even the precise formal definition of their operational semantics a challenge, let alone defining a program logic on top of these semantics and proving it sound. One proposal that has shown potency for large-scale formalization is that of ITrees, which allows the user to define the semantics in a compositional, modular way. However, while the Vellvm project with their LLVM formalization has demonstrated that ITrees scale up to large language formalizations, so far there has been no approach to obtain a program logic in the same compositional style. In this work, our goal is to define program logics over ITrees in Iris. We define these logics compositionally, allowing the user to build up their own logic out of custom components as well as general, reusable components. We also show how to treat concurrency in the context of ITrees, overcoming a long-standing limitation. One of our main theorems is an adequacy theorem that says that if we extend a program logic with concurrency and we prove a weakest precondition of a program in this extended logic, we get weakest preconditions of every interleaving in the original program logic. This lets us treat concurrency as just another reusable building block in our story of composing languages using ITrees.
• 15:30-16:00: Coffee
• 16:00-17:00: Session with the Iris maintainers

Thursday (6 June) – Friday (7 June)

• Discussion groups and meetings organized by attendees.

Location

The workshop will take place in the Alumni Pavillon next to the ETH main building. [map]
Leonhardstrasse 34
8092 Zurich, Switzerland

For the discussions on June 6 and June 7, we have reserved the following rooms in HG (the ETH main building):
E 33.1, E 33.3, E 33.5, F 26.1 (only on Thursday), F 26.3, F 26.5. ("E" rooms are on the ground floor, "F" rooms on the second floor.)

The workshop dinner will be held on Tuesday June 4 in Uto Staffel, Gratstrasse 6, 8143 Uetliberg. [map]

Organizers

• Ralf Jung (ETH Zurich, Switzerland)
• Michael Sammler (ETH Zurich, Switzerland)
• Robbert Krebbers (Radboud University Nijmegen, The Netherlands)

Registration

For registration, please contact the organizers.

Participation is free of charge. The workshop is generously sponsored by ETH Zurich.

Practical information

Accomodation

• Royal Hotel Zurich (walking distance to ETH, 2 tram stops to downtown Zurich/train station)
• Fred Hotel Zürich Leonhardstrasse (walking distance to ETH, 2 tram stops to downtown Zurich/train station)
• Hotel St. Josef (walking distance to ETH and Zurich downtown, 1 tram stop from train station)
• Ruby's Mimi Hotel (3 tram stops to ETH, walking distance to downtown Zurich/train station, new boutique hotel)
• Hotel Rigihof (2 tram stops to ETH, 5 tram stops to downtown Zurich/train station)
• Hotel Bristol (walking distance or 1 tram stop to ETH, 2 tramstops to downtown/train station)
• Hotel Felix (walking distance to ETH and Zurich downtown, 1 tram stop from train station)
• Hotel Zürcherhof (2 tram stops to ETH, downtown Zurich)
• Hotel Rex (3 tram stops to ETH, 5 tramstops from downtown Zurich)

• Hotel Crowne Plaza
• Hotel Easy West
• Hotel Ibis Zurich City West and Hotel Ibis Budget
• Hotel Züri by Fassbind

Information for other well-​priced hotels in the city of Zurich, in all categories, is also available at the preceding link and from many other websites.

Getting to Zurich

Zurich is located in the heart of Europe and well-connected by train and plane.

• There are trains to Zurich HB from many cities throughout Europe.
• Zurich Airport offers many international connections, and is only a 10min train ride away from the central train station.
• Zurich is also easily reachable by car, but parking in the city is expensive (up to 45CHF per day at the parking garage). A cheaper alternative is to park your car outside the city at one of the many P+R parking spaces around Zurich (e.g. Tiefenbrunnen or Stettbach), and then cover the last mile by train. We recommend using public transport instead.

Getting to ETH

ETH Zurich is located in the center of the city and easy to reach.

From Zurich HB (main station), follow the signs towards "Bahnhofplatz" or "Bahnhofstrasse" until you are above ground and outside the station. Then take either:

• Tram no. 6 (direction Zoo) from tram stop "Bahnhofstrasse/HB", exit at tram stop "ETH/Universitätsspital" (right next to the ETH main building). Journey time: about 8 minutes.
• Tram no. 10 (direction Flughafen or Bahnhof Oerlikon) from tram stop "Bahnhofplatz/HB", exit at tram stop "ETH/Universitätsspital". Journey time: about 8 minutes.

Note that there are many tram stops around the main station. The links above show where exactly the two relevant stops are located. There are vending machines for tram tickets at each tram stop; they accept coins (with change, but no bills!) and credit cards. You can get a "Kurzstrecke" (short trip) ticket, which costs 2.80 CHF.

From Zurich airport: You can either take the tram to ETH or a train to the city center (Zurich HB):

• Tram no. 10 from tram stop "Zürich Flughafen" (direction Bahnhofplatz/HB) to tram stop "ETH/Universitätsspital". The tram operates daily from 6 a.m to 11 p.m. with trams departing every 7 to 15 minutes. Journey time: 30 minutes
• S-Bahn/Train: Follow the signs "Bahn/Railway" to the ticket counters and/or ticket machines. You will find instructions in English on the ticket machines. Get a ticket for "Zürich City" (make sure that the display shows "1 Std" = 1 hour). The machines accept coins, bills as well as credit cards and give change (the ticket costs 6.40 CHF). The ticket is valid for 1 hour for all trains to Zürich as well as for trams and buses in the city (streetcar, Strassenbahn). Take the escalator down to the platforms. Trains to the city center leave approx. every 10 minutes and it takes about 10 minutes to reach the main station. From there take tram no. 6 or no. 10 as described above.

What to do in Zurich

The tourist information website provides lots of information about what to do in Zurich.