Improving trust in the compilation from F* to C

Subscribers:
344,000
Published on ● Video Link: https://www.youtube.com/watch?v=YJtk7CMEO4s



Duration: 38:14
524 views
5


F* is a ML-like programming language aimed at program verification, allowing its users to write programs, specifications, and prove them correct in the same tool. It is a key component of the Everest project, whose goal is building a fully verified HTTPS stack, including cryptographic libraries and a TLS implementation. To achieve good performance, F* programs are compiled to C using the KreMLin tool, which is part of the trusted code base. As part of my internship, I worked on improving the trust in the process of translating F* programs to C. I first experimented on a mechanized proof of the soundness of KreMLin in Lean. Then, shifting perspective, I worked on allowing more low-level C-like programming patterns to be verified on F* side. Building on an existing F* library modeling low-level C-like structures, I implemented higher-level constructs like tagged-unions, attempting to bridge the gap between idiomatic F* code and the compiled C code. 

See more on this video at https://www.microsoft.com/en-us/research/video/improving-trust-compilation-f-c/







Tags:
microsoft research