Follow @Openwall on Twitter for new release announcements and other news
[<prev] [next>] [thread-next>] [day] [month] [year] [list]
Date: Sun, 10 Apr 2016 19:18:23 -0700
From: Joe Duarte <>
Subject: Formal verification of MUSL

Hi all,

Has there been any discussion of getting MUSL into a formally verified
state? What would it take?

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.

I started wondering about the possibilities for MUSL after seeing this
write-up from the formally verified seL4 microkernel project:

I draw your attention to the bottom section titled *What the Proof Implies*.
It looks impressive. Their source code is here:

The other piece for me was John Regehr's post on TrustInSoft's audit of the
PolarSSL library:

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:

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.


Joe Duarte

p.s. I don't see MUSL on the free Coverity deal ( I think the LibreOffice devs got some
good insights from it.

Content of type "text/html" skipped

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.