more slides

workshop-2024/schedule/schedule.html

@@ -14,6 +14,7 @@ <h3>Monday (3 June)</h3>
 </li>
 <li>11:30-12:00:  Travis Hance (Carnegie Mellon University)</a>: Verifying Rust code with ghost state and invariants
 <a href="#TravisHance" data-bs-toggle="collapse">[abstract]</a>
+<a href="slides/hance.pdf">[slides]</a>
 <div id="TravisHance" class="collapse"><div class="abstract">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.</div></div>
 </li>
 <li>12:00-12:30:  Aina Linn Georges (MPI-SWS)</a>: Formalizing Jane Street's modal OCaml

workshop-2024/schedule/speakers.csv

@@ -5,7 +5,7 @@ talk_time,raw_html,Name Tag,Affiliation,slides,title,abstract
 2024-06-05 12:00-12:30,,Markus Larsen,IT University of Copenhagen,larsen.pdf,Mechanizing state separation for modular cryptographic proofs,"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."
 2024-06-05 11:00-11:30,,Justus Fasse,KU Leuven,fasse.pdf,Block on! (WIP),"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."
 2024-06-05 09:30-10:30,<strong>Invited talk:</strong>,Guido Martínez,Microsoft Research,martinez.pdf,The Pulse programming language,"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."
-2024-06-03 11:30-12:00,,Travis Hance,Carnegie Mellon University,,Verifying Rust code with ghost state and invariants,"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."
+2024-06-03 11:30-12:00,,Travis Hance,Carnegie Mellon University,hance.pdf,Verifying Rust code with ghost state and invariants,"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."
 2024-06-03 16:00-16:30,,Peter Sewell,University of Cambridge,,Open problems from system software verification,"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."
 2024-06-04 11:30-12:00,,Philipp Haselwarter,Aarhus University,haselwarter.pdf,Compositional Reasoning about Expected Costs for Higher-Order Probabilistic Programs,"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."
 2024-06-05 14:30-15:00,,Simon Spies,MPI-SWS,https://people.mpi-sws.org/~spies/assets/papers/slides-satisfiable.pdf,Making Adequacy of Iris Satisfying,"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."