Re: Formal verification of MUSL

[Joe Duarte <songofapollo@gmail.com>]

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