SPARK Pro – Integrated Development and Verification Environment
You simply can’t write better code.
When software failure is unacceptable, ultra-high reliability can be attained at the same level of effort as traditional testing-based methods.
Through the use of formal methods, SPARK Pro prevents, detects and eliminates defects early in the software lifecycle with mathematics-based assurance. It also helps reduce delivery costs and timescales. The SPARK language and tools have a proven track record in the most demanding safety-critical and high-security systems. They are easily learned by software professionals and do not require a background in formal methods.
Features
The primary design goal of the SPARK language is to provide the foundation for a sound formal verification framework and static analysis toolset. The latest version of the language, SPARK 2014, is based on Ada 2012. It embodies a large subset of Ada 2012, while prohibiting those features which are not amenable to static verification and furthermore can be the source of software defects.
Through the SPARK language’s ability to express contracts, the developer can express both requirements and implementation within the same language framework.
SPARK Pro brings software specification, coding, testing, and unit verification by proof within a single integrated framework. Verification goals that would otherwise have to be achieved by diverse techniques such as manual review can be met by applying the SPARK toolsuite, and reports can be generated to satisfy certification requirements.
The SPARK programming language can be used both for new development efforts and incrementally in existing projects in other languages (such as C and C++). It can be combined with testing in an approach known as hybrid verification.
SPARK Pro has been designated as CWE-Compatible by the MITRE Corporation’s Common Weakness Enumeration (CWE) Compatibility and Effectiveness Program. It detects a variety of code weaknesses, including several that are among the CWE’s Top 25 Most Dangerous Software Errors.
- CWE-120 (Classic Buffer Overflow)
“The program copies an input buffer to an output buffer without verifying that the size of the input buffer is less than the size of the output buffer, leading to a buffer overflow.” - CWE-131 (Incorrect Calculation of Buffer Size)
“The software does not correctly calculate the size to be used when allocating a buffer, which could lead to a buffer overflow.” - CWE-190 (Integer Overflow or Wraparound)
“The software performs a calculation that can produce an integer overflow or wraparound, when the logic assumes that the resulting value will always be larger than the original value. This can introduce other weaknesses when the calculation is used for resource management or execution control.”
