Formal verification of MUSL

Formal verification of MUSL

[Joe Duarte]

[-- 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 --]

Re: Formal verification of MUSL

[Rich Felker]

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

Re: Formal verification of MUSL

[Khem Raj]

On Sun, Apr 10, 2016 at 9:23 PM, Rich Felker <dalias@libc.org> wrote:
>> 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?

I have registered

https://scan.coverity.com/projects/libc-musl

Re: Formal verification of MUSL

[Eric Engeström]

[-- Attachment #1: Type: text/plain, Size: 578 bytes --]

On 11 Apr 2016 5:36 a.m., "Khem Raj" <raj.khem@gmail.com> wrote:
>
> On Sun, Apr 10, 2016 at 9:23 PM, Rich Felker <dalias@libc.org> wrote:
> >> 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?
>
> I have registered
>
> https://scan.coverity.com/projects/libc-musl

"You are not authorized to access this page."
I have no experience with Coverity, but I guess you missed a step to make
it public. (The search also comes up empty.)

[-- Attachment #2: Type: text/html, Size: 941 bytes --]

Re: Formal verification of MUSL

[Joe Duarte]

[-- Attachment #1: Type: text/plain, Size: 2211 bytes --]

>
> >
> > I have registered
> >
> > https://scan.coverity.com/projects/libc-musl
>
> "You are not authorized to access this page."
> I have no experience with Coverity, but I guess you missed a step to make
> it public. (The search also comes up empty.)
>

​Yes, I noticed that as well. It gave me the same "not authorized" message.
Normally, we should be able to add the project to our personal Coverity
accounts by going to My Dashboard (top), click the Add a New Project
button, then search for the project. Currently, musl is still not showing
up in the search – maybe it takes a couple of days to show?

Nagy, everything you said sounds right. What about unikernels? Long-term,
I'm more interested in running unikernels than in running Linux, BSD, or
Windows. I'm thinking of something lik
e OSv
​, where they built an ELF linker from scratch, as well as implementing the
Linux system calls:
https://github.com/cloudius-systems/osv/wiki/Components-of-OSv

In their case, they were going for glibc compatibility, and I assume a
straight musl implementation would be easier. This ultimately gets at the
separation of OS syscalls and ABIs vs. the libc. What if I have an OS or
unikernel that doesn't know anything about C or POSIX, where C isn't a
first-class citizen so much as an honored guest? musl-leveraging C
applications would presumably be statically compiled in that case (and
perhaps containerized), but there would also need be an ABI layer that is
unclear to me. (Maybe this is relevant: How to Run POSIX Apps in a Minimal
Picoprocess: http://research.microsoft.com/apps/pubs/default.aspx?id=183461
-- which they might be drawing from in their recently announced bash or
Ubuntu support. How they emulated the Linux ABI in that paper is very
interesting.)

I think the formal verification task would be simplified if we could shrink
the ABI down in a unikernel or similar context, but I've only just begun to
think about this.

On floating point, the C
ompCert team just published a new paper on verified compilation of floating
point computations:
​ ​
https://hal.inria.fr/hal-00862689
​  ​
It looks like nice work.

Cheers,

Joe

[-- Attachment #2: Type: text/html, Size: 4183 bytes --]

Re: Formal verification of MUSL

[Isaac Dunham]

On Mon, Apr 11, 2016 at 06:00:24PM -0700, Joe Duarte wrote:
> >
> > >
> > > I have registered
> > >
> > > https://scan.coverity.com/projects/libc-musl
> >
> > "You are not authorized to access this page."
> > I have no experience with Coverity, but I guess you missed a step to make
> > it public. (The search also comes up empty.)
> >
> 
> ​Yes, I noticed that as well. It gave me the same "not authorized" message.
> Normally, we should be able to add the project to our personal Coverity
> accounts by going to My Dashboard (top), click the Add a New Project
> button, then search for the project. Currently, musl is still not showing
> up in the search – maybe it takes a couple of days to show?
> 
> Nagy, everything you said sounds right. What about unikernels? Long-term,
> I'm more interested in running unikernels than in running Linux, BSD, or
> Windows. I'm thinking of something like OSv, where they built an ELF
> linker from scratch, as well as implementing the Linux system calls:
> https://github.com/cloudius-systems/osv/wiki/Components-of-OSv

OSv uses a (rather old) version of musl, with some changes needed.
If I understand correctly, they essentially changed musl so that rather
than using syscalls, it would directly call the underlying kernel function.

Another unikernel-type project using musl is the ELLCC "Embedded Little
Kernel": 
http://ellcc.org/blog/?tag=elk


And while we're discussing alternate hosts, I might as well mention that
seL4 uses musl for the POSIX libc.

> In their case, they were going for glibc compatibility, and I assume a
> straight musl implementation would be easier. This ultimately gets at the
> separation of OS syscalls and ABIs vs. the libc. What if I have an OS or
> unikernel that doesn't know anything about C or POSIX, where C isn't a
> first-class citizen so much as an honored guest? musl-leveraging C
> applications would presumably be statically compiled in that case (and
> perhaps containerized), but there would also need be an ABI layer that is
> unclear to me. (Maybe this is relevant: How to Run POSIX Apps in a Minimal
> Picoprocess: http://research.microsoft.com/apps/pubs/default.aspx?id=183461
> -- which they might be drawing from in their recently announced bash or
> Ubuntu support. How they emulated the Linux ABI in that paper is very
> interesting.)
> 
> I think the formal verification task would be simplified if we could shrink
> the ABI down in a unikernel or similar context, but I've only just begun to
> think about this.
> 
> On floating point, the C
> ompCert team just published a new paper on verified compilation of floating
> point computations:
> ​ ​
> https://hal.inria.fr/hal-00862689
> ​  ​
> It looks like nice work.
> 
> Cheers,
> 
> 

Re: Formal verification of MUSL

[Joe Duarte]

[-- Attachment #1: Type: text/plain, Size: 934 bytes --]

On Mon, Apr 11, 2016 at 8:55 AM, Eric Engeström <eric.engestrom@gmail.com>
wrote:

> On 11 Apr 2016 5:36 a.m., "Khem Raj" <raj.khem@gmail.com> wrote:
> >
> > On Sun, Apr 10, 2016 at 9:23 PM, Rich Felker <dalias@libc.org> wrote:
> > >> 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?
> >
> > I have registered
> >
> > https://scan.coverity.com/projects/libc-musl
>
> "You are not authorized to access this page."
> I have no experience with Coverity, but I guess you missed a step to make
> it public. (The search also comes up empty.)
>

​What's the status on Coverity? I'm still getting the "You are not
authorized to access this page." message that Eric reported. And when I
search Coverity Scan for musl, nothing comes up.​

Cheers,

Joe

[-- Attachment #2: Type: text/html, Size: 2099 bytes --]

Re: Formal verification of MUSL

[Szabolcs Nagy]

* 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).