Follow @Openwall on Twitter for new release announcements and other news
[<prev] [next>] [<thread-prev] [day] [month] [year] [list]
Date: Fri, 25 Oct 2019 20:52:02 +0200
From: Julien Lepiller <>
Subject: Re: Formal verification of open source software

Le Fri, 25 Oct 2019 18:37:44 +0300,
Georgi Guninski <> a écrit :

> On Fri, Oct 25, 2019 at 3:17 PM Hanno Böck <> 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:
tried to find bugs in multiple C compilers. Here is what they say about

"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,

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.