Pierre-Yves Strub (MSR INRIA)

Toward Machine-Checked Program Verification for Concrete Cryptography

Jeudi 3 Novembre 2011, 11h salle 1D23

Type systems, relational logics, and interactive proof assistants are effective tools for verifying the security of programs and systems that rely on cryptography. They can provide automation, modularity and scalability. As illustrated in recent case studies, they can be usefully applied to large security protocols and applications [Bhargavan et al., 2008, Fournet et al., 2009].

However, their models traditionally rely on abstract assumptions on the underlying cryptographic primitives, expressed in symbolic models. Cryptographers usually reason on security assumptions in lower-level models that precisely account for the complexity and probability of attacks. These models are more complex and realistic, but recent results suggest thay they are also amenable to formal automated verification [Blanchet, 2006, Barthe et al., 2009, Acar et al., 2011].

I will present our on-going work in adapting and extending our programming and verification framework based on refinement types for ML programs [Bengtson et al., 2008, Bhargavan et al., 2010, Fournet, 2011] which currently uses a combination of automated proofs (using Z3, an SMT solver) and interactive proofs (using Coq), in order to produce machine-checked security proofs of cryptographic programs and libraries under concrete computational assumptions.