Astrée and RuleChecker release 19.04

Astrée screenshot

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.

Astrée screenshot

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.

Astrée screenshot

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.

Astrée screenshot

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”.

Astrée screenshot

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.

Astrée screenshot

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.