Diagrammatic notations for interactive theorem provingShardul Chiplunkar, EPFL
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.
Making the Boogie verifier foundationalGaurav Parthasarathy, ETH Zürich
Practical formal verification at USINatasha Sharygina & Carlo A. Furia, USI
SMT-streamlined software verificationNatasha Sharygina, USI
Practical formal methods: are we there yet?Carlo A. Furia, USI
Type-Checking CRDT Convergence with PropelGeorge Zakhour, University of St Gallen
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.
Track A: Case studies
Using separation logic for proving security protocol implementations secureLinard Arquint, ETH Zürich
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 ComputingLennard Gäher, IBM Research Zurich, and Wojciech Ozga, IBM Research Zurich
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.
FV-ACTUS: Formally Verifiable Financial Contracts.Mark Greenslade, Casper Association
Track B: Low-level tools and techniques
Golem and OpenSMTKonstantin Britikov, Universita della Svizzera Italiana
Quantifying and avoiding path explosion in symbolic executionSolal Pirelli, EPFL
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 VerificationChengyu Zhang, ETH Zürich
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
Leveraging Rust Types for Program SynthesisJonas Fiala, ETH Zürich
How to verify a spinlock with Iris (demo)Ralf Jung, ETH Zürich
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 treesMax Vistrup, ETH Zürich
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
Formal Foundations of the Viper Verification InfrastructureThibault Dardinier, ETH Zürich
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 LithiumMichael Sammler, ETH Zürich
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.
Mutable value semanticsDimi Racordon, LAMP, EPFL
Tutorials and breakouts
Track A: Tutorials
LISA Is Sets AutomatedSimon Guilloud, EPFL
Verifying Functional Properties at the level of JVM BytecodeMarco Paganoni, Università della Svizzera italiana
Prusti: Deductive Verification for RustFederico Poli, ETH Zürich
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
Topics to be determined during the lunch break, in small groups (4-6 people)