F* is a language in the tradition of ML equipped with dependent types, monadic effects, refinement types and a weakest precondition calculus. Together, these features enable the F* programmer to prove functional correctness using a combination of automation via SMT solving and manual program proofs.
In the context of the greater Everest project, we are using F* to prove, build and deploy miTLS, a verified, efficient implementation of the Transport Layer Security (TLS) 1.3 protocol.
This extended abstract presents our work in progress. We are currently focusing our efforts on proving the memory safety and functional correctness of Elliptic Curve Cryptography (ECC) primitives, and on extracting this code to C. ECC primitives are a good candidate: they are modeled after the reference implementations in C. Therefore, they only exercise an imperative, first-order subset of F* that lends itself well to an efficient extraction to C.
Thu 22 SepDisplayed time zone: Osaka, Sapporo, Tokyo change
10:35 - 11:25
WebML at Conference Room 1
Chair(s): Katsuhiro Ueno Tohoku University, Japan
|WebAssembly: high speed at low cost for everyone|
Andreas Rossberg GooglePre-print
|Extracting from F* to C: a progress report|
Jonathan Protzenko Microsoft Research, Karthikeyan Bhargavan INRIA, Jean-Karim Zinzindohoué INRIA, Abhishek Anand , Cédric Fournet Microsoft Research, Bryan Parno , Aseem Rastogi Microsoft Research India, Nikhil Swamy Microsoft ResearchPre-print