Nouvelles
Chargement
![An animation showing an example of a high-level language message format specified by EverParse. From the message, two arrows labeled “EverParse” point to a rectangle labeled “formal specification” and a rectangle labeled “low-level implementation,” respectively, inside a larger rectangle labeled “F* code.” The figure represents EverParse’s ability to automatically generate safe, correct, and fast F* parsing code. “Correctness” is defined as “Correctness: parse (serialize msg) = msg” and “valid msg ==> serialize (parse msg) = msg.” The F* logo appears with the description that F* is a type theory–based programming language and proof assistant that can prove theorems about programs. From the “F* code” rectangle, arrows point from the “low-level implementation” rectangle and a rectangle labeled “verified libraries for combinators” to a rectangle labeled “Safe high-performance C code.”](https://www.microsoft.com/en-us/research/uploads/prod/2021/05/1400x788_everparse_no_logo_still-1-480x280.jpg)
Microsoft Research Blog
EverParse: Hardening critical attack surfaces with formally proven message parsers
| Tahina Ramananandro, Aseem Rastogi, and Nikhil Swamy
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;…