Verifying Low-level Code for Security and Correctness in F*
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.
- Wednesday, June 26: Overview, Functional core of F*, Basic effects, WP-generation, Richer memory models
- Thursday, June 27: lenses; then EverParse: parsers, parser generators
- EverParse, Paper at USENIX Security 2019
- EverParse software on GitHub
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`
Authenticated Encryption: AE.fsti
UF-CMA MAC: MAC.fst
IND-CPA Encryption: CPA.fst
Lecture 3: Friday, June 28: Relational proofs of equivalence
Relational proofs by monadic reification (lecture slides)
Based on a CPP 18 paper.
I also mentioned these other papers:
Simple relational correctness proofs for static analyses and program transformation, Nick Benton, 2004
Turing completeness totally for free, Conor McBride
Perfect secrecy of One-time pads:
Semantic secrecy of El Gamal encryption:
Setoids, modules, functors, epsilon equivalences
Lecture 4: Saturday, June 29: Verified cryptographic primitives, EverCrypt and Vale.
Lecture slides (Thanks Jonathan and Chris!)
Vale @ POPL '19
Efficient, extensible VC generation with typeclasses and normalization MiniValeSemantics.fst
Generic programming, for a model of verified interoperability between Low* and Vale (calling conventions only)
Altenkirch and McBride, Generic Programming within Dependently Typed Programming