Taint analysis
Astrée can now track taint information for memory locations.
This new feature can be used for analyzing security properties.
It is disabled by default and can be enabled by setting the option
track-taint-hues. Additionally, the new directives
__ASTREE_taint and __ASTREE_taint_sink
can be inserted into the code for expressing where variables
are tainted and which memory locations must not be reached by taints.
Spectre vulnerability detection
Astrée now detects and reports Spectre v1, Spectre v1.1,
and SplitSpectre vulnerabilities.
The detection is disabled by default
and can be enabled via the new option detect-spectre.
Closed beta: Astrée for C++
This is the first Astrée release to offer static run-time error analysis of C++ code. Evaluation licenses can now be issued on request.
AUTOSAR C++14 rule set
RuleChecker can now check C++ code for compliance with AUTOSAR C++ coding rules as defined in the AUTOSAR document “Guidelines for the use of the C++14 language in critical and safety-related systems”.
AUTOSAR multi-core support
Astrée now supports AUTOSAR multi-core systems using a multi-core aware OS model with support for spinlocks. The OS setup can be automatically derived from ARXML.
Analysis of finite-state machines
This release introduces a new relational domain for a more precise analysis of finite-state machines. The above screenshot showcases one tricky example that Astrée is now able to analyse with no false alarms.
The new domain is activated with the option state-machine=yes
and reacts to the new directive __ASTREE_states_track((x))
which indicates that x is used to encode
the state of a state machine.
Special treatment stops upon encountering either __ASTREE_states_merge((x))
or __ASTREE_states_merge(()).
The new option automatic-state-machine=yes enables
automatic detection of code patterns used in state machine
implementations, for which Astrée can then insert
__ASTREE_states_track directives.
