Packaging status

From Openproofs

Jump to: navigation, search

Contents

Goal

A key first step of the open proofs project is to package key FLOSS formal methods / high assurance tools for easy installation. There are many promising tools, but if they're hard to install they are unlikely to be used.

Obviously, easy installation is not enough. Tools must be also be easy to learn and use for real problems - which implies a need for documentation and tool refinement. And since there are many tools, documents that help you choose between them (and use them together) are important too. But the first step is to make them easy to install.

The initial goal is to package promising tools so they can easily be installed on various systems. We have started by focusing on Fedora Linux (RPM-based), which is one of the most popular FLOSS systems in the U.S. and has lots of security measures (so it's widely used already by people who care about security). We've focused on ensuring that users can simply select the tools using their normal GUI package installer, without traversing multiple websites to download software. In all cases, this requires requires creating packaging, and/or sending bug reports so that they are integrated together.

We're also looking at Debian and Ubuntu (both deb-based), as you can see below. Again, the intent is to get FLOSS formal methods / high assurance tools into their standard repositories, so that users can easily install these tools. This is not to exclude other systems; the more the merrier. SuSE/Novell, Gentoo, and FreeBSD are especially of interest. It'd be nice to do this for Windows and MacOS too, but many of the tools are not designed to work with these operating systems, so it would likely be a lot more work to port them, and there's also no centralized repository to submit them to.

Please help us!!

Please look at the list of packages below, and see what's not already packaged. Let us know which one you're doing (by updating this page). Then, create a package for it! You normally don't need to be an expert in the program you're packaging; creating a package primarily involves knowing how to create a package file. Read its installation documentation, and go! When done, submit it to the project's repository; repeat til done.

LICENSES MATTER. Repositories for many FLOSS distributions will not accept non-FLOSS licenses, and it may not be legal to redistribute some programs. Nonstandard licenses often make it impossible to combine tools to create larger useful works, which defeats the purpose of this site. In addition, they can take a very long time to go through legal review, and may be rejected for a variety of reasons. So if you can, encourage the tool-makers to use standard FLOSS licenses instead of odd ones. Often lawyers add clauses because "it's fun to write contracts"; they often do not understand the ramifications of the text, and unless a license has been widely vetted through public examination and use, it's probably a terrible idea. (see http://www.dwheeler.com/essays/gpl-compatible.html)

Tool creators should try to limit themselves to these licenses: MIT, BSD-new, LGPL, and GPL; they are widely-used and known to be GPL-compatible (the GPL is the most popular FLOSS license). The Apache 2.0 license isn't so bad, but note that it's incompatible with GPL version 2 (though it is compatible with GPL version 3). At the very least, please use a license already approved by the OSI, the FSF, Fedora, and Ubuntu.

Promising FLOSS tools supporting open proofs

Below is a list of FLOSS tools that look especially promising, and who is packaging them. For more about these projects, as well as information about other tools, see: http://www.dwheeler.com/essays/high-assurance-floss.html In the table below:

  • "IN": Was already in the given repository before openproofs.org work begin
  • "DONE": It is now in that repository, due to our efforts.
  • "DONE BY OTHERS": Now in the repository, by those unconnected to openproofs.org
  • "Name": Name is currently packaging it.
  • "-": no one has checked if it is in their repository. For Ubuntu and Debian, please help us determine which ones are already in the distributions and which are not.
  • "?": It's not in that repository, and no one is working on it.

Please pick anything with "?" and package it!! Let us know by modifying this table. Note: "In repository" for our purposes may mean that it's ready for the next release; it might not be in the current release.

Tool Fedora Debian Ubuntu Comments
Prover9 / MACE4 DONE Tim Colles <timc, at nf.ed.ac.uk> IN IN intrepid Has a text interface, and a separate GUI (separate package).
Coq DONE: Alan Dunn IN IN Implemented in OCaml. Current version is 8.2.
Why / Caduceus / Krakatoa DONE: Alan Dunn IN IN Implemented in OCaml. Caduceus and Krakatoa build on top of Why. Why, in turn, can call lots of other things, such as PVS or Coq (Coq is especially common). They can use a number of different lower-level theorem provers, need to include at least one OSS one they can use. Note that Caduceus is being superceded by Frama-C/Jessie.
CVC3 DONE ? IN PROGRESS

CVC3 is a theorem prover that once had a non-OSS license, but in Oct 2009 switched to BSD (a well-known OSS license). This is used by Why. Initial work done by Jerry James (jjames's Fedora Homepage

Alt-Ergo DONE: Alan Dunn in progress (See Debian) In OCaml, used by Why. Nonstandard GPL-incompatible license (CeCILL-C, not CeCILL); Fedora accepts it as FLOSS. Current version (in Fedora rawhide, soon in 10, 11, is 0.9)
STP DONE: David A. Wheeler ? ?This is very capable for certain kinds of problems (fixed-width calculations). "Why" can generate SMT-LIB; the STP version in the SourceForge SVN repository can process SMT-LIB.
Zenon DONE: David A. Wheeler ? ? Used by old versions of Why, but Why no longer supports it. Zenon can generate Coq traces, but only in an obsolete version of Coq. Its capabilities have been mostly exceeded by CVC3 and alt-ergo, and there is no evidence that it is being maintained. Unless its development re-energizes, this may be removed in future versions of this list (as being superceded by other tools).
Frama-C / Jessie Packaging completed. ? ? Jessie lets you analyze C, but it requires Frama-C. This was very difficult to package, but for Fedora (at least) those problems have been overcome, and there is ongoing work to simplify future packaging. APRON adds some nice capabilities, it can be used without APRON. APRON in turn depends upon the MLGMPIDL library (now packaged) and PPL.
KeY ? ? ? Java verification tool.
Alloy ? ? ? Looks fantastically useful as a spec tool. Package version 4, not version 3. Implemented in Java (Must use openjdk; gcj doesn't seem to work for it). Uses MiniSAT, so Wheeler packaged that for Fedora. Alloy has its own SAT package, but MiniSAT is faster. Alloy is a slightly controversial tool; it gives up perfect provability in exchange for excellent automation - for many circumstances, this is worthwhile.
ACL2 Draft package by Alan Dunn. See [1] and review request. IN IN DWheeler says: Uses Common Lisp. Pick a CL that works. I have a start on this. GNU Common Lisp (gcl) is fast, but current gcl won't compile ACL2, so I switched to sbcl (Steel Bank) - performance results from ACL2 suggest that sbcl is the second-fastest (compared to gcl).
ADunn says: Perhaps we could also consider Clozure Lisp (which is not yet packaged/known to be packageable... license works at least)?
PVS DONE (pvs-sbcl) by jjames ? ? Uses Common Lisp. This is not a Linux virtual server.
MiniSAT2 DONE: David A. Wheeler IN IN SAT solver, used by others (inc. Alloy)
Kodkod Alan Dunn, in progress ? ? Constraint solver that translates high-level constraint problems in relational logic to SAT problems and then employs SAT solvers (MiniSAT, zchaff, SAT4J) to solve them, used by Alloy. Alan says: Unfortunately, the way this tool links to alternate solvers is to include copies of them and recompiling them, which is prohibited for packaging. The only allowed solver in the current form would thus be SAT4J, which doesn't have the same capabilities as MiniSAT does in this package.
BLAST Submitted, awaiting review ? ? Must be configured so it doesn't require proprietary tools (e.g., Simplify and Vampyr) for packaging. (It can use them where available.) Don't go to BSD, use the more recent EPFL release of epfl.ch's BLAST
SPARK ? ? ? A variant of Ada that supports proofs of programs. The "Tokeneer" program was proved with SPARK. GPL license. Here's the Open Proofs page on SPARK
HOL 4 ? ? ? Debian and Ubuntu have HOL88, but not this version (not the same).
Isabelle/HOL ? ? ?  
HOL Light ? ? ? Debian and Ubuntu have HOL88, but not this version (not the same).
DiVinE Wheeler packaged, review in process ? ? DiVinE can read models specified in ProMeLa (as used in the SPIN tool). It appears that "DiVinE Multi-Core" uses a 2-clause BSD license, with GPL and LGPL libraries; if so, then this is clearly FLOSS (these are all known FLOSS licenses). This is not Automatic IP configuration detection for laptops
mCRL2 ? ? ? mCRL2 implements micro Common Representation Language 2. It is a specification language that can be used to specify and analyse the behaviour of distributed systems and protocols. mCRL2 is based on the Algebra of Communicating Processes (ACP) which is extended to include data and time. Boost 1.0 license, which is OSI-approved.
fuzz / tex-zfuzz DONE David A. Wheeler ? ? Actively being used
E DONE: David A. Wheeler ? ? Why uses haRVey, which will require E
Proof General DONE.ININEmacs-based front end for proof assistants that provides a common interface to different provers. Proof scripts can be edited in a buffer and executed as desired. Supports a wide variety of provers (ACL2, Isabelle, Coq, HOL among others), though the exact capabilities vary per prover. Integrates with Emacs tags capabilities through tools for proof scripts (eg. coqtags for Coq proof scripts). Alternative version as an Eclipse plugin is also in the works.
SAT4J IN (in unstable) (in jaunty - release 4/09) Java-based SAT solver. Ships with Eclipse (and must be unbundled...)
Parma Polyhedra Library IN IN (0.9 in unstable, 0.10 in stable) IN Library allows for numerical abstractions - representations of finite sets of points in terms of constraints on their position values - in ways amenable to formal methods and verification.

Many of these programs depend on implementation languages with multiple implementations like ML and Common Lisp - packagers will need to compare implementation possibilities. For example, many of the HOL variations (HOL 4, HOL Light, Isabelle) need an ML implementation, and preferably one that can store its state. Poly/ML is already packaged for Fedora, and can do this, but it'd be good to compare the various ML implementations.

Other potential FLOSS tools supporting open proofs

Here are some "maybes" that would be great to package as well:

  • veriT/haRVey: We've had extensive discussions with the developers of what was originally named harRVey, and is now named veriT. Originally, haRVey-FOL and haRVey-SAT were separate programs, but their developers merged them. This merged result should be examined, but if it's as useful as appears likely, it should be packaged. "Why" can use the older version of haRVey; the Why developers intend to add support for veriT soon. That could be great, as it would add another automated FLOSS prover to "Why". veriT requires a few other packages, e.g., E and miniSAT 1.
  • Gappa: Automated prover for proving constraints on floating point numbers. Invokable from why. Very useful for programs with floating point arithmetic.
  • Sugar - Constraint solver
  • Saturn - statically and automatically verify properties of multi-million line software systems
  • ProofPower - HOL variant and standard Z support.
  • Daikon: ? - Invariant-finder. Not really a formal methods tool _directly_, but a way to help use of formal methods tools
  • JMLEclipse: ? - Front-end for JML
  • JACK, Java Applet Correctness Kit (Cecill C licence): ?
  • Decision Procedure Toolkit on SourceForge
  • APRON (LGPL and GPL) - for static analysis of the numerical variables of a program by Abstract Interpretation
  • MOPS, which can do model-checking of a big system. Model Checking An Entire Linux Distribution for Security Violations discusses MOPS' use on the Linux kernel. Compare this with BLAST - do we want to package both? BLAST and MOPS are similar, but compared to BLAST, "MOPS trades precision for scalability and efficiency by considering only control flow and ignoring most data flow, as we conjecture that many security properties can be verified without data flow analysis".
  • Forge/JForge: ?
  • SNARK: ?
  • CSIsat - Submitted to Fedora, awaiting review. Needed for BLAST.
  • picoSAT - In Fedora. Needed for CSIsat.
  • iProver: ?
  • Darwin: ? - http://combination.cs.uiowa.edu/Darwin/
  • Paradox / Equinox: ? - http://www.cs.chalmers.se/~koen/folkung/ - promising prototype; Equinox is an automated theorem prover for pure first-order logic with equality, built on SAT (miniSAT)
  • Gandalf (Not the image processing system) - this is another promising automated theorem prover. However, we already have several generic automated provers (prover9, E), and for theory-specific ones, CVC3 covers a far broader array of theories, and alt-ergo works well too. In addition, although Gandalf did well in years past, there's little evidence of continuing development. Originally Gandalf was on the list to be packaged first, but now that CVC3 is available, it has been removed from the top priority list. It'd be nice to package, though.
  • Murphi: ? - Lots of branches/variants, hard to track down what to _USE_
  • Deputy: ? - C variant, not really a FM tool
  • CCured: ? - C variant, not really a FM tool
  • Cyclone: ? - C variant, not really a FM tool
  • CPAchecker - Described by its author, the BLAST maintainer, as "a better BLAST".

This is not meant to be an exclusive list. There are many different tools, many focused on different capabilities, and it's hard at this point to identify "winners". Feel free to package something not on this list, and let us know! At this point, it's best to package the more promising ones, and through use the best ones will fall out. But if you can show that some are much more promising than others, please let us know - it'd better to not package clearly inferior products, so that people can simply use the best ones. Many of these were selected by examining the results of the various competitions, such as Conference on Automated Deduction (CADE) Automated Theorem Prover (ATP) System Competition (CASC), and selecting the OSS tools that were the best in at least one category.

For lists of tools, see Free software tools for formal verification of computer program and High Assurance (for Security or Safety) and Free-Libre / Open Source Software (FLOSS)... with Lots on Formal Methods.

For discussion comparing some of these tools and their notations, see The Seventeen Provers of the World.

Uncertain/unreviewed licenses

The following are very unclear:

There are other tools that might be of interest; their legal status needs to be reviewed, as well as whether they're worth packaging:

Not Free/Libre/Open Source Software (FLOSS)

The following are not FLOSS tools, even though some are widely misunderstood as being FLOSS:

  • Spin claims on its front page that it is an "open-source software tool", but this claim does not appear to be true (in the sense that the term "open source" is normally understood). Spin is released under the Spin license. This license has not been certified as being an open source software license by the OSI, nor as Free Software license by the FSF; these are usual the sources for the definitions of "open source software" (aka "free/libre software"), including those used by the U.S. federal government and the state of California. Fedora has examined it and determined that it is not a FLOSS license. Debian's preliminary examination of the Spin license seemed to come to the same conclusion (it's poorly worded, making it difficult to determine what is legal to do). Thankfully, the data format accepted by Spin (ProMela) can be accepted by other tools too, so users can switch to another tool.
  • zchaff is not FLOSS (it is released for "non-commercial use only"). zchaff is nowhere near as good as MiniSAT, anyway.
  • "Simplify" (part of ESC/Java) is not FLOSS. It has been abandoned, and its license is in legal limbo.
  • YiCES is NOT FLOSS. Its publisher does publish other FLOSS tools (e.g., PVS), but YiCES is not one of them.
  • Modex is released under a "non-commercial use only" and "no redistribution" license.

Here's a table of promising tools with license issues, though they may be worked out:

NuSMV ? ? ? Symbolic model checker. Here is an RPM file that could be a useful starting point. Can use miniSAT (version 1, though). Most code is uncontroversially FLOSS (main code is LGPLv2.1 and cudd library uses a BSD license), but the two files cudd-2.4.1.0/cudd/{cuddAddOp.c,cuddBddOp.c} have a non-OSS "educational purposes only, no monies exchanged" license; as written, those license may even forbid grants and student scholarships. Work ongoing to clarify this.

You also need to be careful of dependencies. Some repositories (e.g., Fedora's main repository) require that both the program, and anything it requires, be FLOSS.

How to Create packages

There were many different places to learn how to package for Fedora, and that made it hard to learn. For creating Fedora packages, see the CreatingPackageHowTo page at the Fedora wiki. Much of this information is relevant for other RPM-based distributions, such as Novell/SuSE.

For deb-based Linux distributions, such as Debian and Ubuntu, see the Debian New Maintainers' Guide and Ubuntu packaging guide for more information.

Please make sure you can start the program exclusively using a GUI, even if it's a text-only program. For Linux/Unix systems, please use the desktop entry specification and perhaps the icon theme specification from FreeDesktop.org.

Unfortunately, many of these programs don't follow standards, such as the Filesystem Hierarchy Standard, so you may need to modify them so they can integrate smoothly with other programs.


Comparing tools

There are a number of different tools, but no comprehensive document explaining their pros and cons. There are some useful documents, such as A comparison of PVS and Isabelle/HOL.

Potential Packagers

Here are people who have expressed that they might be interested in doing this. Please let me know of something specific you'd like to do!

  • Tim Colles <timc at inf.ed.ac.uk>
  • Jerry James jjames Jamezone
  • Jeremy Long <Jeremy.Long at gmail.com>
  • Earl Sammons <esammons at hush.com>
  • Justin Acquaro <jacquaro at gmail.com>.
  • Greg KH (for Gentoo, maybe SuSE) <greg at kroah.com>
  • Jesus Arocho <jesus_arocho at comcast.net>
  • Ed Schneider
  • Jonathan Marsden - interested in packaging SPARK for Debian/Ubuntu

Anyone in the Fedora Formal Methods SIG (Special Interest Group) is a potential packager.

Personal tools