PROFILBARU.COM

Astrée
Original author(s)	Patrick Cousot, Radhia Cousot, Jérôme Feret, Antoine Miné, Xavier Rival
Developer(s)	Laboratoire d'Informatique, École normale supérieure (Paris) (LIENS); French Institute for Research in Computer Science and Automation (INRIA, Paris–Rocquencourt)
Initial release	16 December 2002; 21 years ago
Stable release	23.10 / 2023; 1 year ago
Written in	OCaml
Operating system	Windows 10, Linux 64-bit, macOS
Platform	x86-64; AArch64 (M1, M2, M3)
Available in	English
Type	static analyzer
License	Proprietary
Website	www.astree.ens.fr

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 programming languages C and C++, and emits 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. It is proprietary software written in the language OCaml.

The tool is tailored toward 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 added operating system (OS) specifications. On multi-core processors, the placement of threads to cores, and the use of mutex locks and spinlocks are analyzed.

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

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