News for hackers. Stuff that matters.

A comment on Hardening attack surfaces with formally proven binary format parsers. Parent comment

Re:Hardening attack surfaces with formally proven binary for... by masklinn on Monday July 04, 2022 @07:38AM (#31975935)
TBF lots of formal tools don’t either, because you still have to translate the proven code by hand.

It looks like Microsoft’s does the translation, so the only risk is bugs in the code generator, which seems nice.

There’s also Google’s wuffs, but I don’t think that is formal, it just ensures memory safety.

[ Parent | on HN ]
Re:Hardening attack surfaces with formally proven binary for... by jnash on Tuesday July 05, 2022 @12:39AM (#31984371)
Yep if the translation is done by hand then that might be a potential problem. However a lot of modern proof tools have proven correct translators (based on the CompCert work).
[ Parent | on HN ]