[<prev] [next>] [<thread-prev] [thread-next>] [day] [month] [year] [list]
Date: Fri, 25 Oct 2019 14:37:59 +0000
From: Pascal Cuoq <cuoq@...st-in-soft.com>
To: "oss-security@...ts.openwall.com" <oss-security@...ts.openwall.com>
Subject: Re: Formal verification of open source software
Hello,
I work for the company that did a report on PolarSSL, as it was called
then. We have applied similar tech to other open-source components,
at least partially, and identified some interesting bugs in the process.
For some of the components the formal guarantee may be as low as:
"when executing the provided tests, or fuzzer-generated tests, for all
possible results of calls to malloc (success or failure),
the result of execution does not depend on the memory layout
and the execution is free of undefined behavior (for a pretty strict
definition of undefined behavior)".
For some other software components, the guarantee is more what you
would expect from formal methods, that is, for all of (billions of)
inputs for one or several specific usage patterns of the
library. Please look at the PolarSSL report for an example of what
this means. It does not make sense to claim that a C *library* is
formally verified without qualification, because any nontrivial
C function is unsafe when used wrongly. It can only be verified safe
for one or several ways of using it, which the person doing the
verification usually defines, and which may not cover all possible
ways the library is used in practice.
OpenSSL: we have had some open bugs for functions that could allocate
(and thus fail) but were returning void without reporting success or
failure, so that their callers would dereference NULL or worse.
They were reported at the time OpenSSL bug reports were ignored in majority,
but I think all the things we reported have been fixed now.
zlib: https://trust-in-soft.com/auditing-zlib/
tiny-AES128-C: https://trust-in-soft.com/the-sociology-of-open-source-security-fixes-continued/
libwebp: https://trust-in-soft.com/out-of-bounds-pointers-a-common-pattern-and-how-to-avoid-it/
SQLite: https://blog.regehr.org/archives/1292
There are more, but these are the ones that come to mind for which
a bit of writeup is available.
​Pascal
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.
