Antoine Delignat-Lavaud (Microsoft Research Cambridge)
Formal verification tools and automated theorem provers are commonly used to prove the correctness of programs with respect to some logical specification. While useful, correctness properties are typically not sufficient to reason about the security of a program – for instance, a login function that checks that the input password is equal to the input username is insecure even when correctly specified and implemented. The goal of this lecture is to show how critical security properties such as confidentiality, integrity, and authentication can be modeled and verified in F*. Our main application, developed by the Everest team at Microsoft Research and Inria, is the security modeling and verification of transport layer security (TLS), a cryptographic communication protocol widely used to secure Internet traffic. To this end, we will introduce cryptographic idealization, the main technique we use to model the security of cryptographic primitives, and illustrate it with several small applications. We will also explore the challenges of extracting efficient implementations out of security-verified programs, such as the erasure of the modeling state, or avoiding the introduction of side-channels in the extraction process. To conclude, we will demonstrate the integration of our verified components in complex, real-world applications such as web servers, browsers, and operating systems.
Slides (soon) available from the F* course page.
Matthias Heizmann (University of Freiburg)
In this talk, we will see the approach to automatic software verification that is implemented in the Ultimate Automizer tool. The approach is based on a new view to programs. In this new view, the focus lies not on program states, instead the focus lies on sequences of statements, which we call traces. We view a program as an automaton whose alphabet consists of the program’s statements. Hence, each program defines a set of traces and we can apply automata-theoretic operations to programs. Ultimate Automizer uses this connection between programs and sets of traces to decompose a program, to prove correctness of the components, and to compose these correctness proofs to a correctness proof for the program.
Gustavo Petri (IRIF, Univ. Paris Diderot)
In this talk I will address the problem of verifying program invariants for Commutative Replicated Data Types (CRDTs). I will firstly introduce CRDTs, whose implementations generally come in two flavors: operation-based and state-based. I will show a few examples, and then I will address the invariant verification problem for both operation- and state-based implementations. Time permitting, I will demo some tools to automate this process.
Philipp Rümmer (Uppsala University)