To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 05/02/10 - Paris - FR 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 - Rocquencourt Amphi Turing du bâtiment 1 Vendredi 5 février, 10h30 ----------------- Karthik Bhargavan ----------------- INRIA =============================================================== Scalable Verification of Security Protocol Code by Typechecking =============================================================== F7 is a typechecker for verifying security properties of the source code of cryptographic protocols and access control mechanisms. The underlying type theory is a lambda-calculus equipped with refinement types for expressing pre- and post-conditions within first-order logic. We derive formal cryptographic primitives and represent active adversaries within the type theory. Well-typed programs enjoy assertion-based security properties, with respect to a realistic threat model including key compromise. The implementation amounts to an enhanced typechecker for the general purpose functional language F#; typechecking generates verification conditions that are passed to an SMT solver. I will present the underlying type system and evaluate the typechecker on a series of large case studies of protocol code, previously checked using whole-program analyses based on ProVerif, a leading verifier for cryptographic protocols. Our results indicate that compositional verification by typechecking with refinement types is more scalable than the best domain-specific analysis currently available for cryptographic code. This is joint work with Andy Gordon and Cedric Fournet at Microsoft Research Cambridge, Jesper Bengtson at Uppsala University, and Sergio Maffeis at Imperial College London. Some results were published at IEEE CSF'08 and POPL'10.