SPARK released as FLOSS (Free/ Libre / Open Source Software)!
The SPARK toolsuite has just been released as FLOSS (Free/ Libre / Open Source Software) by Praxis (its creator). This is great news for those who want to make software safer, more reliable, and more secure. In particular, this means that Tokeneer is now an open proof. If you haven’t been following this, here’s some background.
Software is now a part of really critical systems (ones that need “high assurance”), yet often that software is not as safe, reliable, or secure as it needs to be. I believe that in the long term, we will need to start proving that our very important programs are correct. Testing by itself isn’t enough; completely testing the trivial “add three 64-bit integers” program would take far longer than the age of the universe (it would take about 2x10^39 years). The basic idea of using mathematics to prove that programs are correct — aka “formal methods” — has been around for decades. There are a number of cases where formal methods have been applied successfully, and I’m glad about that. And yet, applying formal methods is still relatively rare. There are many reasons for this, such as inadequate maturation and capabilities of many formal methods tools, and the fact that relatively few people know how to apply formal methods when developing real programs. But what, in turn, is causing those problems? It’s true that applying formal methods is a hard problem that hasn’t received the level of funding it needs, but still, it’s been decades!
I believe one problem hindering the maturation and spread of formal methods is a “culture of secrecy”. Details of formal method use are often unpublished (e.g., because the implementations are proprietary or classified). Similarly, details about formal methods tools are often unshared and lost (or have to constantly re-invented). Biere’s “The Evolution from LIMMAT to NANOSAT” (Apr 2004) gives an example: “From the publications alone, without access to the source code, various details were still unclear… Only [when CHAFF’s source code became available did] our unfortunate design decision became clear… The lesson learned is, that important details are often omitted in publications and can only be extracted from source code. It can be argued, that making source code of SAT solvers available is as important to the advancement of the field as publications”
This “culture of secrecy” means that researchers/toolmakers often don’t receive adequate feedback, researchers/toolmakers waste time and money rebuilding tools, educators have difficulty explaining formal methods (they have no examples to show!), developers don’t understand how to apply it (and it has an uncertain value to them), and evaluators/end-users don’t know what to look for.
I believe that a way to break through this “culture of secrecy” is to develop “open proofs”. But what are they? An “open proof” is software or a system where all of the following are free-libre / open source software (FLOSS):
Imagine if we had a number of open proofs available. There could be small open proofs that could be used for learning (e.g., as examples and use in class exercises). There could be proofs of various useful functions and small applications, so developers could see how to scale up these techniques, directly reuse them as components, or use them as starting points but add additional (proven) capabilities to them. When problems come up (and they will!), toolmakers and developers could work together to find ways to mature the tools and technology so that they’d be easier to use (e.g., so more could be automated). In short, imagine there was a working ecosystem where researchers/toolmakers/educators, developers of implementations to be proved, and evaluators/end-users could work together by sharing information. I believe that would greatly speed up the maturing of formal methods, resulting in more reliable and secure software.
In this context, Praxis has just released the SPARK GPL Edition. This is their SPARK toolsuite (a formal methods tool) released under the GNU General Public License aka GPL (the most common FLOSS license). So, what’s that?
SPARK is a variant of the Ada programming language, designed to enable proofs about programs (by adding and removing some features of Ada). The additions are in special comments, so SPARK programs can be compiled by a normal Ada compiler like GNAT (which is part of gcc). The Open Proofs page on SPARK has some information on SPARK. The page What is Special About SPARK Contracts? gives a nice quick introduction to SPARK, which I will quote here. It points out that the Ada line:
procedure Inc (X : in out Integer);
just says there is some procedure “Inc” that may read a value X, and
may write it out, but that’s it.
In SPARK, you can add much more precise information, and the SPARK tools
can then check to see if they are true.
For example, if you say this using SPARK:
procedure Inc (X : in out Integer);
--# global in out CallCount;
--# pre X < Integer'Last and
--# CallCount < Integer'Last;
--# post X = X~ + 1 and
--# CallCount = CallCount~ + 1;
then the SPARK tools will ensure at compile-time (not run-time) that:
You can learn more about SPARK from the book High Integrity Software: The SPARK Approach to Safety and Security” by John Barnes. Sample text of Barnes’ book is available online. The open proofs page on SPARK has more information.
This means that the “Tokeneer” program is now an open proof. Remember, to be an open proof, a program’s implementation, proofs, and required tools have to be open source software. Tokeneer was a sample program written to show how to apply these kinds of techniques to actual systems (instead of trivial 5-line programs). The Tokeneer program itself, and its proofs, have already been released as open source software. Many of the tools it required are already FLOSS (e.g., fuzz and LaTeX for its formal specifications, and an Ada compiler to compile it). Now that SPARK has been released as FLOSS, people can examine this entire stack of software to make improvements in all the technologies, as well as learn from them and create improved implementations. No, this doesn’t suddenly make it trivial to make proofs about complex programs, but it’s a step forward.
If you are interested in making future software better, please help the open proofs project. You don’t need to be a math whiz. For example, if you know how to do shell scripting, please help us package some promising formal methods tools (like SPARK) so they are easy to install. It’s hard to get people to try out these tools (and give feedback) if they’re too hard to install. If you know of formal methods software that is rotting in some warehouse, try to get it released as FLOSS. I think all government-funded unclassified research software should be released as FLOSS by default, since “we the people” paid for it! If you’re interested in the latest software technology, try out a few of these formal methods tools, and release as FLOSS any small programs and proofs you develop with them. Send the toolmakers feedback, or write down their strengths and weaknesses to help others understand them. SPARK is a tool that can be used, right now, in certain circumstances. I have no illusions that today’s formal methods tools are ready for arbitrary 20 million line programs. But if we want future software to be better than today, we need to figure out how to mature formal methods technology and make it better-understood so that it can mature and scale. I think making top-to-bottom worked examples and starting points can help us get there.
path: /oss | Current Weblog | permanent link to this entry