From: Joe Duarte <songofapollo@gmail.com>
To: musl@lists.openwall.com
Subject: Formal verification of MUSL
Date: Sun, 10 Apr 2016 19:18:23 -0700 [thread overview]
Message-ID: <CAESemU9=93jRCT9vT-N5+Lrg2m_wC1yECTtjMihdXcf34ffj2A@mail.gmail.com> (raw)
[-- Attachment #1: Type: text/plain, Size: 1694 bytes --]
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:
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.
Cheers,
Joe Duarte
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.
[-- Attachment #2: Type: text/html, Size: 3391 bytes --]
next reply other threads:[~2016-04-11 2:18 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2016-04-11 2:18 Joe Duarte [this message]
2016-04-11 4:23 ` Rich Felker
2016-04-11 4:35 ` Khem Raj
2016-04-11 15:55 ` Eric Engeström
2016-04-12 1:00 ` Joe Duarte
2016-04-12 2:47 ` Isaac Dunham
2016-05-02 0:35 ` Joe Duarte
2016-04-11 12:21 ` Szabolcs Nagy
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to='CAESemU9=93jRCT9vT-N5+Lrg2m_wC1yECTtjMihdXcf34ffj2A@mail.gmail.com' \
--to=songofapollo@gmail.com \
--cc=musl@lists.openwall.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this public inbox
https://git.vuxu.org/mirror/musl/
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).