The AstréeA Static Analyzer


CNRS Centre National de la Recherche Scientifique ENS École Normale Supérieure ENS INRIA (since Sep. 2007)

Participants:

Patrick Cousot (project leader), Radhia Cousot, Jérôme Feret, Antoine Miné, Xavier Rival

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

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.

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.

      A380 Cockpit

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 »  fran\347ais). 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:

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

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. (French)
  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

  1. 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.
  2. 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.
  3. 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).
  4. 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. (French)
    Thèse ès Sciences Mathématiques, Université Joseph Fourier, Grenoble, France, 21 March 1978.
  5. 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.
  6. Patrick Cousot & Radhia Cousot.
    Abstract interpretation frameworks.
    Journal of Logic and Computation, 2(4):511—547, August 1992.
  7. 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.
  8. 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.
  9. Patrick Cousot & Radhia Cousot.
    Temporal Abstract Interpretation.
    In Conference Record of the 27th 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

  1. 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.
  2. 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.
  3. Patrick Cousot & Radhia Cousot.
    Principe des Méthodes de Preuve de Propriétés d'Invariance et de Fatalité des Programmes Parallèles(French)
    (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.
  4. Radhia Cousot.
    Fondements des méthodes de preuve d'invariance et de fatalité de programmes parallèles.  (French)
    Thèse ès Sciences Mathématiques, Institut national polytechnique de Lorraine, Nancy, France, 15 November 1985.
  5. Patrick Cousot.
    Verification by Abstract Interpretation.
    In International Symposium on Verification — Theory & Practice — Honoring Zohar Manna's 64th 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)

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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 11th 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.
  6. 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.
  7. 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

  1. 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.
  2. 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.
  3. 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
  4. 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

  1. 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.)
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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

  1. 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.
  2. 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

RNTL      ANR       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)  (french) (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.