Refinement Types for Secure Implementations

Jesper Bengtson, Karthikeyan Bhargavan, Cédric Fournet, Andrew D. Gordon, Sergio Maffeis

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 λ-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.
Original languageEnglish
Title of host publicationProceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, 23-25 June 2008
PublisherInstitute of Electrical and Electronics Engineers
Pages17-32
Number of pages16
ISBN (Print)978-0-7695-3182-3
DOIs
Publication statusPublished - Jun 2008

Fingerprint

Dive into the research topics of 'Refinement Types for Secure Implementations'. Together they form a unique fingerprint.

Cite this