Improving trust in the compilation from F* to C

Опубликовано 22 августа 2017, 4:41

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 microsoft.com/en-us/research/v...