Swiss Verification Day 2024

, EPFL Microcity, Neuchâtel

Purpose

Bring together the Swiss formal methods and verification community, especially students and post-docs, for a day of informal talks.

Call for participation

Are you a Swiss-based academic or industrial researcher active in the fields of formal methods, verification, and program proofs? Join us for the first Swiss Verification Day workshop, to be held January 10, 2024 on EPFL's Microcity campus, Neuchâtel!

We are soliciting short and informal presentations, tool demos, tutorials, and small-group discussion topics, with a focus on in-progress work and on topics susceptible to foster discussion and collaboration.

Practicalities

Location

EPFL Microcity, Rue de la Maladière 71, CH-2000 Neuchâtel

Time

(coffee available from , welcome and introductions start at , talks start at )

Rooms

Building reception
MC B1 94.25
(upstairs from southern entrance on ground floor, or directly from eastern entrance on first floor)
Auditorium
MC A1 272
Classrooms
MC B1 273 (34 seats)
MC B1 283 (26 seats)
MC B1 303 (56 seats)

Getting there

By train
Get off at Neuchâtel, then either walk 13-15 minutes or take the funicular + bus to Neuchâtel, Microcity
By car
No on-site visitor parking: park at Centre Commercial de la Maladière, then walk 2 minutes.
Access map

Food

Breakfast
We plan to cater coffee and light snacks.
Lunch
EPFL Microcity has a cafeteria on-site (~15-20F per person), and plenty of shops nearby. Locals swear by A l'Emportée for cheap sandwiches, Happy Bowl for salads, and Vio for stir-fry. The Coop also has a restaurant and good take-out options for most special diets.
Dinner
The plan is to break up into small groups. Here are some options, in order of proximity to Microcity:

Program


Arrival, coffee

Hallway B1 94.25

Welcome, introductions

Auditorium A1 272

Keynotes

Auditorium A1 272

Diagrammatic notations for interactive theorem proving

Abstract

Diagrams are ubiquitous in the development and presentation of proofs, yet surprisingly uncommon in computerized mathematics. Instead, authors and developers rely almost exclusively on line-oriented notations (textual abbreviations and symbols). How might we enrich interactive theorem provers with on-the-fly visual aids that are just as usable? We sketch an answer to this question by identifying a key challenge: designing declarative languages for composable diagram templates, that provide good-looking implementations of common patterns, and allow for rapid prototyping of diagrams that remain stable across transformations and proof steps.

Type-Checking CRDT Convergence with Propel

Abstract

Conflict-Free Replicated Data Types (CRDTs) are a recent approach for keeping replicated data consistent while guaranteeing the absence of conflicts among replicas. For correct operation, CRDTs rely on a merge function that is commutative, associative and idempotent. Ensuring that such algebraic properties are satisfied by implementations, however, is left to the programmer, resulting in a process that is complex and error-prone. While techniques based on testing, automatic verification of a model, and mechanized or handwritten proofs are available, we lack an approach that is able to verify such properties on concrete CRDT implementations.

In this paper, we present Propel, a programming language with a type system that captures the algebraic properties required by a correct CRDT implementation. The Propel type system deduces such properties by case analysis and induction: sum types guide the case analysis and algebraic properties in function types enable induction for free. Propel’s key feature is its capacity to reason about algebraic properties (a) in terms of rewrite rules and (b) to derive the equality or inequality of expressions from the properties. We provide an implementation of Propel as a Scala embedding, we implement several CRDTs, verify them with Propel and compare the verification process with four state-of-the-art verification tools. Our evaluation shows that Propel is able to automatically deduce the properties that are relevant for common CRDT implementations found in open-source libraries even in cases in which competitors timeout.


Lunch break


Research talks

Track A: Case studies

Auditorium A1 272
Using separation logic for proving security protocol implementations secure
Abstract

Security protocols are essential building blocks of modern IT systems. Subtle flaws in their design or implementation may compromise the security of entire systems. It is, thus, important to prove the absence of such flaws through formal verification. Much existing work focuses on the verification of protocol models, which is not sufficient to show that their implementations are actually secure. Verification techniques for protocol implementations (e.g., via code generation or model extraction) typically impose severe restrictions on the used programming language and code design, which may lead to sub-optimal implementations.

In this talk, we present a methodology for the modular verification of strong security properties directly on the level of protocol implementations. By leveraging separation logic, we not only support a wide range of implementations and programming languages but, to the best of our knowledge, we are the first to modularly prove injective agreement, i.e., the absence of replay attacks. We evaluate our methodology on Go and C implementations of several security protocols, including the WireGuard VPN protocol for which we prove forward secrecy and injective agreement.

Towards The Formal Verification of Security Monitor For Confidential Computing
Abstract

This talk discusses our efforts on building an open-source, formally proven confidential computing framework called Assured Confidential Execution (ACE). We explain our methodology that leverages the Rust programming language and RefinedRust for formal verification. We present a demo and discuss challenges when implementing and proving low-level systems in Rust.

Track B: Low-level tools and techniques

Classroom B1 303
Quantifying and avoiding path explosion in symbolic execution
Abstract

Symbolic execution runs into the _path explosion_ problem: there are typically too many paths to exhaustively enumerate in reasonable time. Thus, bug-finding tools try to guide symbolic execution towards interesting paths, and verification tools try to handle complex code separately. However, the lack of a formal definition of "path explosion" makes it difficult to evaluate the efficiency of proposed techniques. In this talk, I'll explain why previous metrics don't work, present requirements for a metric, propose a new metric based on state redundancy, revisit previous work in light of this metric, and suggest a way forward to avoid path explosion in common loops.

Solidifying the Foundations for Software Verification
Abstract

Software verification lies at the heart of building reliable software. Consequently, the dependability of verification tools is pivotal for software reliability. It is thus critical to develop effective methodologies and practical tools to help solidify the foundational verification tools. In this talk, I will present effective techniques and extensive effort for uncovering numerous bugs in modern SMT solvers and software verification tools. The talk will focus on both the theoretical and practical challenges of solidifying the verification foundations and introduce the latest advances.

Track C: Logic

Classroom B1 283
How to verify a spinlock with Iris (demo)
Abstract

In this demo I will go through all the steps involved in verifying a simple synchronization primitive with Iris in Coq: a spin lock. If time permits, we will also go through the verification of an example client using the spinlock.

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.

Track D: Tool design

Classroom B1 273
Formal Foundations of the Viper Verification Infrastructure
Abstract

The Viper verification infrastructure provides an architecture on which new automatic verification tools and prototypes can be developed simply and quickly. Viper comprises an intermediate verification language (the Viper language) based on separation logic, as well as automatic verifiers for the language. In this talk, I will first give an overview of Viper. I will then present and illustrate the use of inhale and exhale, two key verification primitives provided by Viper. Finally, I will describe our ongoing work to give formal foundations to Viper, which includes proving that the successful verification of a Viper program corresponds to a valid proof in separation logic.

Building automated and foundational verification tools with Lithium
Abstract

This talk presents Lithium, a domain-specific language for building separation-logic based verification tools in Coq. Concretely, Lithium has been used to automate reasoning about a refinement and ownership type system for C (RefinedC), a separation logic for a realistic model of Arm and RISC-V assembly (Islaris), and a version of the Rust type system enriched with refinement types (RefinedRust). This talk will demonstrate how one can build a verification tool using Lithium on the example of a small language.


Coffee break

Hallway B1 94.25

Tutorials and breakouts

Track A: Tutorials

Auditorium A1 272
Prusti: Deductive Verification for Rust
Abstract

In this talk I will introduce and give a demo of Prusti, our automated program verifier for Rust software. In Prusti, we exploit Rust's type system to greatly simplify the specification and verification of Rust programs. In particular, we lift the ownership and framing-​related information required for a separation logic proof from the type-​checking of the program performed by the Rust compiler. User specifications are automatically interwoven, and focus on the desired functional guarantees expressed in a syntax similar to that of Rust program expressions.

Track B: Breakouts

Classrooms B1 273, B1 283, B1 303.

Topics to be determined during the lunch break, in small groups (4-6 people)


Wrap-up: Apéro

Hallway B1 94.25

Dinner

Organization

Access map