I joined MSR RiSE in September 2016, working on the Everest project: verified implementations of TLS and derivatives, using and extending the F* higher-order, effectful, dependently typed programming language.
My research interests span programming languages and formal methods, especially formal verification, language semantics, verified compilation.
Prior to joining MSR, I worked with Prof. Zhong Shao at Yale University on the CertiKOS verified operating system. Previously, in 2012, I defended my PhD thesis at INRIA and Université Paris Diderot, directed by Dr. Xavier Leroy, on verified compilation for C++ objects. See my external website for more information on my pre-MSR research and publications.
We present EverParse, a framework for generating parsers and serializers from tag-length-value binary message format descriptions. The resulting code is verified to be safe (no overflow, no use after free), correct (parsing is the inverse of serialization) and non-malleable (each…