The AstréeA Static Analyzer

Centre National de la Recherche Scientifique

École Normale Supérieure

INRIA (since Sep. 2007)

Participants:

Support:  AstréeA is supported by the Agence nationale de la recherche (ANR) project ANR-11-INSE-014 (January 1st 2012—November 30th 2016).

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). In 2015, AstréeA has been licensed to AbsInt Angewandte Informatik; the company makes the analyzer available commercially through their Astrée product.

A Workshop on Static Analysis of Concurrent Software has been organized in affiliation with the 23rd Static Analysis Symposium in September 2016 to present the theoretical and practical results achieved through AstréeA.

A poster of the project was presented at Les rencontres du numérique de l'ANR in November 2016.

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, with an initial focus on applications 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 related to parallelism (notably data races and deadlocks). 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 neither per-process analysis nor testing can find. AstréeA analyzes structured C programs, with complex memory usages, statically allocated processes, but without dynamic process allocation nor 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. Quick 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, 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 by covering, at least, all possible executions, including all process interleavings allowed by the scheduler (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 processes are due to the interleaving of their executions [14,15,16,17]. The results achieved by AstréeA were made possible by significant theoretical advances to solve these issues during the course of its development [32,33,34].

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.
  Most automated analyzers for asychronous software actually require programmers to specify which variables are shared and the range of possible values (i.e., each thread is analyzed separately in the context of a programmer-specified environment modeling the other threads).
  In contrast AstréeA is fully automatic, that is never needs to rely on the user's help. In particular, the set of shared variables, as well as their range and possible data races, are discovered automatically.
• 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 (typically between 1% and 10% of false alarms).

Results of AstréeA

AstréeA has started as an academic prototype [30, 31, 32, 33, 34, 35, 36] capable of analyzing real-life parallel programs of millions of lines, in a sound way and with much more automation and more precision than other static analyzers for asynchrony. In an academic context, it achieved a selectivity (rate of code lines without any alarm) of 99.94% in October 2015 on a core use case, a 2.2 million lines ARINC 653 avionics application [37]. Additionnaly, AstréeA has been shown to be usable in industrial context [37].

The AstréeA prototype has been since merged with the commercial version of the Astrée analyzer, developed and distributed by AbsInt Angewandte Informatik, starting from version 15.10. AstréeA has support for detecting all run-time errors, data races and deadlocks in C programs. Initially developed for ARINC 653 avionics applications, AstréeA can now analyze applications developed under a wider range of real-time operating systems, including OSEK/AUTOSAR for automotive applications [38] and a subset of real-time POSIX [37].

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.

33. Antoine Miné.
    Static Analysis of Run-Time Errors in Embedded Real-Time Parallel C Programs.
    Logical Methods in Computer Science (LMCS), 8(1:26), 63 pages, March 2012.

34. Antoine Miné.
    Relational Thread-Modular Static Value Analysis by Abstract Interpretation.
    In Proc. of the 15th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'14), volume 8318 of Lecture Notes in Computer Science (LNCS), 39-58, San Diego, California, USA, Jan. 2014. Springer.

35. 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 Foundations and Trends in Programming Languages (FnTPL), 2(2–3), 71–190, 2015. Now Publishers.

36. Antoine Miné.
    AstréeA: A Static Analyzer for Large Embedded Multi-Task Software.
    In Proc. of the 16th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'15) (invited), volume 8931 of Lecture Notes in Computer Science (LNCS), 3 pages, Mumbai, India, Jan. 2015.

Industrial use of AstréeA

37. Antoine Miné, David Delmas.
    Towards an Industrial Use of Sound Static Analysis for the Verification of Concurrent Embedded Avionics Software.
    In Proc. of the 15th International Conference on Embedded Software (EMSOFT'15), 65–74, Amsterdam, The Netherlands, Oct. 2015. IEEE CS Press.

38. Antoine Miné, Laurent Mauborgne, Xavier Rival, Jérôme Feret, Patrick Cousot, Daniel Kästner, Stephan Wilhelm, Christian Ferdinand.
    Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée.
    In Proc. of Embedded Real Time Software and Systems (ERTS2 2016), 570–579, Toulouse, France, Jan 2016.

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 November 30th 2016.