[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Message-ID: <20191025141540.10b322fe@computer>
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.
