Date: Mon, 11 Apr 2016 18:00:24 -0700 From: Joe Duarte <songofapollo@...il.com> To: musl@...ts.openwall.com Subject: Re: Formal verification of MUSL > > > > > 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 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.