SPARK Pro is a modular toolset that can be applied in a range of different industrial scenarios.
Based on Ada 2012, the latest SPARK language permits hybrid verification: mixing formal proof and unit testing. This allows projects to incrementally introduce higher levels of verification and integrity with the level of formality being selected as appropriate to the assurance level of the system. Contracts are inserted into a SPARK program using Ada aspects and pragmas, and allow a program’s specification to be verified either by means of dynamic checks generated by the compiler or formal proof driven by the SPARK toolset. Contracts can express a variety of properties, including functional behavior, information flow, or safety and security properties.
Re-engineering Existing Code
In addition to supporting the construction of new high-integrity applications, SPARK Pro can be applied to improve the quality of existing software. Ada code in the SPARK language subset can be analyzed for commonly-occurring errors such as uninitialized variables, or contracts can be incrementally added to support other modes of verification.
Existing systems written in other languages can also benefit by conversion of a subset of the application to SPARK. For example, a system written in C could have the application logic and control algorithms converted into SPARK whilst the lower-level hardware interface modules remain unchanged. The robustness of the code that has been converted to SPARK can then be improved by the application of SPARK’s static analysis functions. Taking the approach further, it is possible to add contracts to the converted portion of the code and verify that key properties or functional behaviour has been correctly implemented.
Engineering New Systems
Where new systems are being developed, SPARK can be used as part of a correctness-by-construction approach to systems development. The aim of this approach is to save time and costs by ensuring that high integrity code is delivered from the development phase and thus avoid delays in a lengthy test-and-debug cycle. This approach will also deliver high integrity software for embedded and critical consumer devices, thus avoiding expensive product recalls due to software failures. SPARK supports this approach by:
- Using a language that prevents the introduction of many common progamming errors
- Providing a toolset that detects errors early - before the code is compiled and tested
- Generating evidence as you go
Secure Systems Development
SPARK was designed from the outset with security in mind and has a proven track record in the development and verification of software for high-assurance systems. Several attributes make SPARK particularly well-suited to secure systems.
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
Vulnerabilities introduced by weak or erroneous constructs can be detected and removed early in the systems’ lifecycle - before the software is even compiled - and long before the software enters testing or evaluation.
SPARK allows designers to specify the way that 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 ie. a translation of the security requirements of the system into 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 test-based approach to verification for any realistically sized system.
SPARK can be used to support software assurance to the highest levels of standards such as the Common Criteria and ITSEC, producing the evidence that is required to support the assurance case.
Safety-Critical Systems 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 software-related requirements of all 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 provides a sound basis for static verification.
The SPARK toolset performs static analysis functions required by process-based standards that detect the most common programming errors.
The SPARK toolset generates evidence that is essential to supporting the software-integrity aspects of any safety case required for critical systems certification
SPARK has a proven track record in application to a wide variety of industrial domains and high-profile critical systems