Date: Sun, 10 Apr 2016 19:18:23 -0700 From: Joe Duarte <songofapollo@...il.com> To: musl@...ts.openwall.com 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: 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. 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.