The nature of SPARK language means that a certain class of security flaws can be completely avoided. The SPARK Pro tools can detect and mitigate against dangerous programming errors listed by the CWE/SANS experts such as
- improper input validation
- integer overflow or wraparound
- buffer overflow errors
- improper initialization
- improper validation of array index
- information leak
Vulnerabilities introduced by weak or erroneous constructs can be detected and removed early in the system's lifecycle — before the software is even compiled — and long before the software enters testing or evaluation.
SPARK allows designers to specify how information must flow through a program using Dependency contracts. The toolset will check that the implementation conforms to the requirements of these contracts and, where errors occur, will highlight the paths in the code that can lead to security violations.
For the highest levels of assurance, SPARK allows designers to capture key security properties that the implementation must preserve; i.e., by expressing the security requirements as software contracts. The SPARK toolset can then be used to prove that the software will preserve these security properties for all possible states and inputs - something that is impossible to achieve with a testing-based approach to verification for any realistically sized system.
You can use SPARK to achieve assurance at the highest levels of standards such as the Common Criteria and ITSEC, using the evidence that supports the assurance case.
Safety-Critical System Development
Safety-related or safety-critical systems are usually engineered in a highly-regulated environment and clearly require the highest possible levels of software integrity. SPARK is ideally suited to such an environment, as the technology has been shown to meet the requirements of major international standards such as DO-178B/C, CENELEC 50128, IEC 61508, and DEFSTAN 00-56.
- SPARK meets the requirements for a high-level language suited to safe systems development by prohibiting dangerous programming constructs, and it provides a sound basis for static verification.
- The static analysis performed by the SPARK toolset satisfies the requirement (typical of software assurance standards) to detect common programming errors such as buffer overflow.
Based on Ada 2012, the latest version of the SPARK language permits hybrid verification: mixing formal proof and traditional unit testing. You can thus incrementally introduce higher levels of verification and integrity, with the level of formality selected based on the assurance level of the system. You define contracts in a SPARK program using Ada aspects and/or pragmas, and then can verify the contracts through either dynamic checks generated by the compiler or a formal proof driven by the SPARK toolset. Contracts can express a variety of properties, including functional behavior, information flow, and safety and/or security properties.
