Please point me to High-Assurance Free-Libre / Open Source Software (FLOSS) Components
I’m looking for High Assurance and Free-Libre / Open Source Software (FLOSS) components. Can anyone point me to ones I don’t know about? A little context might help, I suppose…
A while back I posted a paper, High Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS). For purposes of the paper, I define “high assurance software” as software where there’s an argument that could convince skeptical parties that the software will always perform or never perform certain key functions without fail. That means you have to show convincing evidence that there are absolutely no software defects that would interfere with the software’s key functions. Almost all software built today is not high assurance; developing high assurance software is currently a specialist’s field.
High assurance and FLOSS are potentially a great match. We achieve high assurance in scientific analysis and mathematical proofs by subjecting them to peer review, and then worldwide review. FLOSS programs, unlike proprietary programs, can receive similar kinds of review, and many FLOSS programs achieve really good reliability figures for medium assurance. So it can be easily argued that stepping up to high assurance should be easier for FLOSS than for proprietary software. In addition, there are a vast number of FLOSS tools that support developing high assurance components, including PVS, ACL2, Isabelle/HOL, prover9, and Alloy (there’s lots more, see the paper for more details).
Yet it’s hard to find High Assurance Free-Libre / Open Source Software (FLOSS) components. To be fair, high assurance software components are exceedingly rare in the non-FLOSS world as well. But I suspect there are more than I’ve found, and I hope that people will help me by pointing them out to me. I’d like to know about such components for direct use, and also simply for use as demonstrations of how to actually develop high assurance software. Today, it’s nearly impossible to explain how to develop high assurance software, because there are almost no fully-published examples. Existing “formal methods successes” papers generally don’t publish everything including their specs, proofs, and code… which makes it impossible to really learn how to do it. And no, I don’t require that proofs prove every line of machine code; but showing how correspondance demonstrations are made would be valuable, and that’s currently not well demonstrated by working examples.
If you’re curious about the general topic, take a peek at High Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS). I’ve collected lots of interesting information; hopefully it will be useful to some of you. And let me know of high-assurance FLOSS components that I don’t already know about.
path: /oss | Current Weblog | permanent link to this entry