The ASTRÉE Static Analyzer

Centre National de la Recherche Scientifique

École Normale Supérieure

Participants:

Former participants:

Contact(‡):

http://www.astree.ens.fr/

Objectives of ASTRÉE

ASTRÉE is a static program analyzer developed at the Laboratoire d'Informatique of the École Normale Supérieure (LIENS) aiming at proving the absence of Run Time Errors (RTE) in programs written in the C programming language. On personal computers, such errors, commonly found in programs, usually result in unpleasant error messages and the termination of the application, and sometimes in a system crash. In embedded applications, such errors may have graver consequences.

ASTRÉE analyzes structured C programs, with complex memory usages [17], but without dynamic memory allocation and recursion. This encompasses many embedded programs as found in earth transportation, nuclear energy, medical instrumentation, aeronautic, and aerospace applications, in particular synchronous control/command such as electric flight control [22], [23].

ASTRÉE stands for Analyseur statique de logiciels temps-réel embarqués (real-time embedded software static analyzer).

Industrial Applications of ASTRÉE

The development of ASTRÉE started from scratch in Nov. 2001. Two years later, the main applications have been the static analysis of synchronous, time-triggered, real-time, safety critical, embedded software written or automatically generated in the C programming language. ASTRÉE has achieved the following unprecedented results:

In Nov. 2003, ASTRÉE was able to prove completely automatically the absence of any RTE in the primary flight control software of the Airbus A340 fly-by-wire system, a program of 132,000 lines of C analyzed in 1h20 on a 2.8 GHz 32-bit PC using 300 Mb of memory (and 50mn on a 64-bit AMD Athlon™ 64 using 580 Mb of memory).
From Jan. 2004 on, ASTRÉE was extended to analyze the electric flight control codes then in development and test for the A380 series. The operational application by Airbus France at the end of 2004 was just in time before the A380 maiden flight on Wednesday, 27 April, 2005.
In April 2008, ASTRÉE was able to prove completely automatically the absence of any RTE in a C version of the automatic docking software of the Jules Vernes Automated Transfer Vehicle (ATV) enabling ESA to transport payloads to the International Space Station.

Theoretical Background of ASTRÉE

The design of ASTRÉE is based on abstract interpretation, a formal theory of discrete approximation applied to the semantics, applied to the C programming language. The informal presentation Abstract Interpretation in a Nutshell aims at providing a short intuitive introduction to the theory. A video introduces program verification by abstract interpretation (in French: « La vérification des programmes par interprétation abstraite »  ).

Briefly, program verification — including finding possible run-time error — is undecidable: there's is no mechanical method that can always answer truthfully whether programs may or not exhibit runtime properties — including absence of any run-time error —. This is a deep mathematical result dating from the works of Church, Gödel and Turing in the 1930's. When faced with this mathematical impossibility, the choice has been to design an abstract interpretation-based static analyzer that will automatically:

• signal all possible errors (ASTRÉE is always sound);
• occasionally signal errors that cannot really happen (false alarms on spurious executions e.g. when hypotheses on the execution environment are not taken into account).

Of course, the goal is to be precise, that is to minimize the number of false alarms. In the context of safety-critical reactive software, the goal of zero false alarm was first attained when proving the absence of any RTE in the primary flight control software of the Airbus A340.

More advanced introductory references are [1], [2] and [3].

Which Program Run-Time Properties are Proved by ASTRÉE?

• Any use of C defined by the international norm governing the C programming language (ISO/IEC 9899:1999) as having an undefined behavior (such as division by zero or out of bounds array indexing),
• Any use of C violating the implementation-specific behavior of the aspects defined by ISO/IEC 9899:1999 as being specific to an implementation of the program on a given machine (such as the size of integers and arithmetic overflow),
• Any potentially harmful or incorrect use of C violating optional user-defined programming guidelines (such as no modular arithmetic for integers, even though this might be the hardware choice), and also
• Any violation of optional, user-provided assertions (similar to assert diagnostics for example), to prove user-defined run-time properties.

Three Simple Examples ... Hard to Analyze in the Large

The examples below show typical difficulties in statically analyzing control/command programs. Of course, the real difficulty is to scale up!

Booleans

Control/command programs, in particular synchronous ones, manipulate thousands of boolean variables. Analyzing which program run-time properties hold when each such boolean variable is either true or false rapidly leads to a combinatorial explosion of the number of cases to be considered, that is prohibitive time and memory analysis costs.

For example, the analysis of the following program by ASTRÉE:

/* boolean.c */
typedef enum {FALSE = 0, TRUE = 1} BOOLEAN;
BOOLEAN B;
void main () {
  unsigned int X, Y;
  while (1) {
    /* ... */
    B = (X == 0);
    /* ... */
    if (!B) {
      Y = 1 / X;
    };
    /* ... */
  };
}

Floating point computations

Command programs controlling complex physical systems are derived from mathematical models designed with real numbers whereas computer programs perform floating point computations. The two computation models are completely different and this can yield very surprising results, such as:

/* float-error.c */
int main () {
    float x, y, z, r;
    x = 1.000000019e+38;
    y = x + 1.0e21;
    z = x - 1.0e21;
    r = y - z;
    printf("%f\n", r);
}
% gcc float-error.c
% ./a.out
0.000000
% 

/* double-error.c */
int main () {
  double x; float y, z, r;
  /* x = ldexp(1.,50)+ldexp(1.,26); */
  x = 1125899973951488.0; 
  y = x + 1;
  z = x - 1;
  r = y - z;
  printf("%f\n", r);
}
% gcc double-error.c
% ./a.out
134217728.000000
% 

ASTRÉE handles floating point computations precisely and safely. For example, ASTRÉE proves the following program free of run-time error when running on a machine with floats on 32 bits:

/* float.c */
void main () {
  float x,y,z;
  if ((x < -1.0e38) || (x > 1.0e38)) return;
  while (1) {
    y = x+1.0e21;
    z = x-1.0e21;
    x = y-z;
  }
}

Digital filters

Control/command programs perform lots of digital filtering, as shown by the following example:

/* filter.c */
typedef enum {FALSE = 0, TRUE = 1} BOOLEAN;
BOOLEAN INIT;
float P, X;

void filter () {
  static float E[2], S[2];
  if (INIT) {
      S[0] = X;
      P = X;
      E[0] = X;
  } else { 
      P = (((((0.5 * X) - (E[0] * 0.7)) + (E[1] * 0.4)) + (S[0] * 1.5)) - (S[1] * 0.7));
  }
  E[1] = E[0];
  E[0] = X;
  S[1] = S[0];
  S[0] = P;
}

void main () {
  X = 0.2 * X + 5;
  INIT = TRUE;
  while (1) { 
    X = 0.9 * X + 35;
    filter ();
    INIT = FALSE;
  }
}

The absence of overflow (and more precisely that P is in [-1327.05, 1327.05] as found by ASTRÉE) is not obvious, in particular because of 32 bits floating point computations. The situation is even more inextricable in the presence of boolean control, cascades of filters, etc.

ASTRÉE is sound, automatic, efficient, domain-aware, parametric, modular, extensible and precise

• Some static analyzers consider only some of the possible run-time errors while others sort out the most probable ones. The aim is then static testing (that is to find out the most frequent bugs) rather than verification (that is to prove the absence of any run-time error).
  In contrast ASTRÉE is sound. ASTRÉE will always exhaustively consider all possible run-time errors and never omit to signal a potential run-time error, a minimal requirement for safety critical software.
• Some static analyzers (e.g. using theorem provers) require programs to be decorated with inductive invariants.
  In contrast ASTRÉE is fully automatic, that is never needs to rely on the user's help.
• Some static analyzers have high computational costs (typically hours of computation per 10,000 lines of code) while others may never terminate or terminate out of memory.
  In contrast ASTRÉE has shown to be efficient and to scale up to real size programs as found in the industrial practice. Since 2005, ASTRÉE can run on multicore parallel or distributed machines [14].
• General-purpose static analyzers aim at analyzing any program written in a given programming language and so can only rely on programming language-related properties to point at potential run-time errors.
• Specialized static analyzers put additional restriction on considered program and so can take specific program structures into account.
  In contrast, ASTRÉE is domain-aware and so knows facts about application domains that are indispensable to make sophisticated proofs. For example, ASTRÉE takes the logic and functional properties of control/command theory into account as implemented in control/command programs [5] [6].
  Moreover, ASTRÉE is parametric. This means that the rate (cost of the analysis / precision of the analysis) can be fully adapted to the needs of ASTRÉE's end-users thanks to parameters and directives tuning the abstraction.
  ASTRÉE is modular. It is made of pieces (so called abstract domains) that can be assembled and parameterized to build application specific analyzers [20], fully adapted to a domain of application or to end-user needs. Written in OCaml, the modularization of ASTRÉE is made easy thanks to OCaml's modules and functors.
  Finally, ASTRÉE is extensible. In case of false alarms, it can be easily extended by introducing new abstract domains enhancing the precision of the analysis.
• A consequence of generality may be low precision. Typical rates of false alarms (i.e. spurious warnings on potential errors than can never occur at runtime) are from 10% to 20% of the C basic operations in the program.
• Specialized static analyzers achieve better precision (e.g. less than 10% of false alarms).
• Even a high selectivity rate of 1 false alarm over 100 operations with potential run-time errors leaves a number of doubtful cases which may be unacceptable for very large safety-critical or mission-critical software (for example, a selectivity rate of 1% yields 1000 false alarms on a program with 100 000 operations).
  In contrast ASTRÉE, being modular, parametric and domain-aware can be made very precise and has shown to be able to produce no false alarm, that is fully automated correctness proofs.
  Theoretical work was done on locating the origin of alarms [13] [15].

Rapid overviews of ASTRÉE is proposed in [7] and [11].

Presentations of ASTRÉE

• Presentation of the ASTRÉE static analyzer on Tuesday August 24^th, 2004 at the topical day on abstract interpretation of the IFIP World Computer Congress in Toulouse (France).
• Presentation of ASTRÉE on January 20^th, 2005 at the Industrial day on Automatic Tools for Program Verification, a satellite event of VMCAI'05, Paris, January 17—19, 2005.
• Presentation of ASTRÉE on March 21^st, 2007 at the thirteenth ASTReNet Workshop on Formal Aspects of Source Code Analysis and Manipulation, BCS-FACS, London, England.
• Presentation of ASTRÉE on December 8^th, 2007 at the 11^th Annual Asian Computing Science Conference, ASIAN'06, National Center of Sciences, Tokyo, Japan.
• Presentation of ASTRÉE on June 5^th, 2007 at the First IEEE & IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2007, Tutorial, Shanghai, China.
• Presentation of ASTRÉE on October 11^th, 2007 at the Embedded Systems Week, Sept 30^th—Oct. 5^th, Salzburg, Austria.
• Présentation et démonstration d'ASTRÉE on October 11^th, 2007 at the XIV^es Rencontres INRIA - Industrie, INRIA Rocquencourt, France. 
• Presentation of ASTRÉE on December 12^th, 2007 at the 2007 ISoLA Workshop On Leveraging Applications of Formal Methods, Verification and Validation, Special Workshop Theme: Formal Methods in Avionics, Space and Transport, Poitiers, France

ASTRÉE Flyer

• ASTRÉE : Analyse statique de code C critique remps réel synchrone embarqué (pdf)  

Introductory Bibliographic References on Abstract Interpretation

1. Patrick Cousot.
   Interprétation abstraite.
   Technique et Science Informatique, Vol. 19, Nb 1-2-3. Janvier 2000, Hermès, Paris, France. pp. 155—164.

2. Patrick Cousot.
   Abstract Interpretation Based Formal Methods and Future Challenges.
   In Informatics, 10 Years Back - 10 Years Ahead, R. Wilhelm (Ed.), Lecture Notes in Computer Science 2000, pp. 138—156, 2001.
3. Patrick Cousot & Radhia Cousot.
   Basic Concepts of Abstract Interpretation.
   In Building the Information Society, R. Jacquard (Ed.), Kluwer Academic Publishers, pp. 359—366, 2004.

Bibliographic References on ASTRÉE

4. Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux & Xavier Rival.
   Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software, invited chapter.
   In The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, T. Mogensen and D.A. Schmidt and I.H. Sudborough (Editors). Lecture Notes in Computer Science 2566, pp. 85—108, © Springer.

5. Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, & Xavier Rival.
   A Static Analyzer for Large Safety-Critical Software.
   In PLDI 2003 — ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation, 2003 Federated Computing Research Conference, June 7—14, 2003, San Diego, California, USA, pp. 196—207, © ACM.

6. Jérôme Feret.
   Static analysis of digital filters.
   In ESOP 2004 — European Symposium on Programming, D. Schmidt (editor), Mar. 27 —Apr. 4, 2004, Barcelona, ES, Lecture Notes in Computer Science 2986, pp. 33—48, © Springer.

7. Laurent Mauborgne.
   ASTRÉE: verification of absence of run-time error.
   In Building the Information Society, R. Jacquard (Ed.), Kluwer Academic Publishers, pp. 385—392, 2004.

8. Antoine Miné.
   Relational abstract domains for the detection of floating-point run-time errors.
   In ESOP 2004 — European Symposium on Programming, D. Schmidt (editor), Mar. 27 — Apr. 4, 2004, Barcelona, Lecture Notes in Computer Science 2986, pp. 3—17, © Springer.

9. Antoine Miné.
   Weakly relational numerical abstract domains.
   Thèse de l'École polytechnique, 6 December 2004.

10. Jérôme Feret.
    The arithmetic-geometric progression abstract domain.
    In VMCAI 2005 — Verification, Model Checking and Abstract Interpretation, R. Cousot (editor), Lecture Notes in Computer Science 3385, pp. 42—58, 17—19 January 2005, Paris, © Springer.

11. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux & Xavier Rival.
    The ASTRÉE analyser.
    In ESOP 2005 — The European Symposium on Programming, M. Sagiv (editor), Lecture Notes in Computer Science 3444, pp. 21—30, 2—10 April 2005, Edinburgh, © Springer.

12. Laurent Mauborgne & Xavier Rival.
    Trace Partitioning in Abstract Interpretation Based Static Analyzer.
    In ESOP 2005 — ; The European Symposium on Programming, M. Sagiv (editor), Lecture Notes in Computer Science 3444, pp. 5—20, 2—10 April 2005, Edinburgh, © Springer.

13. Xavier Rival.
    Understanding the Origin of Alarms in ASTRÉE.
    In SAS'05 — The 12th International Static Analysis Symposium, Chris Hankin & Igor Siveroni (editors), Lecture Notes in Computer Science 3672, pp. 303—319, 7—9 September 2005, London, UK, © Springer.

14. David Monniaux.
    The Parallel Implementation of the Astree Static Analyzer.
    In APLAS 2005 — The Third Asian Symposium on Programming Languages and Systems, Kwangkeun Yi (editor), Lecture Notes in Computer Science 3780, pp. 86—96, 2—5 November 2005, Tsukuba, Japan, © Springer.

15. Xavier Rival.
    Abstract Dependences for Alarm Diagnosis.
    In APLAS 2005 — The Third Asian Symposium on Programming Languages and Systems, Kwangkeun Yi (editor), Lecture Notes in Computer Science 3780, pp. 347—363, 2—5 November 2005, Tsukuba, Japan, © Springer.

16. Antoine Miné.
    Symbolic Methods to Enhance the Precision of Numerical Abstract Domains.
    In VMCAI 2006 — Seventh International Conference on Verification, Model Checking and Abstract Interpretation, E. Allen Emerson & Kedar S. Namjoshi (editors), Lecture Notes in Computer Science 3855, pp. 348—363, 8—10 January 2006, Charleston, South Carolina, USA, © Springer.

17. Antoine Miné.
    Field-Sensitive Value Analysis of Embedded C Programs with Union Types and Pointer Arithmetics.
    In Proceedings of the 2006 ACM SIGPLAN/SIGBED Conference for Languages, Compilers, and Tools for Embedded Systems (LCTES 2006), 14—16 June 2006, Ottawa, Ontario, Canada. ACM Press, pp. 54—63.

18. Patrick Cousot.
    L'analyseur statique ASTRÉE  , Grand Colloque TIC 2006, Session RNTL « Systèmes embarqués », Centre de congrès, Lyon, 15 novembre 2006.

19. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, & Xavier Rival.
    Combination of Abstractions in the ASTRÉE Static Analyzer. In 11^th Annual Asian Computing Science Conference (ASIAN'06), National Center of Sciences, Tokyo, Japan, December 6—8, 2006. LNCS 4435, Springer, Berlin, pp. 272—300, 2008.

20. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival.
    Varieties of Static Analyzers: A Comparison with ASTRÉE, invited paper.
    First IEEE & IFIP International Symposium on ``Theoretical Aspects of Software Engineering'', TASE'07, Shanghai, China, 6—8 June 2007, pp. 3—17.
21. Patrick Cousot.
    Proving the Absence of Run-Time Errors in Safety-Critical Avionics Code.
    In EMSOFT 2007, Embedded Systems Week, Salzburg, Austria, September 30^th, 2007, pp. 7—9, ACM Press.

Bibliographic References on the Industrial Use of ASTRÉE

22. David Delmas and Jean Souyris.
    ASTRÉE: from Research to Industry.
    Proc. 14^th International Static Analysis Symposium, SAS 2007, G. Filé & H. Riis-Nielson (eds), Kongens Lyngby, Denmark, 22-24 August 2007, LNCS 4634, pp. 437—451, © Springer, Berlin.
23. Jean Souyris and David Delmas.
    Experimental Assessment of ASTRÉE on Safety-Critical Avionics Software.
    Proc. Int. Conf. Computer Safety, Reliability, and Security, SAFECOMP 2007, Francesca Saglietti and Norbert Oster (Eds.), Nuremberg, Germany, September 18—21, 2007, Lecture Notes in Computer Science, Volume 4680, pp. 479—490, © Springer, Berlin.

News on ASTRÉE in the press

• Le Journal du CNRS, Nº 182, mars 2005, page 35, Le CNRS, l'A380 et l'aéronautique de demain.
• Le Monde, Nº 18741, 27 avril 2005, page 18, L'avion qui "bat des ailes" a fédéré de nombreux chercheurs.
• Software ohne Fehl und Tadel by Von Karlhorst Klotz, Das M.I.T. Magazin für Innovation Technology, 21 June 2005.
• Le Journal du CNRS, Nº 185, juin 2005, page 25, A380 : Le CNRS à la fête.
• Le Journal du CNRS, Nº 185, juin 2005, pages 25-27, Sécurité : toujours plus !

Support of ASTRÉE

The development of the ASTRÉE Static Analyzer was supported in part by the French exploratory project ASTRÉE of the Réseau National de recherche et d'innovation en Technologies Logicielles (RNTL)   (2002—2006). The final review of the ASTRÉE project was on July 7th, 2006.

Pictures of ASTRÉE

New York City, 6 Jan. 2007	ASTRÉE poster, 9 Oct. 2007

All spam emails to not containing ASTREE (in uppercase) in the subject are automatically filtered out.