The AstréeA Static Analyzer

Centre National de la Recherche Scientifique

École Normale Supérieure

INRIA (since Sep. 2007)

Participants:

Contact(‡):

http://www.astreea.ens.fr/

Current support:  AstréeA is currently supported by the Agence nationale de la recherche (ANR) project ANR-11-INSE-014 (January 1st 2012—December 31st 2015).

AstréeA stands for Analyseur statique de logiciels temps-réel asynchrones embarqués (real-time asynchronous embedded software static analyzer). The development of AstréeA started in 2006 at the Laboratoire d'Informatique of the École Normale Supérieure (LIENS), initially supported by the THÉSÉE project, the Centre National de la Recherche Scientifique, the École Normale Supérieure and, since September 2007, by INRIA (Paris—Rocquencourt).

Objectives of AstréeA

AstréeA is a static program analyzer aiming at proving the absence of Run Time Errors (RTE) in large scale asynchronous embedded software running under safety-critical, real-time, space and time partitioning operating systems satisfying the ARINC 653 (Avionics Application Standard Software Interface) specification. The considered run time errors are either classical (such as arithmetic overflows or buffer-overruns) or linked to parallelism (such as data races). On personal computers, such errors, commonly found in programs, usually result in unpleasant error messages, if any, and the termination of the application, and sometimes in a system crash. In embedded applications, such errors are not acceptable since they may have much graver consequences. Moreover, for parallel programs, bugs are particular hard to find when they appear only for particular interleavings of the concurrent processes, which may be hardly reproducible. Thus AstréeA finds transient bugs that a per-process analysis cannot find at all. AstréeA analyzes structured C programs, with complex memory usages, statically allocated processes, but without dynamic memory or process allocation and recursion. This encompasses many embedded parallel programs as found in earth transportation, nuclear energy, medical instrumentation, aeronautic, and aerospace applications, in particular modules of differing criticality levels under the Integrated Modular Avionics (IMA) airborne system.

Astrée and AstréeA

AstréeA is built upon Astrée. Rapid overviews of Astrée are proposed in [21] and [22]. Astrée was specialized for synchronous real-time programs whereas AstréeA is developped for asynchronous real-time programs. Asynchrony introduces additional difficulties due to the semantics of parallelism (such as the abstraction of process interleaving, explicit process scheduling, shared memory model, etc).

Theoretical Background of AstréeA

The design of Astrée and AstréeA is based on abstract interpretation, a formal theory of discrete approximation applied to an asynchronous semantics of 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 »  ). More advanced introductory references are [1], [2], [3], and [4].

Briefly, program verification — including finding possible run-time errors — 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éeA is always sound);
• occasionally signal errors that cannot really happen (false alarms on spurious executions e.g. when hypotheses on the execution environment or the user-definable process scheduling are not taken into account).

Of course, the goal is to be precise, that is to minimize the number of false alarms. The analysis must also be cost-effective, e.g. being a small fraction of the costs of running all tests of the program. In the context of safety-critical synchronous reactive software, the goal of zero false alarm was first attained by Astrée when proving the absence of any RTE in the primary flight control software of the Airbus A340.

AstréeA is based on the theory of abstract interpretation [1,2,3,4] and so proceeds by effectively computing an overapproximation of the interleaved trace semantic properties of analyzed processes and then proving that these abstract properties imply the absence of runtime errors. Most abstractions are infinitary which requires convergence acceleration with widening/narrowing [6,11]. The soundness of the abstractions is based on Galois connections [6,9] or concretization-based [10] in absence of best abstraction. The principal difficulties for the static analysis of parallel process are due to the interleaving of their executions [14, 15, 16, 17].

AstréeA aims at being 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éeA is sound. AstréeA does 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 at high levels of criticality.
• Some static analyzers (e.g. using theorem provers or satisfiabilty modulo theory solvers) require programs to be manually decorated with the inductive invariants that they cannot infer.
  In contrast AstréeA 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éeA has shown to be efficient and to scale up to real size programs as found in the industrial practice.
• General-purpose static analyzers aim at analyzing any program written in a given programming language and model of concurrency 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 programs and so can take specific program structures into account.
  In contrast, AstréeA is domain-aware and so knows facts about application domains that are indispensable to make sophisticated proofs.
  Moreover, AstréeA is parametric. This means that the rate (cost of the analysis / precision of the analysis) can be fully adapted to the needs of AstréeA's end-users thanks to parameters and directives tuning the abstraction.
  AstréeA is modular. It is made of pieces (so called abstract domains) that can be assembled and parameterized to build application specific analyzers [23], fully adapted to a domain of application or to end-user needs [23]. Written in OCaml, the modularization of AstréeA and borrowing to Astrée are made easy thanks to OCaml's modules and functors.
  Finally, AstréeA 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 10.000 false alarms on a program with 10 processes of 100.000 operations).

AstréeA is in progress

AstréeA is presently an academic prototype [30, 31, 32] which is capable of analyzing real-life parallel programs over a million of lines, in a sound way and with much more precise than other static analyzers for asynchrony. The selectivity (alarms per line of code) was 0.4% on March 14^th, 2011. So, more work is still needed to achieve a very high precision, as required for a production-quality tool used in an industrial context like Astrée (as distributed by AbsInt). This includes intense research on a scalable relational abstraction of interactions between processes, a scalable and precise abstraction of process scheduling, a more refined and permissive memory model, and on a scalable shape abstractions of complex data structures [26, 27, 28, 29].

Introductory 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.
4. Patrick Cousot & Radhia Cousot.
   A gentle introduction to formal verification of computer systems by abstract interpretation.
   In Logics and Languages for Reliability and Security, J. Esparza, O. Grumberg, & M. Broy (Eds), NATO Science Series III: Computer and Systems Sciences, © IOS Press, 2010, Pages 1—29.

References on the Abstract Interpretation Foundations of AstréeA

5. Patrick Cousot & Radhia Cousot.
   Static Determination of Dynamic Properties of Programs.
   In Proceedings of the second international symposium on Programming, B. Robinet (Ed), Paris, France, pages 106—130, 13—15 April 1976, Dunod, Paris.
6. Patrick Cousot & Radhia Cousot.
   Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints.
   In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238—252, Los Angeles, California, 1977. ACM Press, New York.
7. Patrick Cousot & Radhia Cousot.
   Static determination of dynamic properties of recursive procedures.
   In IFIP Conference on Formal Description of Programming Concepts, E.J. Neuhold, (Ed.), pages 237—277, St-Andrews, N.B., Canada, 1977. North-Holland Publishing Company (1978).
8. Patrick Cousot.
   Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique des programmes.155—164.
   Thèse ès Sciences Mathématiques, Université Joseph Fourier, Grenoble, France, 21 March 1978.
9. Patrick Cousot & Radhia Cousot.
   Systematic Design of Program Analysis Frameworks.
   In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 269—282, San Antonio, Texas, 1979. ACM Press, New York.
10. Patrick Cousot & Radhia Cousot.
    Abstract interpretation frameworks.
    Journal of Logic and Computation, 2(4):511—547, August 1992.
11. Patrick Cousot & Radhia Cousot.
    Comparing the Galois connection and widening/narrowing approaches to abstract interpretation.
    Programming Language Implementation and Logic Programming, Proceedings of the Fourth International Symposium, PLILP'92, Leuven, Belgium, 13—17 August 1992, Volume 631 of Lecture Notes in Computer Science, pages 269—295. © Springer 1992.
12. Patrick Cousot.
    The Calculational Design of a Generic Abstract Interpreter.
    In Broy, M., and Steinbrüggen, R. (eds.): Calculational System Design. NATO ASI Series F. Amsterdam: IOS Press, 1999.
13. Patrick Cousot & Radhia Cousot.
    Temporal Abstract Interpretation.
    In Conference Record of the 27^th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Programming Languages, Boston, Mass., 19-21 January 2000. ACM Press, New York, U.S.A. pp. 12-25.

References on Proof and Static Analysis of Parallel Programs Foundations of AstréeA

14. Patrick Cousot & Radhia Cousot.
    Semantic analysis of communicating sequential processes.
    Seventh International Colloquium on Automata, Languages and Programming, Noordwijerhout, The Netherlands, 14--18 July 1980, Lecture Notes in Computer Science 85, pages 119—133. © Springer 1980.
15. Patrick Cousot & Radhia Cousot.
    Invariance Proof Methods and Analysis Techniques For Parallel Programs.
    In A.W. Biermann, G. Guiho & Y. Kodratoff, editors, Automatic Program Construction Techniques, pages 243—271. Macmillan, New York, 1984.
16. Patrick Cousot & Radhia Cousot.
    Principe des Méthodes de Preuve de Propriétés d'Invariance et de Fatalité des Programmes Parallèles. 
    (Principle of invariance and inevitability proof methods of concurrent programs.) In « Parallélisme, communication et synchronisation », J.-P. Verjus et G. Roucairol (Eds.), Éditions du CNRS, Paris, pp. 129—149, 1985.
17. Radhia Cousot.
    Fondements des méthodes de preuve d'invariance et de fatalité de programmes parallèles.  
    Thèse ès Sciences Mathématiques, Institut national polytechnique de Lorraine, Nancy, France, 15 November 1985.
18. Patrick Cousot.
    Verification by Abstract Interpretation.
    In International Symposium on Verification — Theory & Practice — Honoring Zohar Manna's 64^th Birthday, Sunday, June 29 — Friday, July 4, 2003, Taormina, Sicily, Italy, Lecture Notes in Computer Science, vol. 2772, Nachum Dershowitz (Ed.), pp. 243—268, © Springer 2003.

Selected references on Astrée relevant to AstréeA (more references on Astrée are available on its web page)

19. 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, D.A. Schmidt and I.H. Sudborough (Editors). Volume 2566 of Lecture Notes in Computer Science, pp. 85—108, © Springer.

20. 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.

21. 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.
22. 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), Volume 3444 of Lecture Notes in Computer Science, pp. 21—30, 2—10 April 2005, Edinburgh, © Springer.

23. 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.

24. 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.

25. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, and Xavier Rival.
    Why does Astrée scale up?
    Formal Methods in System Design, Springer, Volume 35, Number 3, Pages 229—264. December, 2009.

Selected references on Shape analysis of data structures relevant to AstréeA

26. Patrick Cousot, Radhia Cousot, & Laurent Mauborgne.
    A Scalable Segmented Decision Tree Abstract Domain.
    In Zohar Manna, Doron Peled (Eds.): Time for Verification, Essays in Memory of Amir Pnueli. Lecture Notes in Computer Science 6200, pp. 72—95. © Springer 2010.

27. Patrick Cousot, Radhia Cousot, & Francesco Logozzo.
    A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis.
    In Thomas Ball, Mooly Sagiv (Eds.): Conference Record of the 38th ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages, Austin, TX, USA, January 26—28, pp. 105—118, 2011. © ACM Press, New York.

28. Bor-Yuh Evan Chang & Xavier Rival.
    Relational Inductive Shape Analysis.
    In George C. Necula and Philip Wadler (Eds.): Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, CA, USA, January 10—12, 2008, pp. 247—260. © ACM 2008

29. Xavier Rival & Bor-Yuh Evan Chang.
    Abstracting Calling Contexts with Shapes.
    In Thomas Ball, Mooly Sagiv (Eds.): Conference Record of the 38th ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages, Austin, TX, USA, January 26—28, pp. 173—186, 2011. © ACM Press, New York.

References on AstréeA

30. Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, & Xavier Rival.
    Static Analysis and Verification of Aerospace Software by Abstract Interpretation.
    In AIAA Infotech@Aerospace 2010, Atlanta, Georgia. American Institute of Aeronautics and Astronautics, 20—22 April 2010. © AIAA.
    (Best paper award.)

31. Julien Bertrane, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, & Xavier Rival.
    Static Analysis by Abstract Interpretation of Embedded Critical Software.
    In Third IEEE International workshop UML and Formal Methods, 16 November 2010, Shanghai, China, © IEEE.

32. Antoine Miné.
    Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs.
    In Proc. of the 20th European Symposium on Programming (ESOP'11), Lecture Notes in Computer Science 6602, © Springer 2011.

Support of AstréeA

The development of the AstréeA Static Analyzer was supported in part by the French exploratory project THÉSÉE of the Réseau National de recherche et d'innovation en Technologies Logicielles (RNTL, now Agence Nationale de la Recherche, ANR)   (2006—2009), which final review was held on March 7th, 2010 and the Agence nationale de la recherche (ANR) project ANR-11-INSE-014 from January 1st 2012 to December 31st 2015.

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