[prev in list] [next in list] [prev in thread] [next in thread] 

List:       oss-security
Subject:    Re: [oss-security] Formal verification of open source software
From:       Julien Lepiller <security () lepiller ! eu>
Date:       2019-10-25 18:52:02
Message-ID: 20191025205144.231de493 () sybil ! lepiller ! eu
[Download RAW message or body]

Le Fri, 25 Oct 2019 18:37:44 +0300,
Georgi Guninski <gguninski@gmail.com> a écrit :

> On Fri, Oct 25, 2019 at 3:17 PM Hanno Böck <hanno@hboeck.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).
[prev in list] [next in list] [prev in thread] [next in thread]