Fast and sound static analysis
Static analyzer that proves the absence of runtime errors in safety-critical C code
Astrée is a static analyzer for safety-critical software written or generated in C or C++. Astrée is sound — that is, if no errors are signaled, the absence of errors has been formally proved. In 2020, the US National Institute of Standards and Technology determined that Astrée satisfies their criteria for sound static code analysis.
Features
- *Exceptionally fast and precise analyses, including:
- –Runtime error analysis
- –Data race analysis
- *Non-interference analysis
- *Advanced taint analysis
- *Detection of Spectre vulnerabilities
- *Signal-flow, data-flow, and control-flow analysis
- *Control-coupling and component-interference analysis
- *User-defined cybersecurity analyses
- *Analysis of functional program properties
- *Rule checks for MISRA, CERT, JSF, CWE, AUTOSAR, and other guidelines
- *Analysis of numerous code metrics
- *Dead code recognition
- *Support for C, C++, and mixed code bases
- *Support for collaborative reviews of analysis results
- *TLS-encrypted communication with OpenID and OAuth2 support
- *Automatically generated report files for documentation and certification purposes
- *Qualification Support Kits for DO-178B/C, ISO 26262, EN-50128, and other standards
- *Feature-rich GUI with graphical and textual views for analysis results, source code, control flow, and user comments
- *Command-line mode for easy integration into automated build processes
- *Plugins for TargetLink, Jenkins, μVision, and JSON
- *LSP support for integration with Visual Studio Code, Eclipse, or any other IDE or code editor that provides an LSP client
- *Node-locked, floating, and cloud licenses
- *Regular updates and excellent tech support
Static analysis of runtime properties
Astrée statically analyzes whether the programming language is used correctly and whether there can be any runtime errors during any execution in any environment. This covers any use of C or C++ that, according to the selected language standard, has undefined behavior or violates hardware-specific aspects.
Additionally, Astrée reports invalid concurrent behavior, violations of user-specified programming guidelines, and various program properties relevant for functional safety.
Astrée detects any:
*division by zero,
*out-of-bounds array indexing,
*erroneous pointer manipulation and dereferencing (NULL, uninitialized and dangling pointers)
*integer and floating-point arithmetic overflow,
*read access to uninitialized variables,
*data races (read/write or write/write concurrent accesses by two threads to the same memory location without proper mutex locking), inconsistent locking (lock/unlock problems),
*invalid calls to operating system services (e.g. OSEK calls to TerminateTask on a task with unreleased resources),
*Spectre vulnerabilities,other critical data and control-flow errors,
*violations of optional user-defined assertions to prove additional runtime properties (similar to assert diagnostics),dead code.
Astrée is sound for floating-point computations and handles them precisely and safely. All possible rounding errors, and their cumulative effects, are taken into account.The same is true for −∞, +∞ and NaN values and their effects through arithmetic calculations and comparisons.
Data-flow and control-flow analysis
Astrée tracks accesses to global variables, static variables, and local variables whose accesses are made outside of the frame in which the local variables are defined (e.g. because their address is passed into a called function).
All data and function pointers are resolved automatically. The soundness of the analysis ensures that all potential targets of data and function pointers are taken into account.
Signal-flow analysis
Astrée is able to analyze the flow from input signals to output signals through complex real-world software. This is accomplished through taint analysis that builds upon a full-fledged semantic analysis, thus taking into account the influence of application configuration parameters on the signal flow. The analysis can be performed for a specific application configuration, avoiding false signal flows not present in that configuration. Alternatively, the influence of application parameters on the output signal can be determined for a generic configuration.
If the taint analysis does not report an influence of an input signal on an output signal, independence has been proven. If an unexpected influence is reported, Astrée helps you understand the signal flow to either improve your code or tweak the analysis precision.
Support for C++ and mixed code bases
Since 2020, Astrée can be applied to C++ and mixed C/C++ code bases. By now, it supports C++ versions from C++98 to C++23. Astrée’s C++ analysis is designed to meet the characteristics of safety-critical embedded software and so is subject to the same restrictions as Astrée for C. The high-level abstraction features and template library of C++ facilitate the design of very complex and dynamic software. Extensive use of these features may violate the established principles of safety-critical embedded software development and lead to unsatisfactory analysis times and results. The Astrée manual gives recommendations on the use of C++ features to ensure that the code can be well analyzed. For less constrained (less critical) C++ code, we recommend using the standalone RuleChecker.
MISRA and more
The seamlessly integrated RuleChecker lets you check your code for compliance with various coding standards, including MISRA, CWE, ISO/IEC, SEI CERT, and AUTOSAR. You can easily toggle individual rules and even specific aspects of certain rules. The tool can also check for various code metrics such as comment density or cyclomatic complexity. Custom extensions for your own in-house coding guidelines are available on request.
RuleChecker can be envoked separately, to allow for even faster checks of your code, or in conjunction with the sound semantic analyses offered by Astrée, to additionally guarantee zero false negatives and minimize false positives on semantical rules. No competing standalone MISRA checker can offer this, and no testing environment can match the full data and path coverage provided by the static analysis.
Qualification support
Your usage of Astrée can be qualified according to DO-178B/C, ISO 26262, IEC 61508, EN-50128, the FDA Principles of Software Validation, and other safety standards. We offer special Qualification Support Kits that simplify and automate the qualification process.