Astrée

What is Astrée?

Astrée is a static code analyzer that proves the absence of runtime errors and invalid concurrent behavior in critical security software written or generated in C.

Astrée is primarily focused on embedded applications, as found in aeronautics, ground transportation, medical instrumentation, nuclear energy and spaceflight. However, it can also be used to analyze any structured, handwritten, or generated C program with complex uses of memory, dynamic memory allocation, and recursion.

What properties of Astrée software?

Astrée analyzes whether the C programming language is used correctly and whether there may be runtime errors during any run in any environment. This covers any use of C that, according to the C99 standard, behaves undefined or violates specific aspects of hardware.

In addition, Astrée reports invalid concurrent behavior, violations of user-specified programming guidelines, and various program properties relevant to functional security.

Astrée detects

• Division by zero,
• Out-of-bounds array indexing,
• Incorrect pointer and referencing manipulation (NULL, uninitialized, and pending pointers),
• Aritmetic excess of integers and floating point,
• Read access to uninitialized variables,
• Data runs (simultaneous read/write or write/write accesses by two threads to the same memory location without proper mutex lock),
• Inconsistent blocking (blocking/unlocking issues),
• Invalid calls to operating system services (for example, OSEK calls to Terminate Taska task with unreleased resources),
• Violation of optional user-defined assertions to prove additional runtime properties (similar to assert diagnostics),
• Code may prove to be inaccessible under any circumstances.

Adapt it to your own needs

Astrée offers powerful annotation mechanisms to provide external knowledge and improve analysis accuracy for individual loops or data structures. Detailed messages and an intuitive GUI that guides you to the exact cause of each potential runtime error. Actual errors can be corrected and in the case of a false alarm, the analyzer can be adjusted to avoid it. This allows analysis with few or even zero false alarms.

System Requirements

Windows: Windows 7 64-bit SP1 or newer

Linux: CentOS / RHEL 6 64-bit or compatible

4 GB of RAM (16 GB recommended)

4 GB of disk space