Security verification and cryptographic modelling in F*
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.
Traces, interpolants, and automata : Ultimate Automizer’s approach to software verification
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.
Slides: PDF
Invariant Verification for CRDTs
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.
Slides here.
SMT, Strings, and Security
Philipp Rümmer (Uppsala University)
The recent years have seen a wealth of research on string solvers, i.e., SMT solvers that can efficiently check satisfiability of quantifier-free formulas over a background theory of strings and regular expressions. String solvers can be applied in a variety of verification approaches, for instance in software model checking to take care of implication and path feasibility checks; the most widespread adoption has occurred in the area of security analysis for languages like JavaScript and PHP, for instance to discover information leaks or vulnerability to injection attacks. To process constraints from those domains, it is necessary for string solvers to handle a delicate combination of (theoretically and practically) highly challenging operations: concatenation in word equations, to model assignments in programs; regular expressions or context-free grammars, to model properties or attack patterns; string length, to express string manipulation in programs; transduction, to express sanitisation, escape operations, and replacement operations in strings; and others. The lecture will explain properties of the theory, existing and/or successful solver architectures, and also outline the application of string solvers for security properties.
Slides: PDF