F7: Refinement Types for F#

Microsoft Research, Cambridge

F7 is an enhanced typechecker for the F# programming language. F7 supports static checking of properties expressed with refinement types. Our motivation is to check various security properties of F# implementation code by typing.

Paper

• J. Bengtson, K. Bhargavan, C. Fournet, A.D. Gordon, S. Maffeis Refinement Types for Secure Implementations (paper at CSF 2008) (talk at CSF 2008) (MSR-TR-2008-118) (summary)

  We present the design and implementation of a typechecker for verifying security properties on 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 a 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.

Software

• The F7 Typechecker: Download, Manual

Researchers

• Karthik Bhargavan, Microsoft Research
• Cédric Fournet, Microsoft Research
• Andy Gordon, Microsoft Research

Collaborators

• Sergio Maffeis, Imperial College and University of California Santa Cruz
• Jesper Bengtson, Uppsala University