Re: Formal verification of MUSL

[Szabolcs Nagy <nsz@port70.net>]

* Rich Felker <dalias@libc.org> [2016-04-11 00:23:13 -0400]:
> On Sun, Apr 10, 2016 at 07:18:23PM -0700, Joe Duarte wrote:
> > Has there been any discussion of getting MUSL into a formally verified
> > state? What would it take?
> 
> There's been some discussion (off-list) of using tis-interpreter on
> musl, but that's not the same as formal verification. So far I'm not
> aware of anything in the way of actual verification.
> 

in general libc won't be formally verified until its api
and the underlying platform are formally defined
(i.e. the implemented posix api and underlying linux and
toolchain behaviour) this won't happen any time soon.

formal verification requires a precise model of the
interface (which means an alternative implementation)
and some annotation to help proving that the libc
matches the model.

this is a lot of work even for simple apis, it is more
realistic to only prove some easy but practically useful
property for a subset of the libc code, so you have to
be more precise what you ask for.

some properties are easy to model, but still hard to verify
(e.g. ieee 754 arithmetics has formal models, but verifying
the accuracy of math functions is hard.)

some properties are easy to verify with moderate modelling
effort (e.g. checking for posix namespace violations in libc
headers).

some properties are hard to verify, but easy to check at
runtime with moderate overhead (e.g. signed int overflow
checks with ubsan instrumentation).

etc.

checking for security issues is a small subset of formal
verification (in c the most relevant property is probably
well-defiend memory accesses).