<story><title>Hardening attack surfaces with formally proven binary format parsers</title><url>https://www.microsoft.com/en-us/research/publication/hardening-attack-surfaces-with-formally-proven-binary-format-parsers/</url></story><parent_chain></parent_chain><comment><author>dataangel</author><text>I find it very impressive that the work actually made it into the Windows kernel. AFAIK the Linux kernel doesn&amp;#x27;t have formally verified parsers for any of the wire formats it deals with, this seems like an improvement on actually-in-use-outside-the-lab state of the art.</text></comment>
<story><title>Hardening attack surfaces with formally proven binary format parsers</title><url>https://www.microsoft.com/en-us/research/publication/hardening-attack-surfaces-with-formally-proven-binary-format-parsers/</url></story><parent_chain></parent_chain><comment><author>tbrownaw</author><text> &amp;gt; &lt;i&gt;Software artifacts. The application of our toolchain to
Windows includes proprietary source code and is not publicly available. However, the 3D toolchain, including the EverParse libraries, the F programming language, Z3 SMT solver,
and the KaRaMeL C code generator are all open source and
developed publicly on GitHub. Documentation, code samples, and links to our latest tool releases are available from
&lt;a href=&quot;https:&amp;#x2F;&amp;#x2F;project-everest.github.io&amp;#x2F;everparse&quot; rel=&quot;nofollow&quot;&gt;https:&amp;#x2F;&amp;#x2F;project-everest.github.io&amp;#x2F;everparse&lt;/a&gt;.&lt;/i&gt;&lt;p&gt;From the linked paper.</text></comment>