High Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS)... with Lots on Formal Methods / Software Verification

by David A. Wheeler, 2006-06-02 (updated 2013-11-24)

This paper discusses some relationships between high assurance software (for security or safety) and free-libre / open source software (FLOSS). In particular, it shows that many tools for developing high assurance software have FLOSS licenses, by identifying FLOSS tools for software configuration management, testing, formal methods, analysis implementation, and code generation. It particularly focuses on formal methods, since formal methods are rarely encountered outside of high assurance. However, while high assurance components are rare, FLOSS high assurance components are even rarer. This is in contrast with medium assurance, where there are a vast number of FLOSS tools and FLOSS components, and the security record of FLOSS components is quite impressive. The paper then examines why this is the circumstance. The most likely reason for this appears to be that decision-makers for high assurance components are not even considering the possibility of FLOSS-based approaches. The paper concludes that in the future, those who need high assurance components should consider FLOSS-based approaches as a possible strategy. The paper suggests that government-funded software development in academia normally be released under a GPL-compatible FLOSS license (not necessarily the GPL), to enable others to build on what tax dollars have paid for, and to prevent the vast waste of effort caused by current processes. Finally, developers who want to start new FLOSS projects should consider developing new high-assurance components or tools; given the increasing attacks and dependence on computer systems, having more high assurance programs available will be vital to everyone’s future.

Introduction

This paper discusses some relationships between high assurance software (for security or safety) and free-libre / open source software (FLOSS). First, let’s define these key terms.

Definitions

Free-libre / open source software (FLOSS) is software whose license gives users the freedom to run the program for any purpose, to study and modify the program, and to redistribute copies of either the original or modified program (without having to pay royalties to previous developers). It’s also called libre software, Free Software, Free-libre software, Free-libre / Open source (FLOS) software, or open source software / Free Software (OSS/FS). The term “Free Software” can be confusing, because there may be a fee for the Free Software; the term “Free” is derived from “freedom” (libre), not from “no price” (gratis). More formal definitions of open source software and free software (in the sense of libre software) are available on the web. Examples include the Linux kernel, the gcc compilation suite, the Apache web server, and the Firefox web browser. Many FLOSS programs are commercial, while many others are not.

For purposes of this paper, let’s 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 (though I think all software developers should know a little about it). To develop high assurance software you must apply many development techniques much more rigorously, such as configuration management and testing. You need to use implementation tools you can trust your life to. And in practice, I believe that you need to use mathematical techniques called “formal methods” for a product to be high assurance, for the simple reason that it’s usually hard to create truly convincing arguments otherwise. A significant fraction of this paper covers formal methods, since they are rarely encountered outside of high assurance. There isn’t a single universal definition of the term high assurance, and products have been labelled “high assurance” without having any formal methods applied to them. But this definition should be sufficient for my purpose. Other terms used for this kind of software are “high integrity” and “high confidence” software.

Usually high assurance software is developed because of serious safety or security concerns. Strictly speaking, software by itself has no safety or security properties -- it can only be safe or secure in the context of a larger system. A nice discussion of this issue from the safety point of view is in Nancy Leveson’s book Safeware (see section 8.3). But software tends to control safety and security systems, and such software is often called “safe software” or “secure software”. For this paper I’ll talk about the security or safety of the software, with the understanding that this only makes sense if you understand the system that the software will be part of.

For purposes of this paper, the identity of the software’s supplier is not part of the definition of high assurance. By supplier, I mean the provenance (origin) and pedigree (lineage -- who the software passed through) of the software. By keeping the supplier identity out of the definition of high assurance, I can concentrate on technological issues. In reality, there may be some people who you wouldn’t trust even if they’d “proved” their code correct... so in practice it’s quite reasonable to ask questions like, “Who developed or modified the software? Can I trust them?” For both FLOSS and proprietary software, provenance and pedigree can be considered in exactly the same way -- in both cases, you’d consider who originally developed the software (in terms of each change), and who controlled the software from development through deployment to you. In particular, you’d consider who has rights to modify the software repository, and whether or not you trusted them. You might also consider how well the development environment itself is protected from attack. Don’t be fooled into thinking that FLOSS is “riskier” than proprietary software because it can be legally modified by anyone. Anyone can modify a proprietary program with a hex editor, too -- but that doesn’t mean you’ll use that modified version. The issue with suppliers is who controls your supply chain, and FLOSS often has an advantage in provenance and pedigree (because it is often easier with FLOSS to determine exactly who did what, and who has modification rights). But provenance and pedigree issues have to be handled on a case-by-case basis, and trying to cover those issues as well would over-complicate this paper. For example, the whole issue of “who trusts who” varies depending on the organizations and the circumstances. In an ideal world this wouldn’t matter, because the proofs would be true and could be rechecked everywhere. Given the massive move to globalization, I think that would be worth trying to make who created the software irrelevant. In any case, let’s concentrate on the technical aspects in this paper.

Contrasting levels of assurance

More generally, assurance is simply the amount of confidence we have that the software will do and not do the things it should and should not. Sometimes the things it should not do, what I call "negative requirements" , are the most important. Any particular piece of software can be considered by someone to be low, medium, or high assurance. This is obviously a qualitative difference; two products could be in the same assurance category, yet one be more secure than another.

For purposes of this paper, let’s define medium assurance to be software which doesn’t reach high assurance levels, but where there has been significant effort expended to find and remove important flaws through review, testing, and so on. Note that when creating medium assurance software, there’s no significant effort to prove that there are no flaws in it, merely an effort to find and fix the flaws.

Medium assurance software must undergo testing and/or peer review to reduce the number of flaws. Such mechanisms can be really valuable in reducing flaws, and eliminate a great many of them, but the normal method of using these mechanisms won’t guarantee their absence. You can eliminate some types of flaws completely by some activities, e.g., you can completely eliminate buffer overflows by choosing almost any programming language other than C or C++... but doing so would not eliminate all flaws! In particular, testing by itself is impractical to prove anything about real software. After all, exhaustively testing a program that just adds three numbers would take 2.5 billion years (assuming each number was 32 bits, you could run the program a billion times per second, and you used 1,000 computers for testing). Real programs are much more complicated than this, which is why testing by itself can’t reach the highest levels of assurance.

The differences between medium and high assurance (as I mean the terms in this paper) seem to confuse people, so let me contrast them directly. When developing a high assurance program, the program is presumed to be wrong (guilty) until a preponderance of evidence proves that it’s correct. When a medium assurance program is being developed, it is spot-checked in various ways throughout its development to try to detect and remove some of its worst defects. Medium assurance software development normally leave some defects in the program afterward. Few like the presence of latent defects, but few people are willing to pay for (or invest the time) for high assurance development techniques today in most software.

It’s reasonable to think that as technology improves, high assurance programs will become more common. But even today there are some situations where medium assurance is not enough. Typically this is where people’s lives, or the security of a nation, is at stake. In such cases, some of today’s customers need serious evidence that there are no critical defects of any kind. They need something different: High assurance.

High assurance challenges and standards

Ideally, all software would be high assurance, but ideally we’d all live in mansions. It’s very difficult to create truly high assurance software. The configuration management and testing requirements are usually more severe (and time-consuming) than those for other kinds of software. Applying formal methods requires significant mathematical training that most software developers don’t have, and can be very time-consuming.

Because of these challenges, high assurance software is usually only developed for critical security or safety components. When creating critical security or safety components, a number of regulations are often imposed.

High assurance software for security is the point of the Common Criteria for IT Security Evaluation (ISO standard 15408) when you select EAL 6 or higher -- and EAL 6 is really a compromise! For purposes of this paper, medium assurance software is in the EAL 4 to 5 range of the Common Criteria, so Red Hat Linux and Microsoft Windows would both be considered medium assurance products. I consider EAL 2 (or less) to be low assurance; EAL 3 is a compromise, but it’s basically low assurance.

Here are some other standards that are often mentioned in the security or safety world, which often impact this kind of development:

Organization of paper

The rest of this paper looks at FLOSS tools that can be used to create high assurance components (there are many), and FLOSS components that are high assurance themselves (they are rare). It then contrasts this situation with medium assurance -- there are many medium assurance FLOSS tools, and FLOSS components with impressive results. The paper then speculates why this is the circumstance, and then concludes.

Tools to create high assurance components

It turns out that there are a lot of FLOSS tools that can be used to help develop high assurance software. To prove that, I’ve identified a few important tool categories, and for each category I identify several FLOSS tools. The tool categories I discuss below are configuration management tools, testing tools, formal methods (specification and proof) tools, analysis implementation tools, and code generation tools.

There are many other categories of tools, and many other specific FLOSS tools, that are not listed below. But the discussion below should prove my point that there are many FLOSS tools that can be used to help develop high assurance components.

Configuration management tools

There are many FLOSS software configuration management (SCM) tools, indeed, I’ve written a review of several FLOSS SCM tools. (I’ve also written a paper discussing SCM and security.)

CVS is an old and still very widely-used SCM tool. I suspect that most software worldwide, both proprietary and FLOSS, is still managed by CVS as of 2006. Subversion (SVN) is the SCM tool rewritten as a replacement for CVS, and it’s widely used, too. But the list of FLOSS SCM tools is amazingly long, including GNU Arch, git/Cogito, Bazaar, Bazaar-NG, Monotone, mercurial, and darcs (see my paper for a longer list). Clearly, there’s no problem finding a FLOSS SCM tool.

Testing tools

All developers test their software, but high assurance software requires much more testing to gain confidence in it. But again, there’s a massive number of FLOSS tools that support testing. In fact, there are so many FLOSS tools for testing that there’s a website (opensourcetesting.org) dedicated to tracking them; as of April 2006 they list 275 tools! This ranges from bug-tracking tools like Bugzilla, to frameworks for test scripts like DejaGnu.

Many high assurance projects are required to meet specific measurable requirements on their tests. One common measure of testing is “statement coverage” (aka “line coverage”), the percentage of program statements that are exercised by at least one test. One problem with the statement coverage measure is that statements that have decisions, such as the “if” statement, can cause different paths. Thus, another common measure of testing is “branch coverage” the percentage of “branches” from decision points that are covered. Branch coverage has its weaknesses too, so there are many other test measures as well -- but statement and branch coverage are the two most commonly-used measures, so we’ll start with them.

Some experts believe that unit testing (low-level tests) should achieve 100% statement coverage and 100% branch coverage, with the simple argument that if you’re not even covering each statement and each branch, your testing is poor. Most others argue, however, that 80%-90% in each is adequate -- because the effort to create tests to meet the last percent is very large and less likely to find problems than by spending the effort in other ways. No matter what, in my opinion you should create your tests first and then measure coverage -- don’t write your tests specifically to get good coverage values. That way, you’ll often gain insight into what portions of the code are hard to test or don’t work the way you thought they would. That insight will help you create much better additional tests to bring the values up to whatever your project requires.

(Oh, and why measure both statement and branch coverage? It turns out it's possible to meet one without the other. For example, an "if" statement with a "then" clause but no "else" caluse might have all its tests yield true.. in which case all the statements are covered, but not all the braches are covered (the "false" branch is not covered). Normally, when you cover all branches you cover all statements, but there are special cases where that is not true. For example, if your program (or program fragment) doesn't contain any branches, or if there is an exception handler without any branches in its body, you can have all branches covered but not all statements covered. Exception handlers might be considered a branch, but that interpretation is not universal.)

There have been several recent developments in testing that improve test efficiency:

Even in the case of test case measurement, there are FLOSS tools that can meet this need. There are several FLOSS “test coverage” tools, such as gcov, that can report which statements or which branches were not exercised by your test suite.

Formal methods tools

Many software developers have no idea what “formal methods” are. Yet my definition of high assurance implies that we’ll usually need to use “formal methods” to create high assurance software. This section explains what formal methods are, shows that there are lots of FLOSS tools even in this area, and then discusses some of the implications.

Formal methods: Introduction

Formal methods, broadly, are the application of rigorous mathematical techniques to software development (see An International Survey of Industrial Applications of Formal Methods for a lengthier definition and discussion). Ideally, we’d like a rigorous mathematical specification stating exactly what we want the program to do and not do, and then prove all the way down to the machine code that the software meets the specification. This is normally hard to do, so various compromises are often made. Many have identified three different broad levels of the use of formal methods, in order of increasing cost and time:

The “levels” are a little misleading, because you can actually do things partially (perhaps only a part of the software is formally specified), and level 1 is somewhat ambiguous. But these levels give the basic flavor; there is a trade between rigor and effort.

Now we come to the decision of where to draw the line, and this isn’t an easy decision. For purposes of this paper, to count as “high assurance” there needs to be some carefully-reasoned explanation as to why the running code meets its key requirements. How much effort is needed for this justification depends on the risk you’re willing to take, and where you perceive the risks to be. Thus, while level 0 may be less costly, that is often not enough, so high assurance development often moves into level 1 and uses a focused application of level 2 on the parts that cannot be shown correct otherwise. Almost no one tries to prove all code down to the machine code; typically developers with such concerns will check the machine code by hand to ensure that it corresponds with the source code. Some may prove down to the source code, or at least the parts of the source code that are most worrisome. Others may use proofs to a detailed software design, and then use other less rigorous arguments to justify the source code. You can even back off further, using formal methods only for the specification (level 0), or not at all. In all cases, though, there needs to be some careful reasoning that convinces others that the code actually meets the key requirements, typically by showing a stepwise refinement from specification through to the code. Mantras such as “correct by construction” come into play in these kinds of systems.

We would love to formally prove that every line of code, down to the machine code, is correct; doing so has lots of benefits. Why is it so costly? Simply put, creating proofs is incredibly hard to do; often tools and knowledgeable humans must work together to create them. To prove code correct, you generally must write the code and proofs simultaneously (so that the code is in a form that is easier to prove). Requiring proofs also creates limits on the size of programs (and thus their functionality), because our ability to do proofs does not scale that well. Years ago, the old historical rule of thumb for the largest amount of code that can be reasonably proven correct all the way down to the code level was about 5,000 lines of code. Cleanly-separated components can be verified separately (e.g., a computer’s boot and initialization programs might be separable from an operating system kernel), and that helps. This rule of thumb is (I believe) historical; the tools for verifying code have improved, and good tools (including languages designed for provability) can help today’s developers go significantly beyond this scale. SPARK Ada’s developers in particular claim they can go way beyond this. But it’s not clear where the upper bounds really are, and it’s clear that formally proving code gets harder as the software gets larger. Typical operating systems have millions of lines of code and are growing fast, so no matter what the upper bound is, there is a real gap between typical commercial demands for functionality and the ability of today’s formal methods tools to verify it. Don’t expect Windows, MacOS, the Linux kernel, or *BSD kernels to be formally proved down to their code level. Proving only general models of code (instead of the system itself) eliminates this problem, but as I noted above, this doesn’t show that the code itself is highly assured.

Note that all formal methods have a basic weakness: They must make assumptions, because you have to start somewhere. In any such system, humans have to check the assumptions very, very carefully. If you start with a false assumption, a "proof" could produce an invalid conclusion. This problem -- that your assumptions may be invalid -- is a key reason that testing and other activities are still needed for high assurance software, even if you use formal methods extensively.

Another trade-off in formal methods is between expressiveness and analyzability. Fundamentally, any formal method has some sort of language, a set of axioms, and inference rules (the rules that let you determine if something else is true). A language that is extremely flexible (expressive) typically tends to be harder to analyze. As a result, there are many different languages, each better and different things.

For more information about formal methods, you can see the Wikipedia information on formal methods (particularly the main article on formal methods, automated theorem proving, and model checking), the Formal Methods Virtual Library, the NASA Langley Formal Methods Site, and the Formal Methods Education Resources. QPQ (“QED Pro Quo”) is intended to be an “online journal for publishing peer-reviewed source code for deductive software components”, and has links to various tools and papers. Aleksey Nogin’s “A Review of Theorem Provers” has a nice short summary comparing theorem provers. The Seventeen Provers of the World compares 17 proof assistants for mathematics, and some of which are relevant to software development. Most surveys seem to be old, unfortunately. A quick overview is available from the CMU 1996 paper “Strategic Directions in Computing Research Formal Methods Working Group” as E. Clarke and J. Wing’s 1996 “Formal Methods: State of the Art and Future Directions” [PDF]. I can point out “Notes on PVS from a HOL perspective” by Michael J.C. Gordon (1995), An Analysis of two Formal Methods: VDM and Z (1997), and Vienneau’s 1993 “A Review of Formal Methods” (even the full version is incomplete for its time, but at least it is easy to read). The History of the HOL System explains some of the convoluted history of LCF, HOL, and their various derivatives, and also notes some other systems. "Formal Methods for IT Security" (May 2007) has quick overview of tool types (one quibble: I agree that automatic theorem provers like prover9 take less effort than interactive tools like PVS and HOL, but automatic tools don't give less assurance - it's just that they cannot be effectively used on certain classes of problems). The “Handbook of Automated Reasoning” (Edited by J. Alan Robinson and Andrei Voronkov) is a survey. A short 2003 survey of tools commented on many tools, and the Formal Methods Framework report (1999) summarizes many tools. DACS’ list of formal methods literature is old, but it’s nicely focused on key works. Ingo Feinerer's "Formal Program Verification: A Comparison of Selected Tools and Their Theoretical Foundations" (2005) is a much more recent comparsion of formal methods tools (in this case, of the Frege Program Prover, KeY, Perfect Developer, Prototype Verification System). Griffioen and Huisman's 1998 work compares PVS and Isabelle; Zolda's 2004 work compares Isabelle and ACL2. Formal Methods Europe is an independent association with aim of stimulating the use of, and research on, formal methods for software development; their website has some summaries (though it has a very anemic list of tools as of May 2006). The mathematically-oriented papers Information technology implications for mathematics: a view from the French riviera and Deliverable 4.1: Survey of Existing Tools for Formal MKM compares tools’ mathematical foundations (these have the informal look of notes not intended for the masses, but they are still interesting). Johann Schumann’s Automated Theorem Proving in High-Quality Software Design discusses integrating automated theorem provers into larger development approaches and tools. High-Integrity System Specification and Design by Bowen and Hinchey is a collection of older key essays. Bowen and Hinchey’s “Ten Commandments of Formal Methods ...Ten Years Later” (IEEE Computer, January 2006) discusses previously-identified lessons learned (their “ten commandments” of their IEEE Computer April 1995 article) and argues that they have generally stood the test of time. Two oft-referenced formal methods advocacy pieces were published in IEEE Software: “Seven Myths of Formal Methods” by Anthony Hall (Sep/Oct 1990) and “Seven More Myths of Formal Methods” by Bowen and Hinchey (July 1995). Richard Sharpe argues that formal methods may be increasingly used in the future. Palshikar’s “An introduction to model checking” is a gentle introduction to that topic. Tony Hoare and Jay Misra have proposed a “Grand Challenge” effort to speed maturation of formal methods -- for their pitch, see Verified software: theories, tools, experiments (July 2005). The VSETTE conference of October 2005 has a response to this proposal, focusing on systemic methods for specifying, building, and verifying high-quality software. Shankar’s presentation The Challenge of Software Verification gives interesting comments on this challenge. The paper Formal specification and verification of data separation in a separation kernel for an embedded system (Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard, and John McLean of the Naval Research Laboratory) describes a very promising approach to proving all the way down to the code. These tools generally presume that you already understand the basics of formal logic; if you don't, books such as P. D. Magnus' "forall x" may be of use to you. (A serious problem in the U.S. is that many software developers have never studied discrete math, including logic, even though that's the basis of their field; few would allow a civil engineer to design a bridge without first learning calculus.) No doubt there are many other sources of information. Peter Gutman's article on "Verification Techniques" (a chapter of his thesis) is a much more pessimistic view of verification techniques, and has important insights on the limitations of formal methods and some other verification techniques.

After I wrote this paper, I discovered the very interesting list Free software tools for formal verification of computer programs by David Mentré. You should definitely take a look at this paper as well if you're interested in the topic! Trac's list of Theorem Proving systems identifies their licenses, many of which are FLOSS.

Here are some other lists of formal methods related tools:

Note - don’t treat “formal methods” as a checklist item for high assurance (oh look, some math, we’re done!). The point in high assurance is to identify the risk areas, and then use tools (like formal methods) to convincingly show that there isn’t a problem. There is more than a little overlap between those developing high assurance software and the research community; applying these techniques can be difficult for some domains, if you need to get really high levels of confidence for complex systems.

Formal methods: Categories of tools

There are many different kinds of formal methods tools, which I will group into these categories:

Note that these are very rough and imprecise categories. All formal methods tools must support some kind of specification notation, tools often have multiple capabilities, and there is a general trend of combining these tools into larger interoperable capabilities. A general discussion about issues in integrating tools is in the paper “PVS: Combining Specification, Proof Checking, and Model Checking”. Thus, any categorization is imperfect, but hopefully this division will help.

There are some interesting competitions, particularly for the automated tools. Here are the CASC results of 2008 using TPTP, for example.

It turns out that there are many FLOSS tools that support using formal methods, in all of those categories, as the following sections will show.

Formal methods: Specification tools

All formal tools have some sort of specification language, but some languages are often focused on higher-level specifications -- helping users enter, syntactically check, and cleanly display the specifications with a minimum of effort. These are often used for level 0 and 1 type of work (though they can be used for more -- often by devising connections to other tools). Here is a partial list of specification languages, and FLOSS tools that support them:

Formal methods: Theorem Provers/Proof Checkers

Here are FLOSS theorem provers and checkers (increasingly they are combined with model checkers, in which case I list them here and not under model checkers):

I have not included some tools in this list because I can't confirm that they have a FLOSS license. MAYA (originally part of Inka, something that supports graphs and connects to various other useful components) has no license that I can find; its "mathweb" component is clearly GPL'ed, but it's unclear it's entirely GPLed, and it depends on the proprietary Allegro Common LISP. RRL has no license I can find, and I can't download it. The lesson here is that if you develop a tool, you need to clearly identify its license so that others can use it.

Formal methods: Model checkers

Here are tools that are model checkers that at least say they are FLOSS:

Formal methods: SAT Solvers

The Boolean satisfiability (SAT) problem is the problem of determining if the variables of a given Boolean formula (where all variables can only be true or false) can be assigned in such a way as to make the formula evaluate to TRUE; alternatively, it's to determine if no such assignments exist (i.e., if it's unsatisfiable). SAT programs are low-level programs/algorithms that many other formal methods tools (like theorem provers) build on. In the last number of years there have been a lot of improvements in SAT solvers, resulting in improvements on anything built on them. SAT is a big area; SAT live tracks SAT goings-on. Here are some SAT surveys. There are a number of competitions, including the International SAT competition,
  1. MiniSat (MIT license). In the SAT 2005 competition, MiniSAT all by itself won Silver in the industrial categories SAT+UNSAT and SAT. MiniSAT is a "conflict driven solver", one of main (modern) styles of SAT solvers. SatELiteGTI is the combination of SatELite (used as a preprocessor) with MiniSat (the “GTI” component). SatELiteGTI won Gold in all three industrial categories: SAT+UNSAT, SAT, and UNSAT. I cannot find the license for SatELite, but the developers are making SatELite obsolete anyway by incorporating its capabilities into their updated version of MiniSAT.
  2. MarchDL (GPLv2+) is a SAT solver based on the "look-ahead" approach (one of the other main modern styles of SAT solvers). It won a prize at the 2007 SAT competition.
  3. Fast SAT Solver (GPL) is a SAT solver based on genetic algorithms.
  4. PicoSAT (MIT-style) is a recent and strong SAT solver. It did very well in the SAT'07 SAT Solver competition; Version 535 won the category of "satisfiable industrial instances" and came second on all industrial instances (satisfiable and unsatisfiable).
  5. Vallst (Reciprocal Public License, a GPL-like but stricter OSI-certified license) is another SAT solver. It won two golds and one bronze in the SAT 2005 “world championships”.

Formal methods: SMT Solvers

The Satisfiability Modulo Theories (SMT) problem is an extension of the SAT problem (above). Basically, given expressions with boolean variables and/or predicates (functions that take potentially non-boolean values yet return boolean values), determine the conditions that would make it true (or conversely, show it's false). An SMT solver adds one or more "theories" for various predicates, e.g., it might add real numbers (adding predicates like less-than and equal-to), integers, lists, and so on. SMT solvers are sometimes implemented on top of SAT solvers.

Many other systems build on top of SMT solvers. The SMT-LIB: The Satisfiability Modulo Theories Library and SMT-COMP: The Satisfiability Modulo Theories Competition are important to many SMT solver implementors. Here is a list of SMT solvers (current and abandoned, FLOSS and not).

Examples include:

  1. Ergo (Alt-Ergo) (CeCILL-C license) is an automatic theorem prover focused on program verification. It supports equational theory (=) and linear arithmetic, and it's relatively small. One significant problem is that this is licensed under the extremely rare CeCILL-C license, not the CeCILL license. I can't find a major FLOSS organization who has ruled that the CeCILL-C license is FLOSS (including the FSF, OSI, Debian, or Fedora). This license is intended to be FLOSS, but that is as yet untested.
  2. CVC3 (BSD) is "an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination." CVC3 is the successor to CVC Lite. The license of earlier versions of CVC3 included some highly-controversial non-standard clauses, one of which was an "indemnification" clause that to some appeared highly dangerous to any user or distributor. Fedora eventually ruled that the license was "non-free" and thus unacceptable. I contacted the developer, and although it took a long time, I'm delighted to report that as of October 2009, the CVC3 license was changed to a simple, normal BSD license, resolving the issue.
  3. Gappa (CeCILL or GPL, libraries LGPL) is a tool "intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic. It has been used to write robust floating-point filters for CGAL and it is used to certify elementary functions in CRlibm. It requires Coq support library 0.8. ("Why" can invoke Gappa.)
  4. The Decision Procedure Toolkit (DPT) (Apache license) is "a system of cooperating decision procedures for answering satisfiability queries. The DPT implementation in OCaml comprises a DPLL-style SAT solver with theory-specific decision procedures".
  5. Arithmetic and Boolean solver (ABSolver) (Common Public License 1.0) is a framework for combining other tools to solve mixed arithmetic and Boolean problems, and is designed to make it easy to add new solvers. ABSolver is remarkable in its ability to solve non-linear problems. However, "Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure" (Journal on Satisfiability, Boolean Modeling and Computation 1 (2007) 209–236) warns that ABSolver's "currently reported implementation uses the numerical optimization tool IPOPT (https://projects.coin-or.org/Ipopt) for solving the non-linear constraints. Consequently, it may produce incorrect results due to the local nature of the solver, and due to rounding errors."
  6. Argo-lib (GPLv2) is an SMT-LIB solver. It is "a C++ library which provides a generic support for using decision procedures in automated reasoning systems and also support for several schemes for combining and augmenting decision procedures. This platform follows the SMT-lib initiative which aims at establishing a library of benchmarks for satisfiability modulo theories. ARGO-lib platform can be easily integrated into other systems, but it should also enable comparison and unifying of different approaches, evaluation of new techniques and hopefully help advancing the field. ARGO-lib follows a range of techniques and different systems. The latest version of ARGO-lib provides support for DPLL(T) scheme and for producing object-level proofs."
  7. OpenSMT (GPLv3) is a "compact and open-source SMT-solver written in C++, with the main goal of making SMT-Solvers easy to understand. OpenSMT is built on top of MiniSAT (http://minisat.se)... Currently OpenSMT supports only the theory of Equality with Uninterpreted Functions [QF_UF]... In the future we plan to extend OpenSMT with other theories."
  8. Fx7 (BSD-like license).
  9. haRVey SMT prover has two branches: haRVey-FOL (LGPL) and haRVey-SAT (BSD license). From the website: "Current developments aim at merging both branches, and provide one uniform tool. The main issues are the logics are different (haRVey-SAT is multi-sorted, haRVey-FOL is not) [and] there is some technical and theoretical difficulties to combine first-order provers within a Nelson-Oppen scheme. So, haRVey is still in development stage...". haRVey downloads are available (but watch out, some links are broken, so it can be hard to find).
  10. STP (MIT license) is a Decision Procedure for Bitvectors and Arrays. "STP is a constraint solver (also referred to as a decision procedure or automated prover) aimed at solving constraints generated by program analysis tools, theorem provers, automated bug finders, intelligent fuzzers and model checkers. STP has been used in many research projects at Stanford, Berkeley, MIT, CMU and other universities. It is also being used at many companies such as NVIDIA, some startup companies, and by certain government agencies. The input to STP are formulas over the theory of bit-vectors and arrays (This theory captures most expressions from languages like C/C++/Java and Verilog), and the output of STP is a single bit of information that indicates whether the formula is satisfiable or not. If the input is satisfiable, then it also generates a variable assignment to satisfy the input formula. We are currently adding the theory of finite sets and the theory of uninterpreted functions to STP." There is a SourceForge home page for STP. It uses MINISAT.

Formal methods: Other Tools

Here are FLOSS tools that are don’t easily fit into the above categories:

Formal methods: Unmaintained tools

These tools appear to be no longer maintained, but they may still be useful as basis for new work:

Formal methods: Proprietary tools

Not all formal methods tools are free-libre / open source software (FLOSS). I thought I should briefly note a few, so that people can save time instead of trying to track down their licenses.

"Proprietary" simply means that the program is not FLOSS, and thus users do not have the right to use the software for any purpose, view the source code, modify it, and redistribute it (modified or not). Many tools were developed at public expense at universities, but are nevertheless proprietary. Even if the software's development was completely paid for using public funds, do not assume that software will be released as FLOSS to the public. In some cases there are "demo" binaries of the tool available to the public, but the source code is not distributed and/or there are significant limitations on the tool's use.

The following are proprietary tools: Barcelogic, Boolector, HySAT, Spear, Yices, and Microsoft's Z3. ESC/Java and Simplify are not FLOSS; they were once widely distributed, but since they were never FLOSS, when their company's direction changed they became abandoned, legally risky to use, and impractical to maintain. Similarly, Z/Eves was once widely distributed, but it was never FLOSS, so when its distributor stopped distributing it, users had no legal recourse.

MathSAT is not FLOSS, even though it has the text of the GPL and LGPL licenses in its release. Alberto Griggio explained the real situation to me in 2008: "It is linked with the GNU multiprecision library GMP, which is covered by the LGPL. So, the sourcecode doesn't have to be available, and in fact at the moment it is not, sorry. The tarball includes a copy of the GPL as well as of the LGPL, because, as far as we know, you must ship a copy of the LGPL if you link against an LGPL'd library, and the LGPL itself requires that you also ship a copy of the GPL. Sorry if this was unclear,

Epigram has no clear license statement. I've sent an email requesting that this be clarified.

CBMC is a model-checker with an almost free license, so it's probably not FLOSS. It allows change, but requires notification before installation; that certainly fails Debian's requirements (e.g., it fails the "Desert Island" test). Once again, it's frustrating that people want to create new licenses, please STOP!

Bogor is non-commercial-use only, and thus not FLOSS.

HCMC is a model-checking tool, but I haven't found a clear license statment about it.

Formal methods: Commentary

My point is simply that there are many FLOSS tools in this space, and I think I have proven that convincingly. This is certainly not a complete list; see the resources listed above, the Yahoda verification tools database, CoLogNET’s list of automated reasoning tools , the CASC entrants, Formal Methods Education (FMEd) Resources tools page, the Formal methods virtual library, Automation of reasoning net links, and Freek Wiedijk’s overview for even more programs. There are many non-FLOSS formal methods tools, just as there are non-FLOSS SCM and testing tools, but that does not invalidate my point.

Many of these FLOSS tools are considered very strong, innovative, and/or have been used for serious applications. Spin and the Boyer-Moore Theorem Prover (the basis of ACL2) each received the ACM’s prestigious Software System Award, which recognizes a “software system that has had a lasting influence”. Both have been used for extremely important applications, from checking space probe algorithms through microprocessor design. PVS is also widely considered to be one of the better tools of its kind. Otter has been used to find new proofs previously unknown to mathematics. HOL 4 and Isabelle are widely used among these kinds of tools. MiniSat, Paradox, and Vallst have won awards in recent competitions against other similar tools. Alloy is a new tool, but I think it’s pretty innovative.

One type of tool I’m not including are probabilistic / statistical / Monte Carlo model checkers, such as PRISM (GPL license). They appear to be valuable for medium assurance, but I am skeptical that they are appropriate for high assurance. One tool in this space I should note is GMC (GPL license, likely), which is a highly experimental Monte Carlo-based software model checker for the gcc compiler suite. Open-Source Model Checking explains more about GMC. GMC is very experimental, and does not appear suitable for development use at this time; I note it here because it embodies some very interesting ideas, for those who are interested in the up-and-coming research. Monte carlo model checkers have great promise for medium assurance, but because they only cover statistical likelihoods (not all possible situations), I would be nervous about using any of them for high assurance.

Sadly, many tools have completely disappeared from the world because they were not released under FLOSS licenses. What’s particularly galling is that many governments pay for academics to develop code, yet fail to require releases of that code (that they paid for!) under FLOSS licenses. In my mind, this is shameful; if my taxes paid for the tool, then I should have the right to see, use, and improve it, unless there is strong and specific evidence that an alternative license would be better for that particular circumstance. FLOSS licenses allow others to study, use, improve, and release those original or improved versions, and are thus a much better vehicle for making continued research possible. Instead, often a tool is released (if it’s released at all) only as a proprietary binary file (which is unmodifiable and will eventually be unrunnable) or possibly as restricted source code; in either case its license often has lots of anti-FLOSS restrictions (such as you can’t modify it or you can’t use it for a commercial purposes). The tool often cannot be used for commercial purposes except through special licensing deals; that might sound fine, but in practice this generally squelches research through trial commercial use, and it also prevents distributors (such as Linux distributors) from making the tool widely available. Then either (1) the academic loses interest, or (2) a proprietary company builds on the tool and tries to build a business based on it. If the original academic loses interest, then no one else (even other academics!) has the rights to build on that code. The second option (proprietary commercialization) sounds good, but remember, we've had decades of almost uniform failure in trying to sell formal methods tools (Most restaurant starts fail, never mind niches like this where there are few users and the tools take time to learn.) In the end, the project usually fails. In either case, the software ends up being unavailable to all -- even if government funds were used to develop it. This is incredibly wasteful, and in my opinion this is one of the primary reasons people don’t use formal methods as often: most of the research work is locked up in software with proprietary licenses that is eventually thrown away. A company can do what it likes with its own money, of course, but if it will not sell it as a proprietary product, I think they should at least release it as FLOSS so others can build on it and improve the field. Governments have no such excuse; it is their citizens’ money they are squandering. I believe that, with a little creativity, governments could ensure that such projects can continue and grow.

Obviously, it is possible to have proprietary tools with long support, but investigate any such vendor very carefully. If you use such tools, depending on proprietary versions can be a big risk; if the company goes out of business (which is historically very likely), your largest cost suddenly depends on an unsupportable tool. In large markets, open standards help -- by having multiple competing implementations which you can switch between, competition lowers costs and incentivizes improvement. There are a few standards in this area (e.g., those for Z and VDM). But depending on competition often fails when there is a thin market, as in the case of formal methods tools. You might consider requiring the vendor to escrow their code as FLOSS if they decide to stop selling or supporting their product, so at least you can have a support option if the vendor leaves the business (as most do). This isn’t an empty concern; here are some examples where a proprietary tool license has caused problems for its users:

In contrast, some of the tools that have been released as FLOSS have resulted in incredible benefits to the world, and lower risks for their users. ACL2, Isabelle, HOL4, and splint (for example) come from very long lines of research, and their continued use today demonstrates that releasing software developed during academic research under FLOSS licenses can have tremendous, long-lasting benefits. (The computer algebra system Maxima has demonstrated the same thing; it’s been around since the late 1960s and is still actively maintained.) The NuSMV project specifically re-implemented the SMV tool, so they could get the benefits of being a FLOSS project (permitting extensions like TSMV, an extension of NuSMV to deal with timed versions of circuits). Any company doing research would be wise to consider releasing its code as FLOSS -- if it’s research, they can often receive far more than they release. I think it would be much wiser to require that government-funded software development in academia be released under a FLOSS license under usual circumstances. That way, anyone can start with what was developed through government funds and build on it, instead of starting over.

Indeed, in some ways, FLOSS is an ideal way to commercialize formal methods tools. Formal methods tools require people to learn and apply new skills, so for bigger projects you generally need someone to help you understand how to apply the tool. Thus, the FLOSS commercial model of “give away the code and sell support services” is especially easy to apply in this area. And if the commercial company flops, the work is still available for future research or for combining with other components.

I do not think that within a few years suddenly everyone will be using formal methods, for a variety of reasons. But I do think that over the next many years we will see a very gradual increase in use of these tools in very critical areas.

Of course, one challenge is that assurance tools are often not assured themselves. Assurance tools could even be maliciously undermined; see the discussion under compilers for more about “trusting trust” types of attacks. Here are few items related to assuring the assurance tools:

Tools can’t do everything for you; humans have to help create proofs, and they often have to try many different paths to find the proof. This haiku by Larry Paulson expresses some of the challenges of that process:

Hah! A proof of False.
Your axioms are bogus.
Go back to square one.

(Yes, many tools are designed to counter bogus axioms, but the basic point is still true. Namely, anyone trying to prove properties of real systems often struggles and has to restart several times, going through many different approaches, before succeeding.)

Analysis implementation tools

A different issue is how to run the various formal methods tools listed above. A few of them are implemented in widely-available languages also used for other purposes (like C, C++, or Java). Obviously, they’ll need an operating system, and usually need other common tools like text editors. (Warning: Most analysis tools run on Linux/Unix and are either not available for Windows, or only work on Windows with an emulation tool like Cygwin -- making the tool slower.) But there are already well-known FLOSS implementations for these, so we don’t need to discuss them in more detail.

However, specification and proof systems are often built “on top” of other (less common) programming languages. These other languages are often specialized themselves, and in some cases using the specification or proof tools also involves interacting directly with the underlying implementation tools as well (e.g., to control/“drive” the proof system).

Programming languages which are functional programming languages, or have a functional programming subset, are very common for these purposes. A functional programming language is simply a language where assignment is not (normally) used, and thus there are no “side-effects” -- instead, functions accept values and return values (like a spreadsheet does). There are many arguments for the advantages of such systems, but one reason is simply that such systems make it possible to use much more of the arsenal of mathematics. Functional languages usually have built-in support for lists and other constructs useful for the purpose. J Strother Moore’s position is that all highly-assured software should be written in a functional programming language, because it is much easier to prove properties about programs written in them. (Most widely-used languages are “imperative” languages, including C, C++, Ada, Java, C#, Perl, Python, PHP, and Ruby. Techniques for proving programs in imperative languages are known; C. A. R. Hoare’s 1969 paper on Floyd-Hoare logic did so, as did Edsger Dijkstra’s weakest precondition work that was part of his 1975 work on predicate transformers. Moore argues that their complexities are not worth it, and that using a functional approach makes proofs much easier.)

In some cases it’s hard to figure out where to place some language. In particular I’ve placed Maude here, but Maude could arguably be considered an analysis tool (and be placed above). In any case, there are many useful FLOSS implementations of these tools too:

Code generation

Clearly, you need to have a way to execute the highly-assured source code... which requires either a compiler or interpreter.

If you write code in C or C++, it quite common to use the gcc compiler suite (GPL license), which is FLOSS. Developers of high-assurance software who choose to use C or C++ often use gcc as well, so clearly there are FLOSS tools covering these languages.

However, programming languages often used for other assurance levels don’t work as well for high assurance. Here are comments on some programming languages if you are interested in high assurance:

Sometimes the best approach is to create domain-specific language, use that to define at least part of your system, and then create a code generator for your language. This makes it much easier to use languages you might not be able to use otherwise. This can be very effective, but you must still decide how to implement the code generator (and the rest of the code, if applicable), and you must somehow verify that the generated program does what you want.

There are a lot of guidance documents out there on how to use various languages to implement high assurance software, or have more general guidance on development. ISO/IEC JTC 1/SC 22 has a list of some related documents. If you're interested in how to develop secure software, see my book developing secure programs. Some relevant documents include:

In all cases, you want to use the tools in a way that tries to catch as many mistakes as possible before the code gets out to the user. For example, you would normally turn on essentially all warning flags, and you would normally set up guidelines on how to use the language (to avoid things that are known to be problematic).

Compilers are hard to verify too. There’s been some research progress for formally verify that a compiler correctly implements its language, but it’s not ready for typical use yet with real compilers; current work focuses on tiny toy languages, and even these are difficult. The article Qualification of Software Development Tools From the DO-178B Certification Perspective notes some of the challenges in qualifying tools directly (from the DO-178B perspective). An approach more commonly used today is to have the compiler generate code, and then do hand-checking to make sure that the generated code matches the source code. This is obviously not ideal, but it easily beats writing the assembly code by hand, and if the compiler directly supports it (the GNAT Ada compiler does) this is not to hard to do. Using a widely-used compiler, and avoiding “stressing” the compiler, reduces the risk of accidentally inserting an error into the final machine code to a very small amount, and hand-checking can detect such errors.

Intentional malicious subversion of compilers turns out to be much more difficult to counter. An Air Force evaluation of Multics, and Ken Thompson’s famous Turing award lecture “Reflections on Trusting Trust” showed that compilers can be subverted to insert malicious Trojan horses into critical software, including themselves, and it’s shockingly hard to counter the attack. Thompson even performed the attack under controlled experimental conditions, and the victim never discovered it. For decades it’s been assumed that this was the “uncounterable attack”. Thankfully, my own academic work on Countering Trusting Trust through Diverse Double-Compiling shows how to counter subversive compilers, so even this nasty problem is now solvable.

High assurance components

There are very few high assurance FLOSS components available. A later section will discuss this, but for now, here are the closest to high assurance FLOSS components that I’ve been able to identify (some are quite a stretch):

There’s much more available if you are simply looking for a real-time operating system (RTOS) kernel, and aren’t really looking for high assurance. eCos is a FLOSS RTOS, for example, and there are several projects that create “real-time” versions of the Linux kernel. Also, if you want a hypervisor, Xen is very popular and is FLOSS. But none of these are high assurance.

Recently several proprietary Multiple Independent Levels of Security (MILS) separation kernels, have become available. It’s not clear that there are FLOSS implementations becoming available as well, though clearly it’s possible (the TCX project might do so, but it’s not clear that the code will be FLOSS, and it’s not clear that it will be sufficiently capable to be useful... it’s currently not available). The July 2004 draft separation kernel protection profile, which defines the requirements for the separation kernel, is a Common Criteria-based document requiring EAL 6 plus augmentation. More information is about the MILS architecture is available in the August 2005 Crosstalk article about the MILS architecture, and you can look at John Rushby’s papers that discuss this in more technical detail. Greve, Wilding, and vanFleet have defined a formal specification for a MILS separation kernel using ACL2 [code]; Alves-Foss and Taylor comment on it. I could imagine a variant or re-implementation of Xen meeting this, however, Xen is designed for performance instead of trying to meet these requirements.

Medium assurance

There are a lot of FLOSS tools to help achieve medium assurance, and there are also many FLOSS programs that achieve medium assurance. Let’s look at them, so we can contrast the situation of FLOSS tools and components in medium assurance against those in high assurance.

FLOSS tools for medium assurance

There are a number of FLOSS tools to help find defects in programs. These include splint and flawfinder; my Flawfinder home page identifies many of these program analysis tools, such as PMD for Java. The Linux kernel developers even developed their own static analysis tool to examine the kernel (kernels are very different from application programs, and their common failure modes are different than applications’). But note that these tools are generally designed to to look for specific common defects and defects that are easy for tools to find. These could have some value in high assurance applications as well, since these tools could quickly filter out problems before bringing out the “big guns”. But these tools aren’t enough; a program can pass every such tool and still have serious flaws. It’s also worth noting that these tools often have many false positives (“bug” reports that aren’t really defects at all).

I should note that it’s been widely and repeatedly proven that the most efficient method for finding and repairing defects, in terms of found and repaired defects per person-hour spent, are peer reviews -- groups of people actually looking at the code. There are various processes for this, going under names such as “software inspections” (Fagan and Gilb have different processes sharing that name). Peer reviews are low-tech, and often not exciting to do... but they’re so effective that anyone leading a software project should be interested in them. Andy German’s 2003 paper “Software Static Code Analysis Lessons Learned” reports that “independent code walkthroughs are the most effective [static code analysis] technique for software anomaly removal [, finding] up to 60 percent of the errors present in the code.” I co-edited and co-authored an IEEE Computer Society Press book, “Software Inspection: An Industry Best Practice”, which if you can get it (it’s now out of print) presents lots more information about it. The Formal Technical Review Archive lists many other texts. For high assurance, 60% is not 100%, but for medium assurance it’s fantastic. The known effectiveness of peer review explains why the “many eyeballs” idea of FLOSS really can work.

FLOSS components at medium assurance

Several FLOSS implementations have undergone traditional medium assurance evaluations. There are at least two Linux distributions that have undergone Common Criteria evaluations (Red Hat and Novell/SuSE) at what I would term medium assurance levels. Similarly, the cryptographic library OpenSSL has undergone FIPS evaluation. To be fair, a program that has not undergone a Common Criteria evaluation process might be more secure than one that has, and a program that underwent a lower EAL Common Criteria evaluation might be more secure than one at a higher level. The Common Criteria is a standardized set of processes for evaluating the security of software, and higher EAL values add more evaluation processes. A product that has not gone through the higher levels might still be very secure -- all we know for sure is that no one has paid for the higher-level evaluation to be performed.

Unsurprisingly, many other popular FLOSS programs and systems have undergone many tool-based evaluations searching for flaws as well:

Looking more broadly, it is clear that there are many FLOSS projects which take significant steps to search for and remove defects.

General issues: FLOSS and medium assurance

Many experts have concluded that FLOSS has a potential advantage over proprietary software when it comes to security or reliability, though not all FLOSS programs are more secure than their competitors. This is borne out by many studies of actual FLOSS programs, which show that FLOSS does very well in terms of security and reliability (often much better than their proprietary competition).

Several papers and presentations discuss the general issue of security and FLOSS, noting some potential advantages of FLOSS. Examples of such sources include “Issues of Dependability in Open Source Software Development” (ACM SIGSOFT, Software Engineering Notes, May 2002) the section on open source software in my book Secure Programming for Linux and Unix HOWTO, and my presentation on open source software, security, and software assurance. There’s no guarantee that a FLOSS program will be more secure than a proprietary program -- do not mistakenly think otherwise. However, there are potential advantages to FLOSS, for example:

There’s certainly lots of evidence that FLOSS programs can be more reliable and secure than their proprietary competition. My paper “Why Open Source Software / Free Software (OSS/FS or FLOSS)? Look at the Numbers!” has lengthy lists of studies showing that various FLOSS programs do very well in terms of reliability and security; see them for more. For example:

In addition, many FLOSS programs have now built-in countermeasures to counter security problems in other components. "Security Enhancements in Red Hat Enterprise Linux (beside SELinux)" by Ulrich Drepper describes many mechanisms in Red Hat Enterprise Linux that counter or limit damage even if another component has a vulnerability. I'm a strong advocate of this belt-and-suspenders approach to security; by all means, eliminate vulnerabilities in components, but also deploy defensive measures so that unfound vulnerabilities are less serious.

In short, there is every reason to believe FLOSS components can be at least as reliable and secure as proprietary components, if not more so.

Why are high assurance FLOSS components so rare?

So now we come to an interesting question -- why are high assurance FLOSS components so rare? There are very few real high assurance components available, period, so we would expect there to be few FLOSS components. Yet FLOSS still seems under-represented.

Jeffrey S. Norris and Poul-Henning Kamp’s “Mission-Critical Development with Open Source Software: Lessons Learned” (IEEE Software) clearly shows that people do develop mission-critical systems at NASA using FLOSS components; they relied heavily on FLOSS components, reporting that they kept the project within budget and resulted in a more robust and flexible tool. The text suggests that these were medium assurance applications, but the lessons are worth considering at any assurance level.

Key vendor-differentiating software is usually not FLOSS. If a company or government uses a particular piece of software as part of their competitive advantage, they should usually not release it at all (as either proprietary or FLOSS). But most software is actually not company or government differentiating, and even if the software as a whole is, some of its pieces are still typically commodity components. A company that sells software licenses to others will often not choose to release that program as FLOSS -- but if they have customers that use the software, sometimes those users find that using a FLOSS program instead has its advantages. Components that are commodities shared among many devices, such as a separation kernel or real-time operating system kernel, would make sense as FLOSS.

There’s fragmentation in the high assurance market (e.g., different detailed requirements in different standards and different circumstances) which probably doesn’t help. But this harms other approaches for developing software too, and increasingly this problem is being recognized and addressed.

Clearly high assurance components are normally required to go through expensive independent evaluations (due to various regulations). But again, that is a hurdle that has been overcome before, many times.

FLOSS is widely represented in other areas. There are many medium assurance FLOSS programs that have better security or reliability records than competing proprietary programs. FLOSS is certainly well-represented by tools to create medium and high assurance components as well. A vast number of FLOSS tools are available, in fact, for creating high assurance components (and many have already been used for the purpose, including ACL2, SPIN, and GNAT).

It’s even more bizarre when you compare software proofs with the way normal mathematical proofs are made. “Normal” mathematicians publish their proofs, and then depend on worldwide peer review to find the errors and weaknesses in their proofs. And for good reason; it turns out that many formally published math articles (which went through expert peer review before publication) have had flaws discovered later, and had to be corrected later or withdrawn. Only through lengthy, public worldwide review have these problems surfaced. If those who dedicate their lives to mathematics often make mistakes, it’s only reasonable to suspect that software developers who hide their code and proofs from others are far more likely to get it wrong. Joyner and Stein's "Open Source Mathematical Software" (Notices of the AMS, Nov. 2007) notes how well FLOSS matches the methods in mathematics for producing high-quality results, and includes some interesting quotes. Andrei Okounkov (2006 Fields medalist) notes that "I think we need a symbolic standard to make computer manipulations easier to document and verify... An open source project could, perhaps, find better answers to the obvious problems such as availability, bugs, backward compatibility, platform independence, standard libraries, etc... I do hope that funding agencies are looking into this." Neubüser notes that with proprietary software "two of the most basic rules of conduct in mathematics are violated: In mathematics information is passed on free of charge and everything is laid open for checking.”

The nonsense that FLOSS is more vulnerable to insertion of malicious code doesn't wash, either. Any FLOSS or proprietary program can be modified - just get a hex editor. The trick is to get the maliciously-modified program into a customer's supply chain, and that's much harder: You have to get the malicious code into the FLOSS component's trusted repository, and not noticed (else it will be removed). "Application Security: Is the Backdoor Threat the Next Big Threat to Applications?" by Scott Berinato (in CSO Online) interviewed security researcher Chris Wysopal of Veracode. "As detection and scanning technology gets better at finding the accidental coding errors like buffer overflows, Wysopal believes the malicious will turn more and more to using backdoors--holes in programs usually intentionally programmed in to allow access to an application." Wysopal goes on to note that "The lifetime of a backdoor in open source is very short. It’s measured in weeks. The lifetime of a backdoor in closed source is measured in years. The many eyes concept of open source is working to detect backdoors. We found that in most open source cases, the malicious or accidental opening was detected in a matter of days, sometimes a few weeks. But every backdoor in the binary of proprietary software was there for years or an indeterminate length of time. It never happened that closed source backdoors were discovered in months. With an old one, Borland Interbase, we saw seven years worth of versions where a backdoor was there." The interviewer was surprised, and appears to have been unaware of FLOSS trusted repositories and how they work. He asked, "with so many people manipulating open source code, the number of backdoors to detect must be exponentially higher than proprietary systems, and the potential virulence, of spreading backdoors, must be much higher with open source?" Rather than explain this, Wysopal went immediately to the measure that mattered: "when we looked at special credential backdoors, the four biggest were all closed source products." The notion that FLOSS always makes you more vulnerable to backdoors is contrary to real world experience.

Yet the source code and proofs for high assurance programs are almost never published publicly at all (never mind being released as FLOSS). This means that many "high assurance" programs fail to exploit the methods used by mathematics to strengthen claims. Thus, there’s a good case to be made that high assurance FLOSS programs would tend to be much higher assurance than proprietary programs, because there could be a worldwide review of the proofs. At least for safety-critical work making FLOSS (or at least world-readable) code and proofs would make sense; why should we accept safety software that cannot undergo worldwide review? Are mathematical proofs really more important than software that protects people’s lives?

Several potential explanations come to mind, and I suspect only the last two are really true:

  1. Is high assurance too expensive to do using FLOSS? Certainly, developing high assurance components requires a great deal of personnel time, but this is true for other assurance levels too (though they place their effort in different areas). As I demonstrated in my paper “More than a Gigabuck”, FLOSS development approaches are quite capable of employing massive amounts of development effort. In 2001, the old Red Hat Linux 7.1 represented more than one billion U.S. dollars of development effort, and that is a small fraction of today’s FLOSS development effort. It’s true that independent evaluations are normally required at high assurance levels, and they require cash payments that may be harder to get. Yet the fact that other FLOSS programs have undergone independent evaluations (such as Common Criteria evaluations for Red Hat Linux and Novell/SuSE, and FIPS evaluation for OpenSSL) suggests that this is probably not a real barrier either. At least, it’s not a barrier if there’s an economic model to support it, which brings us to our next point.

  2. Is there no possibility of a rational economic model for FLOSS high assurance? FLOSS is a licensing model that is typically associated with certain development and distribution models. FLOSS is not a single business model; instead, there are many different business and non-profit economic models that can be employed by FLOSS projects. Business/economic issues in FLOSS are discussed in many places, including Bruce Perens’ “The Emerging Economics of Open Source Software” and Eric Raymond’s “The Magic Cauldron”. Indeed, there’s a micro-industry of economists who analyze FLOSS business models, because they think FLOSS “shouldn’t” work (due to failure to understand it) but it does anyway. There are many different business models for FLOSS, but for our purposes they all involve either making money and/or reducing expenditures. The “make money” models typically do this by charging for warranties, indemnification, support, or related services (the latter is sometimes an example of “commoditizing your complements”). The “reducing expenditures” models typically involve cost sharing or cost avoidance, and often look like consortia with an unusually efficient legal framework (Apache and the X consortium are examples). Linux distributors typically do both; they sell support and services (to make money), while exploiting the far lower expenditures to compete against established proprietary organizations. Lots of organizations do this in many other areas, so unless there’s something especially unique to high assurance, it’s hard to believe the approach can’t work for FLOSS.

    Commercial organizations often support FLOSS projects when it’s in their financial interest to do so. Essentially all work in major FLOSS projects like the Linux kernel and Apache website are done through software developers paid to do so. Even in high assurance tools there are examples; ACL2 is financially supported by many corporations; AMD, Rockwell Collins, and Sun Microsystems are three of them, and they’ve supported ACL2 because they’ve used it in microprocessor development. Not all FLOSS projects are financially supported like this, of course, but today’s corporations are willing to do so when it’s in their own interests.

    Certainly, there’s a big problem that there is a very high “initial fee” to create and evaluate an initial product, but that’s true for other FLOSS products too. For years it was assumed that modern compilers and operating system kernels were “too hard” for FLOSS; that myth has been completely blown. And besides, these also mitigate against proprietary suppliers; proprietary suppliers have difficulty raising enough money in these cases too. These initial fees could be addressed by having several large integrators or users (who use lots of high assurance components) pool their funds to create such a component, with the idea that they’ll reduce their overall costs. Such organizations manage to create consortia in other areas; there’s little reason they can’t handle this too.

    Of course, such organizations could claim that they’re worried about “free riders” who use the component without paying for initial development, but that’s missing the economic point. Nearly all costs for software are not in development -- they are in maintenance. One reason FLOSS projects do so well is that many people copy the software (starting out as “free riders” ), but a small fraction eventually contribute valuable information (bug reports, patches, etc.)... because they must to cost-effectively use the product. As a result, releasing a component as FLOSS allows the maintenance costs -- the majority of all costs -- to be shared, even among those who did not pay for initial development. This means that a proportion of those who start as “free riders” eventually help share the maintenance costs, reducing the maintenance costs for all. Since maintenance is the primary cost, there is a reasonable economic rationale for releasing software this way (in some cases). The initial investors have an additional reason to invest: they will decide what will be implemented first, and how, and many have decided that this additional control is worth the initial investment. That doesn’t mean that FLOSS is always the best economic approach, but it does mean that it’s an approach worth exploring.

    The only obvious true difference I see are liability issues, but this could help FLOSS implementors. Some people may think that the liability costs of high assurance software will make it “impossible” to use FLOSS -- yet this misses the point. Liability is something customers are willing to pay for, and even better for a FLOSS business, customers would typically have to pay for liability protection and support. AdaCore, who support the GNAT Ada compiler, depend on this and seem to be doing well. So this makes high assurance unusually tempting for a FLOSS business -- customers can try out the product (making it more likely to be considered), but will be required to pay the supplier through laws and contracts requiring liability protection.

    Many different economic models could be devised; let’s imagine just one. A consortium could be established to create such high assurance components, and give a liability price break to its founders -- with others paying a higher (but reasonable) price to gain liability protection and support (perhaps the costs go down after paying double the costs of the initial founders). Such a consortium could encourage code and monetary contributions through a variety of means (e.g., by using the LGPL license, or using a dual-license approach with the GPL license being one of them and a for-pay license being the other). Organizations like major government integrators might be interested in such a consortium, because it would be a way to reduce their expenditures... and they would not want to have to compete against those in the consortium, if they were outside it, since those inside might have lower future expenditures. Many variations of these ideas are possible, of course. There seems to be little evidence that there’s no economic model for FLOSS high assurance components.

  3. Is the expertise too specialized and hard to acquire? Developing high assurance components truly is a specialized art. More importantly, there are few published examples of how to actually do it, so it’s very difficult to learn how to do it. In fact, there are reasons to fear that some of this knowledge at the highest end is disappearing and will need to be re-discovered when its practitioners die. The lack of published proven programs is a real problem!

    Halloran and Scherlis’ paper “High Quality and Open Source Software” notes that in the medium assurance realm, the “quality and dependability of today’s open source software is roughly on par with commercial [proprietary] and government developed software”, and then asks, “what attributes must be possessed by quality-related interventions for them to be feasibly adoptable in open source practice?” They then note several attributes, which would presumably apply to high assurance as well. They note that FLOSS projects generally bootstrap on top of other FLOSS tools, in part due to ideology, but also because it lowers barriers for new participants and enables developers to fluidly shift their attention from tool use to tool development/repair. As noted above, there are FLOSS tools available. But in their conclusions they note these criteria: “(1) an incremental model for quality investment and payoff (e.g., incrementally adding analysis support, test cases, measurement, or other kinds of evidence collection), (2) incremental adoptability of methods and tools both within the server wall and in the baseline client-side tool set, (3) a trusted server-side implementation that can accept untrusted client-side input, and (4) a tool interaction style that is adoptable by practicing open source programmers (i.e., that does not require mastery of a large number of unfamiliar concepts).” Based on this list, they conclude that “With the exception of testing technology and some code analysis technology, these requirements suggest that some adaptation will be required before adoption is possible for tools that embody, say, lightweight formal methods approaches or advanced program analysis approaches. Clearly, any technique or tool is not feasibly adoptable if it requires a major (client-visible) overhaul of a project web portal, collaboration tools, development tools, or source code base. Discernible increments of benefit from increments of participant effort is key to adoptability.” In short, formal methods require a lot more training before the benefits can accrue -- and because they aren’t incremental (and are rare), it’s harder to do.

    I think the difficulty of acquiring the necessary skills before being able to do any work is a real and valid issue. This is a real problem for using these techniques to develop proprietary software, too! But there is such experience, so while valid I don’t think that’s the primary issue.

  4. Have few considered the possibility? It may be that many potential customers/users have simply failed to consider a FLOSS option at all. In fact, I think this is the most likely reason of all.

    People tend to do what they know how to do, and repeat approaches they've used before. In many cases, the people who are interested in developing a small high-assurance component have done this before and used a proprietary approach... and since that is what they did before, they do not think to consider an alternative.

    For example, I went to a detailed economic review in 2006 of one particular high assurance effort, where the big contrast was between “government-owned” and “commercial proprietary software vendors”. The possibility of a FLOSS approach (e.g., establishing a consortia to create a FLOSS implementation) simply never entered any decision-maker’s mind! When an alternative is never considered, it’s not surprising when it isn’t chosen. The developers of high-assurance software are quite familiar with FLOSS, and in fact are developers of it themselves (just look at all the FLOSS tools for high assurance!). But the decision-makers about high-assurance software are not the same people, and in fact tend to be very conservative people because they’re worrying about security and safety. Conservatism about technology makes sense for these stakes, but that doesn’t mean that valid economic alternatives should be ignored.

    The TCX research project is even more bizarre, because it specifically notes that it hopes to aid both the proprietary commercial and the “open-source” sectors. The TCX project even mentions planning to release its results “using a philosophy similar to the open source approaches”. But the information published so far does not suggest that the materials will ever be released under a FLOSS license, nor have I found evidence that this option was considered. Licensing was not even a criteria in its tool survey, yet depending on a language only implemented by a proprietary tool would be certain to drive away many FLOSS developers. The TCX published works so far include a mathematical model, which could be used as a basis for further work, but it is only released as a file in (uneditable) PDF format, with no rights to make improvements. There is no FLOSS license granting rights to improve any of the works released as of April 2006, even though the TCX text seems to imply that the MIT and BSD-new licenses might be appropriate for them. There’s also no published rationale for why the works will not be released under a FLOSS license; given the many pages discussing other project decisions, the failure to discuss the licensing of the results (where dissemination is the whole point of the project) is jarring. The reader is left with the impression that the ideas of using FLOSS licensing terms to release their work, and working with the larger FLOSS community, never occurred to the project leaders.

    In short, I think this is the primary explanation: the FLOSS option does not seem to be even considered as a potential strategy. I don’t think every high assurance component of the future will be FLOSS, in fact, I expect there to be a continued number of proprietary high assurance products. But there also seems to be no special reason that it should be ignored. I suspect that the number of FLOSS high-assurance products will grow as decision-makers start to consider FLOSS options as well. In the long term, I expect a mixture of proprietary and FLOSS components, just as this is already true for compilers, operating system kernels, web browsers, web servers, and so on.

Conclusions

There are a large number of FLOSS tools available for creating high assurance components. There are a vast number of tools supporting configuration management, testing, formal methods, and code generation. This paper focused on formal methods, since this is distinctive for high assurance, and showed that there are many tools in this space (both research and industrial-strength). Some of these tools are ACL2, HOL 4, Isabelle, Otter, ProofPower, ZETA, CZT, Spin, NuSMV, BLAST, and Alloy. (I find ACL2, Otter, Spin, BitC, and Alloy especially interesting, though with different reasons for each.)

In contrast, few high assurance components are FLOSS. After looking at the options, the most likely reason for this appears to be that decision-makers are not even considering the possibility of FLOSS-based approaches. Decision-makers should consider FLOSS-based approaches as future high assurance components are needed, including the possibility of creating consortia, so that a FLOSS-based strategy can be chosen where appropriate.

Governments should require that government-funded research normally release all software it develops under a FLOSS license, unless the government is convinced that in this particular case there is a better alternative. This is amply demonstrated by the many discarded and underused proprietary projects in these fields; the waste and lost opportunity alone is enough to justify this. More fundamentally, governments use money from their people to do research; it is only fair to ensure that all the people (who pay for the research) can reap the benefits, unless they will be better served some other way. If software research results are FLOSS, then anyone can start with what was developed and build on it, instead of starting over. The Open Informatics Petition text goes farther and suggests that governments simply mandate this no matter what. I will not go that far; I think there are good reasons for cases where government-funded research should not be released as FLOSS, but the petition does explain in more detail the advantages of this approach. Most detractors are concerned about this being required on all research. If you simply say that FLOSS is a wiser “default”, I think a much better balance is struck than the current system in many countries. The Open Informatics web site has more information. Requiring FLOSS release does not prevent commercialization; there are many FLOSS-based businesses, and many FLOSS licenses permit adding extensions and making the result proprietary. The many success stories from FLOSS-based approaches (e.g., ACL2, Security-Enhanced Linux, etc.) suggest that releasing software under FLOSS licenses is a very effective way to improve tech transition and establish sustainable research. Since the GPL is the most common FLOSS license (in formal methods tools and in general), whatever FLOSS license is used in this case should at least be GPL-compatible -- that way, research efforts can be combined into larger works as needed. For the same reason, I would recommend that one of the “classic” FLOSS licenses be used in most cases (i.e., MIT, BSD-new, LGPL, or GPL) -- they are well-understood, and can be combined as necessary.

Finally, developers who want to start new FLOSS projects should consider developing or improving high-assurance components or tools (including tools that combine other tools). Improving the user interfaces, capabilities, or integration of tools would be very valuable. Sample assured components, especially ones that are useful (like separation kernels or RTOSs) would be of value too, both for potential users and for others developing such programs (because there are few publicly-available examples that people can experiment with and learn from). These are technically interesting, and given the increasing attacks and dependence on computer systems, having more high assurance programs available will be vital to everyone’s future.


You can see David A. Wheeler’s home page, http://www.dwheeler.com

You should also see the Open proofs web site.