Date: Mon, 11 Apr 2016 14:21:07 +0200 From: Szabolcs Nagy <nsz@...t70.net> To: musl@...ts.openwall.com Subject: Re: Formal verification of MUSL * Rich Felker <dalias@...c.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).
Powered by blists - more mailing lists
Confused about mailing lists and their use? Read about mailing lists on Wikipedia and check out these guidelines on proper formatting of your messages.