Piste: • permanence • permanence_2011-05-20 • pique_nique_estival_2005 • pistache • planete_en_fete • portables_libres • presentation_framac • prets_gulliver • prod_son • program_dev_check_environments
Table des matières

Environments to develop and check programs


I have put under this category software that can be applied to real world programs (in languages like C or Ada for example) to prove properties on them. I also lists environments that help to check algorithms, etc.

Maude


Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications. Maude has been influenced in important ways by the OBJ3 language, which can be regarded as an equational logic sublanguage. Besides supporting equational specification and programming, Maude also supports rewriting logic computation.

Rewriting logic is a logic of concurrent change that can naturally deal with state and with concurrent computations. It has good properties as a general semantic framework for giving executable semantics to a wide range of languages and models of concurrency. In particular, it supports very well concurrent object-oriented computation. The same reasons making rewriting logic a good semantic framework make it also a good logical framework, that is, a metalogic in which many other logics can be naturally represented and executed.

Sparkle


Sparkle is a proof tool specially constructed for Clean (a state-of-the-art pure and lazy functional programming language). The tool knows the Clean 2.0 syntax and semantics. It comes with a rich set of proof tactics and a powerful hint mechanism to aid the user in proving properties of Clean programs.

SPARK ADA


SPARK is a formally-defined computer programming language based on the Ada programming language, intended to be secure and to support the development of high integrity software used in applications and systems where predictable and highly reliable operation is essential either for reasons of safety (e.g., avionics in aircraft/spacecraft, or medical systems and process control software in nuclear powerplants) or for business integrity (for example financial software for banking and insurance companies).

There are two versions of the SPARK language; one based on Ada 83, and the other on Ada 95. The SPARK language consists of a highly restricted, well-defined subset of the Ada language that uses annotated meta information (in the form of Ada comments) that describe desired component behavior and individual runtime requirements, thereby optionally facilitating mandatory use of Design by Contract principles to accurately formalize and validate expected runtime behavior.

Because the annotations are in commentary, SPARK programs are generally also valid Ada programs and can be compiled by an appropriate Ada compiler. The most recent revision of the implementation, RavenSPARK, includes the Ravenscar tasking profile which aims to support concurrency in high integrity applications. The formal, unambiguous definition of SPARK allows and encourages a variety of static analysis techniques to be applied to SPARK programs.


Brillant


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


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.


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 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.
 
program_dev_check_environments.txt · Dernière modification: 2012/01/28 11:48 par migrate-to-doku     Haut de page
Recent changes RSS feed Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki Design by Chirripó