Verifying Cryptographic Implementations with F*

Course at Computer-aided security proofs, Aarhus, Denmark, 9-11 October 2017

Lecturers: Cédric Fournet, Cătălin Hriţcu, Aseem Rastogi

Materials

• Cédric (10:00-11:00): Overview of Project Everest
• Cătălin (11:00-12:00): A Gentle Introduction to F*: Verifying purely functional programs (code)
• Cătălin (13:00-15:00): Verifying Stateful Programs with F* (code)
• Cédric (15:00-16:00): Verifying crypto algorithms
• Exercise session (16:00-17:00) (RSA; stacks)

• Aseem (9:00-10:30): Monotonic State in F* (code)
• Cédric (10:30-12:00): Crypto security: authenticity and confidentiality
• Cédric (13:00-15:10): Crypto security: authenticity and confidentiality
• Aseem (15:10-15:40): Secure File Transfer (code)
• Cătălin (15:40-16:40): Monadic effects in F* and Dijkstra Monads
• Aseem (16:40-17:00): F* memory models (Code: Heap, HyperHeap, HyperStack)

• Cédric (9:00-10:45): Crypto security: AEAD and TLS
• Aseem (11:00-12:00): Wys*: A Verified Language Extension for Secure Multi-party Computations

Code

• Code from F* slides
• Exercises from F* slides; solutions

Setup

• Online editor
• F* binaries (instructions)
• F* OPAM package
• F* mode for Emacs
• Other ways to install F*

More references

• F* website
• F* tutorial
• F* code on GitHub