Ceci est une ancienne révision du document !


Free software tools for formal verification of computer programs


by David Mentré <dmentre @ linux-france.org>

Version 1.23- 2011-12-11

We are now living in the XXIst century. We should no longer make software as in the sixties or seventies, with a few tests. We are now able to make software without any bugs (well, without most of them, see below). This is possible using specialised tools called formal tools. Such tools are able to match a computer program against a specification, i.e. a formal description of the expected behaviour of the program. If the specification is correct and the formal verification can be done, then the program is guaranteed to be bug free. Of course, this is the ideal case and we are far from guaranteed bug free programs in the real world. But, as developer of free software, we should try to be as close as possible of this goal. As a first step, I list here free software tools that can help verification of computer programs.

Note: David A. Wheeler as made a lengthy paper on High Assurance (for Security or Safety) and [[free_-_libre|Free-Libre / Open Source Software (FLOSS)… with Lots on Formal Methods]]. You should read it if you are interested in the subject!

Sub-pages :


Tools to help verification of real programs


I have put under this category software that can be applied to real world programs (in language like C for example) to prove properties on them.

Brillant


Set of free software tools aiming at implementing the B method, for both software and hardware.

[[im_prove|ImProve]]


ImProve is an imperative programming language for high assurance applications. ImProve uses infinite state, unbounded model checking to verify programs adhere to specifications. Yices (required) is the backend SMT solver. ImProve compiles to C, Ada, Simulink, and Modelica.

Boogie


Boogie is a program verification system that produces verification conditions for programs written in an intermediate language (also named Boogie). The intermediate language is easy to target from source languages such as Spec#, C#, or even C.

Saturn


The goal of the Saturn project is to statically and automatically verify properties of large (meaning multi-million line) software systems. The focus of much of our work is simultaneously achieving scalability, precision, and a straightforward way of expressing analyses that is easy to reason about. We plan to use these techniques to verify properties of a full operating system.


[[frama_-c|Frama-C]]


Frama-C is a suite of tools dedicated to the analysis of the source code of software written in C.

If you have a C program and need to

  • validate it formally
  • look for potential runtime errors
  • audit or review it
  • reverse engineer it to understand its structure
  • generate formal documentation

One or more of the following Frama-C tools may be of assistance to you:

  • A parser, a type checker and source level linker for C code optionally annotated with ACSL formulas.
  • A set of builtin static analysis plugins:
    • A runtime error detection plug-in based on abstract interpretation techniques
    • A dependencies computation plug-in
    • An interactive value analysis plug-in
    • A Use/Defs computation plug-in
    • A slicing plug-in
    • A weakest precondition calculus plug-in based on Floyd-Hoare logic
  • List of alarms detected by the value analysis is “uninitialized access, use of a dangling pointer, overflows in signed integer arithmetics, invalid memory access, invalid comparison of pointers, division by zero, undefined logical shift, overflows in conversions from floating-point to integer, infinite or NaN resulting from a floating-point operation, undefined side-effects in expressions”


CIL


CIL is a framework to analyse and manipulate C programs.


Splint


Splint is a tool for statically checking C programs for security vulnerabilities and coding mistakes. With minimal effort, Splint can be used as a better lint. If additional effort is invested adding annotations to programs, Splint can perform stronger checking than can be done by any standard lint.


Cqual


Cqual is a type-based analysis tool that provides a lightweight, practical mechanism for specifying and checking properties of C programs. Cqual extends the type system of C with extra user-defined type qualifiers. The programmer adds type qualifier annotations to their program in a few key places, and Cqual performs qualifier inference to check whether the annotations are correct. The analysis results are presented with a user interface that lets the programmer browse the inferred qualifiers and their flow paths.


CCured


CCured is a source-to-source translator for C. It analyzes the C program to determine the smallest number of run-time checks that must be inserted in the program to prevent all memory safety violations. The resulting program is memory safe, meaning that it will stop rather than overrun a buffer or scribble over memory that it shouldn't touch. Many programs can be made memory-safe this way while losing only 10$-160% run-time performance (the performance cost is smaller for cleaner programs, and can be improved further by holding CCured's hand on the parts of the program that it does not understand by itself). Using CCured we have found bugs that Purify misses with an order of magnitude smaller run-time cost.


CHIC


CHIC is a modular verifier for behavioral compatibility checking of software and hardware components. The goal of CHIC is to be able to check that the interfaces for software or hardware components provide guarantees that satisfy the assumptions they make about each other. CHIC supports a variety of interface property specification formalisms.


Smatch!!!


Smatch is C source checker but mainly focused checking the Linux kernel code. It is based on the papers about the Stanford Checker.

Basically, Smatch uses a modified gcc to generate .c.sm files. The .c.sm files are piped through individual Smatch scripts that print out error messages.

For example, someone might want to write a Smatch script that looked for code that called copy_to_user() while the kernel was locked. If the script saw a place that called lock_kernel() then it would record the state as locked. If the script saw a place that called unlock_kernel() it would set the state to unlocked. If the state was locked and the script saw a place that called copy_to_user() the script would print out an error message.


Sparse


Sparse, the semantic parser, provides a compiler frontend capable of parsing most of ANSI C as well as many GCC extensions, and a collection of sample compiler backends, including a static analyzer also called “sparse”. Sparse provides a set of annotations designed to convey semantic information about types, such as what address space pointers point to, or what locks a function acquires or releases.

Stance


Features:

  • Error-finding tool based on static analysis.
  • Target language is C (ANSI C99), but extensible to C#/C++/Java.
  • Full ANSI C99 support, including most GNU C extensions.
  • Modular structure, easy extensibility, fast development.
  • Easy to use interface and error path inspection.
  • Makefile support and batch execution.

Errors detected:

  • Memory allocation errors (null pointers, memory leaks, dangling pointers)
  • Bad locking discipline (double locks/unlocks, locks not released etc.)
  • Interrupt handling (cli/sti-style).
  • And all the errors which can be described by state automata.

Tools to make formal models


Alloy


The Alloy Analyzer is a tool developed by the Software Design Group for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. The tool can generate instances of invariants, simulate the execution of operations (even those defined implicitly), and check user-specified properties of a model. Alloy and its analyzer have been used primarily to explore abstract software designs. Its use in analyzing code for conformance to a specification and as an automatic test case generator are being investigated in ongoing research projects.

mCRL2


mCRL2 is a formal specification language with an associated toolset. The toolset can be used for modelling, validation and verification of concurrent systems and protocols.

The toolset supports a collection of tools for linearisation, simulation, state-space exploration and generation and tools to optimise and analyse specifications. Moreover, state spaces can be manipulated, visualised and analysed.

TLA+ Proof System


The TLA+ Proof System (TLAPS) is a platform for computerized verification of TLA+ proofs using formal reasoning systems such as automated theorem provers, proof-assistants, SMT/SAT solvers, and decision procedures. TLA+ is a specification language designed for concurrent, distributed, reactive and real-time systems, but it can also be used to formalize any discrete algorithm. The TLA+ proof language is declarative, hierarchical, and scalable to large system specifications. It provides a consistent abstraction over the various “backend” verifiers. The current release of TLAPS handles just enough temporal reasoning to check safety properties; an extension to the full TLA+ language is under active development.

Conclusion


It remains to test all those programs. A hard task that is not yet done.

 
free_software_for_formal_verification.1327747069.txt.gz · Dernière modification: Le 13/02/2012 à 21:07 (modification externe)     Haut de page
Recent changes RSS feed Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki Design by Chirripó