Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct:
                  https://webconf.math.cnrs.fr/b/fra-ryy-fjn

			     S É M I N A I R E

                   ______                __    _
                  / ____/___ _____ ___  / /_  (_)_  ______ ___
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                          Salle Lions 1, bâtiment C

                          Lundi 27 septembre, 10h30

                                    ------
                                    Son Ho
                                    ------

                                 Inria Paris

                ==============================================
                Noise∗: A Library of Verified High-Performance
                   Secure Channel Protocol Implementations
                ==============================================

Correctly implementing cryptographic protocols like TLS is an error-prone
task, where bugs can lead to massive security issues. Those vulnerabilities
call for the application of program verification, but the wide number of use
cases and the corresponding variety of specialized protocols makes their
verification a daunting work.

In this talk, I will introduce Noise∗, a verified implementation of a compiler
for the Noise protocol framework. Noise is a framework which defines a
succinct notation and execution framework for a large class of 59+ secure
protocols, some of which are used in popular applications such as WhatsApp and
WireGuard. The Noise∗ compiler takes *any* Noise protocol, and produces an
optimized C implementation with extensive correctness and security guarantees.

To this end, we formalize the complete Noise stack in F∗, from the low-level
cryptographic library to a high-level API. We write our compiler also in F∗,
prove that it meets our formal specification once and for all, and then
specialize it on-demand for any given Noise protocol, relying on a novel
technique called hybrid embedding.

We thus establish functional correctness, memory safety and a form of
side-channel resistance for the generated C code for each Noise protocol. We
propagate these guarantees to the high-level API, using defensive dynamic
checks to prevent incorrect uses of the protocol.

Finally, we formally state and prove the security of our Noise code, by
building on a symbolic model of cryptography in F*, and formally link
high-level API security goals stated in terms of security levels to low-level
cryptographic guarantees.