Use SPARK Extensively (SWE01)
Level \(\rightarrow\) Advisory
- Category
- Safety:
\(\checkmark\)
- Cyber:
\(\checkmark\)
- Goal
- Maintainability:
\(\checkmark\)
- Reliability:
\(\checkmark\)
- Portability:
\(\checkmark\)
- Performance:
\(\checkmark\)
- Security:
\(\checkmark\)
Remediation \(\rightarrow\) High, as retrofit can be extensive
Verification Method \(\rightarrow\) Compiler restrictions
Reference
Description
SPARK has proven itself highly effective, both in terms of low defects, low development costs, and high productivity. The guideline advises extensive use of SPARK, especially for the sake of formally proving the most critical parts of the source code. The rest of the code can be in SPARK as well, even if formal proof is not intended, with some parts in Ada when features outside the SPARK subset are essential.
Applicable Vulnerability within ISO TR 24772-2
N/A
Applicable Common Weakness Enumeration
Noncompliant Code Example
Any code outside the (very large) SPARK subset is flagged by the compiler.
Compliant Code Example
N/A
Notes
Violations are detected by the SPARK toolset.