Date: Fri, 25 Oct 2019 20:52:02 +0200 From: Julien Lepiller <security@...iller.eu> To: oss-security@...ts.openwall.com Subject: Re: Formal verification of open source software Le Fri, 25 Oct 2019 18:37:44 +0300, Georgi Guninski <gguninski@...il.com> a écrit : > On Fri, Oct 25, 2019 at 3:17 PM Hanno Böck <hanno@...eck.de> wrote: > > > > > > There's been a lot of work in the crypto community in this > > direction. Most of it is code under OSS licenses: > > > > Thanks for the links. > > Are there known bugs in formally verified software or hardware? Hi, I think it's my first time writing to the list :) CompCert is not FOSS, but it's a verified compiler. This paper: https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf tried to find bugs in multiple C compilers. Here is what they say about CompCert: "The striking thing about our CompCert results is that the middle- end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users" (they have found a few bugs in unverified parts of the compiler, though) So there is a real impact of formal methods on program correctness. I don't know much about other verified software, so I'll be happy to read anything about bugs in them. > > Is there any software which comes with monetary warranty? > > Are loops sizes in C code serious problem for verification? > (something like infinity in math. IIRC Coq have problem with this).
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.