[<prev] [next>] [<thread-prev] [day] [month] [year] [list]
Message-ID: <20191025205144.231de493@sybil.lepiller.eu>
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.
