Date: Fri, 25 Oct 2019 14:15:40 +0200 From: Hanno Böck <hanno@...eck.de> To: oss-security@...ts.openwall.com Subject: Re: Formal verification of open source software On Fri, 25 Oct 2019 13:43:57 +0300 Georgi Guninski <gguninski@...il.com> wrote: > Are there success stories of formal verification of open source > software? There's been a lot of work in the crypto community in this direction. Most of it is code under OSS licenses: Hacl* is a formally verified crypto library. Some of the crypto algorithm implementations are used in Mozilla's NSS: https://blog.mozilla.org/security/2017/09/13/verified-cryptography-firefox-57/ Also NSS/Mozilla, they have identified a flaw in their gcm implementation with cryptol: https://timtaubert.de/blog/2017/06/verified-binary-multiplication-for-ghash/ There's been a formal verification of (a subset of) PolarSSL: https://blog.regehr.org/archives/1261 This is an incomplete list, just the first things I remembered, there's a lot more. In terms of operating system kernels there's sel4: https://sel4.systems/ -- Hanno Böck https://hboeck.de/ mail/jabber: hanno@...eck.de GPG: FE73757FA60E4E21B937579FA5880072BBB51E42
Powered by blists - more mailing lists
Please check out the Open Source Software Security Wiki, which is counterpart to this mailing list.
Confused about mailing lists and their use? Read about mailing lists on Wikipedia and check out these guidelines on proper formatting of your messages.