Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o / ) __) / / / / / /\/| (___/ (_/ (_ (_ / (__/ / | I N R I A - Paris 2 rue Simone Iff (ou: 41 rue du Charolais) Salle Lions 1, bâtiment C JEUDI 3 octobre, 10h30 ------------------- Tahina Ramananandro ------------------- Microsoft Research, Redmond ================================================================ EverParse: verified efficient parsing for transport data formats ================================================================ Parsers are a security-critical part of networking software, where bugs can lead to such catastrophes as the 2017 Cloudflare data leaks ("Cloudbleed".) We present EverParse, our open-source library and tools for automatic generation of verified efficient parsers for binary transport data formats. EverParse takes a data format description and produces an F* implementation of parsers and serializers for it. EverParse produces low-level code in the Low* subset of F* that is then compiled to C. The produced code is verified for memory safety, functional correctness (parsers and serializers are inverse of each other) and such security properties as non-malleability (unique binary representation for authentication purposes.) The produced code is memory-efficient, minimizing the need for memory allocations and copies. EverParse is part of Project Everest, a collaborative (MSR-CMU-INRIA-U.Edinburgh) research effort to deploy verified implementations of the TLS protocol and derivatives.