Tahina Ramananandro
Principal Research Software Development Engineer
About
I joined MSR RiSE (opens in new tab) in September 2016, working on the Everest (opens in new tab) project: verified implementations of TLS and derivatives, using and extending the F* (opens in new tab) higher-order, effectful, dependently typed programming language.
I am one of the main authors of the EverParse (opens in new tab) toolchain for formally verified binary data parsing and formatting.
My research interests span programming languages and formal methods, especially formal verification, language semantics, verified compilation.
See my external website (opens in new tab) for more information on my pre-MSR research and publications.
Featured content
EverParse: Hardening critical attack surfaces with formally proven message parsers
EverParse is a framework for generating provably secure parsers and formatters used to improve the security of critical code bases at Microsoft. EverParse is developed as part of Project Everest, a collaboration between Microsoft Research labs in Redmond, Washington; India;…
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats
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…