Refinement Types for Secure Implementations

Jesper Bengtson, Karthikeyan Bhargavan, Cedric Fournet, Andrew D. Gordon, and Sergio Maffeis

Abstract

We present the design and implementation of 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. We describe a series of checked examples. This is the first tool to verify authentication properties of cryptographic protocols by typechecking their source code.

Details

Publication typeTechReport
URLhttp://www.computer.org/portal/site/ieeecs/index.jsp
NumberMSR-TR-2008-118
Pages46
InstitutionMicrosoft Research
PublisherIEEE Computer Society
> Publications > Refinement Types for Secure Implementations