Re: Formal verification of MUSL

[Rich Felker <dalias@libc.org>]

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.

> I'm a bit concerned about vulnerabilities like CVE-2015-1817 from March of
> last year. MUSL is a safer bet than the alternatives, but we still seem to
> occupy a universe where all non-trivial C software or libraries are likely
> to have exploitable memory issues at any arbitrary time point / at all
> times including the present. This baseline reality strikes me as strange.

Indeed.

> I started wondering about the possibilities for MUSL after seeing this
> write-up from the formally verified seL4 microkernel project:
> http://ssrg.nicta.com.au/projects/TS/l4.verified/proof.pml
> 
> I draw your attention to the bottom section titled *What the Proof Implies*..
> It looks impressive. Their source code is here: https://github.com/seL4
> 
> The other piece for me was John Regehr's post on TrustInSoft's audit of the
> PolarSSL library: http://blog.regehr.org/archives/1261
> 
> I think what they did was a bit less formal and perhaps less laborious than
> what the seL4 project team did, but it's still pretty neat, and probably
> quite rare. Their report, or "verification kit", is here:
> http://trust-in-soft.com/polarSSL_demo.pdf
> 
> I assume that external audits aren't cheap. Something maintainable and
> somewhat automated would be ideal. I've never messed with theorem provers
> and formal verification – is this feasible? In any case, whether an
> external audit or house project, I'm in for fifty bucks at least.

One thing you have going for you with libc is that there's not a lot
of interdependency; most components could be treated individually. Of
course the big important ones like stdio have a lot of internal
complexity themselves (and some "gratuitous UB" we need to fix due in
stdio's case to the awful buffer pointer model we inherited). The
worst part is probably proving correctness of thread synchronization
primitives and related code.

> p.s. I don't see MUSL on the free Coverity deal (
> https://scan.coverity.com/projects). I think the LibreOffice devs got some
> good insights from it.

What's needed to get it there?

Rich