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

SPARK User's Guide, section 8: "Applying SPARK in Practice"

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

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.