Improving trust in the compilation from F* to C
Episode details
Episode description
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/
Watch also from the same channel
More episodes from this channel
You might be interested in
