Apr 1
Very cool twist on packet parsing from @eriangazag; use an OCaml DSL to do verified parsing via Everparse, including zero copy codecs. Uses CCSDS satellite packets as a running example: I wrote a hand parser in C for this when at JPL in 1998, just trying to dig out my old code from RCS/CVS! gazagnaire.org/blog/2026-03-…
5
28
2,046
19 Nov 2023
We have started on coq and everparse, but we want to learn more!
1
201
15 Nov 2023
For a format specification in 3D, EverParse generates both verified parsers in C as well as both positive and negative test inputs for that parser. The positive inputs are especially useful for fuzzing application logic behind the verified parser. github.com/project-everest/e…
2
217
5 Oct 2023
Our team at @TechAtBloomberg is looking for its very first certified programming expert! You’re good with @CoqLang & love @MSFTResearch’s F* / everparse? Wanna apply your skills to industrial problems and always wanted to give NYC a shot? This is for you! Reach out :)
1
5
1,892
7 Jun 2023
Had a good close read of Everparse and was aware of Erlang's approach, though not in depth. I went around and around with how to deal with variable-length things and decided that reifying them was too magic; fixed length is enough of a value-add to ship layouts as is.
2
2
78
18 Mar 2023
to be explicit; i did not paste in the paper. I didn't even give the full title of the paper.
My entire initial prompt was "what does the ◃ parser combinator do in the EverParse paper?" and -4 gave me a correct answer.
9
1,409
20 Dec 2022
ASN1* at CPP 23:
Formalizing ASN.1 DER in EverParse, led by the amazing Haobin Ni from Cornell.
ASN.1 is a data description language. That lock icon in your browser when you connect using https... it hinges on the security of X.509 and ASN.1
fstar-lang.org/papers/asn1st…
#fstarlang
1
13
1,964
15 Jun 2022
EverParse is super cool! It even has support for zero-copy parsing!
1
28 Feb 2022
Accepted (conditionally) at PLDI 2022: "Hardening Attack Surfaces with Formally Proven Binary Format Parsers" ... describing multiple years of work getting correct & secure parsers into the Windows network virtualization stack.
#everparse #fstarlang @MSFTResearch #pldi2022
3
13
116
EverParse: Hardening critical attack surfaces with formally proven message parsers
lobste.rs/s/n62mdp #ml #security
microsoft.com/en-us/research…
1
3
The application of #EverParse to HyperV is a pioneering demonstration that #verification is both more secure and possible at scale in systems. Congratulations to @lambdaNik, the #ProjectEverest team, and their #WindowsNetworking partners for taking this huge step. @MSFTResearch
3 May 2021
It's been really exciting to work with the Windows Network Virtualization team over the past 18 months to deploy high-performance, low-level code for parsing network messages backed by mathematical proofs of correctness and security.
1
2
12
4 May 2021
hardware wallet devs check this out: MS Research "EverParse seeks to make handwritten low-level parsers a thing of the past. With the state of the art in program proofs, we can generate highly efficient, provably correct, and secure low-level parsers" project-everest.github.io/ev…
1
3
4 May 2021
This is really cool. More solutions like this please…
“Put another way, network packets are handled first by EverParse code that is proven to correctly parse and accept only well-formed messages, rejecting potentially malicious inputs before they reach the rest of the system.”
3 May 2021
Improper input validation is a common & serious software threat. EverParse offers protection. The framework automatically produces high-performance, formally proven C code for parsing messages. Learn how it’s being used to harden critical attack surfaces: aka.ms/AAcdr3f
3
4 May 2021
EverParse sounds pretty amazing and ready for prime time if it’s shipping formally verified virtual switch code in hyper-v. Windows and Linux developers should check it out!
3 May 2021
"We now turn to the use of EverParse in the Windows kernel to secure the virtual networking stack, specifically its use in Hyper-V Virtual Switch" 👏
5
10
3 May 2021
EverParse: Hardening critical attack surfaces with formally proven message parsers microsoft.com/en-us/research…
2
3 May 2021
"We now turn to the use of EverParse in the Windows kernel to secure the virtual networking stack, specifically its use in Hyper-V Virtual Switch" 👏
3 May 2021
Improper input validation is a common & serious software threat. EverParse offers protection. The framework automatically produces high-performance, formally proven C code for parsing messages. Learn how it’s being used to harden critical attack surfaces: aka.ms/AAcdr3f
4
47
3 May 2021
Improper input validation is a common & serious software threat. EverParse offers protection. The framework automatically produces high-performance, formally proven C code for parsing messages. Learn how it’s being used to harden critical attack surfaces: aka.ms/AAcdr3f
2
78
290
EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats
lobste.rs/s/rjd8dz #formalmethods #security
usenix.org/conference/usenix…
3
16 Aug 2019
Next up at #usesec19: "EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats"
Tahina Ramananandro, Antoine Delignat-Lavaud, Cédric Fournet, and Nikhil Swamy, Microsoft Research; Tej Chajed, MIT; Nadim Kobeissi, Inria Paris; Jonathan Protzenko, MS Research
1
1
3