Swiss Verification Day 2024

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.

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.

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.

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.

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.

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.

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.

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.

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.