illustration of data storage and cloud storage around the Eiffel tower

Inria Joint Center

Microsoft Research Blog

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.”
Blog de recherche Microsoft

| Tahina Ramananandro, Aseem Rastogi, et 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;…

a view of a snow covered mountain
Blog de recherche Microsoft

| Nikhil Swamy

Project Everest is a multiyear collaborative effort focused on building a verified, secure communications stack designed to improve the security of HTTPS, a key internet safeguard. This post—about the proving methodology and verification tools of Project Everest—is the third in…

Blog de recherche Microsoft

| Jonathan Protzenko et Bryan Parno

Project Everest is a multiyear collaborative effort focused on building a verified, secure communications stack designed to improve the security of HTTPS, a key internet safeguard. This post, about the high-performance industrial-grade EverCrypt cryptographic provider, is the second in a…

Blog de recherche Microsoft

Project Everest is a multiyear collaborative effort focused on building a verified, secure communications stack designed to improve the security of HTTPS, a key internet safeguard. This post, about the verification tools and techniques the Everest team is using and…

Jonathan Protzenko standing outside
Podcast de recherche Microsoft

Episode 58, January 9, 2019 - Dr. Protzenko talks about what’s wrong with software (and why it’s vitally important to get it right), explains why there are so many programming languages (and tells us about a few he’s been working…

photo of Dr. Ben Zorn - Research Manager, Principal Researcher, wearing glasses and smiling at the camera
Podcast de recherche Microsoft

In an era of AI breakthroughs and other exciting advances in computer science, Dr. Ben Zorn would like to remind us that behind every great technical revolution is… a programming language. As a Principal Researcher and the Co-director of RiSE…

Blog de recherche Microsoft

Jeannette M. Wing Photo credit: Scott Eklund/Red Box pictures By Jeannette M. Wing, corporate vice president, Microsoft Research “Think Bolder, Aim Higher” is a mantra I’ve been chanting since my arrival at Microsoft three years ago. I’ve wanted to encourage…