Astrée (static analysis) explained
| Astrée |
| Author: | Patrick Cousot, Radhia Cousot, Jérôme Feret, Antoine Miné, Xavier Rival |
| Developer: | Laboratoire d'Informatique, École normale supérieure (Paris) (LIENS)
French Institute for Research in Computer Science and Automation (INRIA, Paris–Rocquencourt) |
| Latest Release Version: | 23.10 |
| Programming Language: | OCaml |
| Engines: | --> |
| Operating System: | Windows 10, Linux 64-bit, macOS |
| Platform: | x86-64
- AArch64 (M1, M2, M3)
|
| Language: | English |
| Genre: | static analyzer |
| License: | Proprietary |
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]
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.
- 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.
- 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.
- Jean-Louis Boulanger. Static Analysis of Software: The Abstract Interpretation. . 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,, 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.
External links
Notes and References
- Web site: Home . astree.ens.fr.
- News: L'Avion qui "bat des ailes" a fédéré de nombreux chercheurs . Le Monde.fr . 26 April 2005.
