Astrée (static analysis)

Astrée ("Analyseur statique de logiciels temps-réel embarqués"[1]) is a static analyzer based on abstract interpretation. It analyzes programs written in the C and C++ programming languages and outputs an exhaustive list of possible runtime errors and assertion violations. The defect classes covered include divisions by zero, buffer overflows, dereferences of null or dangling pointers, data races, deadlocks, etc. Astrée includes a static taint checker and helps finding cybersecurity vulnerabilities, such as Spectre.

The tool is tailored towards safety-critical embedded code: specific analysis techniques are used for common control theory constructs (finite state machines, digital filters, rate limiters...) and floating-point numbers.

Concurrent code is analyzed with a sound interleaving semantics that is aware of the concurrent threads of execution, their priorities and synchronization mechanisms. Astrée supports the ARINC 653, OSEK and AUTOSAR execution models and can be adapted to additional OS specifications. On multi-core processors the placement of threads to cores, and the usage of mutex locks and spinlocks are taken into account.

Astrée was developed in Patrick Cousot's group at École Normale Supérieure, a joint group with CNRS, and is marketed by AbsInt GmbH. It is used in the defense/aerospace, industrial control, electronic, and automotive industries. One of the main industrial users is Airbus.[2]

Astrée is a commercial product available from AbsInt Angewandte Informatik.

See also

Bibliography
  • 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). Volume 2566 of Lecture Notes in Computer Science, pp. 85–108, Springer. doi:10.1007/3-540-36377-7_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. doi:10.1145/781131.781153
  • David Delmas and Jean Souyris. Astrée: from Research to Industry., Proc. 14th International Static Analysis Symposium, SAS 2007, G. Filé & H. Riis-Nielson (eds), Kongens Lyngby, Denmark, 22–24 August 2007, LNCS 4634, pp. 437–451
  • Arnaud J. Venet and Michael R. Lowry. 2010. Static analysis for software assurance: soundness, scalability and adaptiveness. In Proceedings of the FSE/SDP workshop on Future of software engineering research (FoSER '10). ACM, New York, NY, USA, 393-396. doi:10.1145/1882362.1882442
  • Jean-Louis Boulanger. Static Analysis of Software: The Abstract Interpretation. ISBN 978-1-84821-320-3. Wiley.
  • Daniel Kästner, Stephan Wilhelm, Stefana Nenova, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival. Astrée: Proving the Absence of Runtime Errors. Embedded Real Time Software and Systems Congress ERTS², Toulouse, 2010.
  • A. Miné, L. Mauborgne, X. Rival, J. Feret, P. Cousot, D. Kästner, S. Wilhelm, C. Ferdinand. Taking Static Analysis to the Next Level: Proving the Absence of Run-Time Errors and Data Races with Astrée. In ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, Jan 2016, Toulouse, France.
  • D. Kästner, L. Mauborgne, N. Grafe, C. Ferdinand. Advanced Sound Static Analysis to Detect Safety- and Security-Relevant Programming Defects. 8th International Journal on Advances in Security, ISSN 1942-2636, vol. 11, no. 1 & 2, 149-159, IARIA, 2018.
  • D. Kästner, B. Schmidt, M. Schlundt, L. Mauborgne, S. Wilhelm, C. Ferdinand. Analyze This! Sound Static Analysis for Integration Verification of Large-Scale Automotive Software. SAE Technical Paper 2019-01-1246, SAE World Congress 2019, Detroit, April 2019. doi:10.4271/2019-01-1246

References
  1. "Home". astree.ens.fr.
  2. "L'Avion qui "bat des ailes" a fédéré de nombreux chercheurs". Le Monde.fr. 26 April 2005.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.