Bruno Blanchet (INRIA Paris)
Slides - Link to paper
Title : The security protocol verifier ProVerif and its major recent improvements
Abstract : ProVerif is a widely used automatic security protocol verifier that relies on symbolic model of cryptography. It can prove various security properties (secrecy, correspondences, some equivalences) for an unbounded number of sessions, as well as find attacks. In this talk, we will present an overview of ProVerif and its recent improvements. These improvements are twofold. First, we extended ProVerif with lemmas, axioms, proofs by induction, natural numbers, and temporal queries. These features not only extend the scope of ProVerif, but can also be used to improve its precision (that is, avoid false attacks) and make it terminate more often. Second, we reworked and optimized many of the algorithms used in ProVerif (generation of clauses, resolution, subsumption, ...), resulting in impressive speed-ups on large examples. These improvements are joint work with Vincent Cheval and Véronique Cortier, to appear at IEEE Security and Privacy 2022.
Sandrine Blazy (IRISA, Rennes)
Slides
Title : Semantic preservation of constant-time policies during compilation
Abstract : A formally verified compiler is a compiler that comes with a machine-checked proof that no bug is introduced during compilation. This correctness property states that the compiler preserves the semantics of programs. Formally verified compilers guarantee the absence of correctness bugs, but do not protect against other classes of bugs, such as security bugs. This limitation partly arises from the traditional form of stating compiler correctness as preservation of semantics that do not capture non-functional properties such as security. Moreover, proof techniques for compiler correctness do not immediately apply to secure compilation, and need to be extended accordingly.
This talk will address the challenges of defining and preserving security policies for timing side-channel leakages during compilation, where a program is secure when observing its leakage during execution does not reveal any information about secrets. Two policies will be studied, from the specific angle of turning an existing formally-verified compiler into a formally-verified secure compiler: the popular cryptographic constant-time policy (which is widely used in cryptographic libraries to protect against timing and cache attacks), and the the constant-resource policy, a relaxation of the previous policy which is used is some cryptographic implementations.
This is a joint work with Gilles Barthe, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie and Alix Trieu.
Pierre-Yves Strub (Meta, France)
Title : EasyPQC: Verifying Post-Quantum Cryptography
Abstract : EasyCrypt is a formal verification tool used for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical attackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this talk, I will present a natural extension of the EasyCrypt core logics that permits capturing a wide class of post-quantum cryptography proofs. Leveraging this result, we implemented EasyPQC, an extension of EasyCrypt for post-quantum security proofs, and used EasyPQC to verify post-quantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption.
Aurélien Francillon (EURECOM)
Slides
Title : Symbolic execution by compiling symbolic handling into binaries with SymCC and SymQEMU
Abstract : Symbolic execution has the potential to make software more secure by significantly improving automated vulnerability search. Its principled reasoning can automatically explore parts of the program under test that would otherwise be hard to reach. However, many current implementations face challenges in scalability and usability: The power of symbolic execution comes at a cost. In this talk, we present the benefits of embedding symbolic handling into compiled programs instead of symbolically interpreting a higher-level representation of the program under test. Using this approach, we develop a compiler-based symbolic executor (SymCC) and show that it indeed achieves high execution speed in comparison with state-of-the-art systems. Since the compiler is limited to scenarios where source code of the program under test is available, we then design and implement a complementary solution for symbolic execution of binaries (SymQEMU); it uses the same basic idea of embedding symbolic execution into fast machine code but combines the approach with binary translation to handle the challenges of binary-only analysis. Both systems, the compiler-based symbolic executor as well as the binary translator, put a strong focus on ease of use with the goal of emphasizing that symbolic execution can benefit software developers and analysts in various fields.
Loading... 
