Verifying Low-level Code for Security and Correctness in F*

Oregon Programming Language Summer School (OPLSS 2019)

Videos of the lectures are here.

The material I presented represents work by a large team of people working on F* and Project Everest.

For questions about F* join fstar.zulipchat.com.
  1. Lecture 1
    1. Wednesday, June 26: Overview, Functional core of F*, Basic effects, WP-generation, Richer memory models
    2. Thursday, June 27: lenses; then EverParse: parsers, parser generators
    3. EverParse, Paper at USENIX Security 2019
    4. EverParse software on GitHub


  2. Lecture 2: Thursday, June 27: Modeling and Proving Cryptographic Security
    Code: In the examples/crypto directory: Make it using `make -f Makefile.oplss verify-all`
    1. Authenticated Encryption: AE.fsti
    2. UF-CMA MAC: MAC.fst
    3. IND-CPA Encryption: CPA.fst


  3. Lecture 3: Friday, June 28: Relational proofs of equivalence
    1. Relational proofs by monadic reification (lecture slides) Based on a CPP 18 paper. I also mentioned these other papers:
      1. Simple relational correctness proofs for static analyses and program transformation, Nick Benton, 2004
      2. Turing completeness totally for free, Conor McBride
    2. Perfect secrecy of One-time pads: OTP.fst
    3. Semantic secrecy of El Gamal encryption: ElGamal.fst
    4. Setoids, modules, functors, epsilon equivalences Setoids.fst


  4. Lecture 4: Saturday, June 29: Verified cryptographic primitives, EverCrypt and Vale.
    1. Lecture slides (Thanks Jonathan and Chris!)
      Vale @ POPL '19
      EverCrypt paper EverCrypt code
    2. Efficient, extensible VC generation with typeclasses and normalization MiniValeSemantics.fst
    3. Generic programming, for a model of verified interoperability between Low* and Vale (calling conventions only) Interop.fst
      Altenkirch and McBride, Generic Programming within Dependently Typed Programming