SPARK Pro is a language — a formally analyzable subset of Ada 2012 — and toolset that brings mathematics-based confidence to software verification.
Use SPARK Pro to formally define and automatically verify software architectural requirements, and to guarantee a wide range of software integrity properties such as freedom from run-time errors, enforcement of safety properties or security policies, and full functional correctness (compliance with a formally defined specification).
The SPARK Language
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.
One of the key features of the SPARK language is the ability to be able to express contracts; i.e., behavioral properties that must be implemented correctly by the developer and can be checked by the verification toolset. SPARK 2014 contracts use the same syntax as Ada 2012, thus allowing the developer to express both requirements and implementation within the same language framework. Contracts can be checked at run time using Ada semantics and/or verified statically by the SPARK toolset.
Head over to our learning site for an interactive introduction to the SPARK programming language and its formal verification tools. You will learn the difference between Ada and SPARK and how to use the various analysis tools that come with SPARK. See the 'Intro to SPARK' course at learn.adacore.com »
Use SPARK at the right level for you
You can adopt the SPARK methodology through a set of tools built on top of the GNAT Pro Toolsuite. SPARK Pro is the most complete toolset for SPARK. SPARK Discovery (included in GNAT Pro) is a reduced toolset that performs the same analyses as SPARK Pro but only comes with one automatic prover instead of three. Other advantages of SPARK Pro over SPARK Discovery include integration of the CodePeer static analyzer proof technology, generation of counterexamples for failed proofs, support for programs using modular arithmetic or floating-point arithmetic, and a lemma library for more difficult proofs.
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. Experience in projects such as Tokeneer shows that formal methods can achieve ultra-high reliability in a cost-effective manner.
Read our booklet that summarizes the contribution that the Ada and SPARK languages and AdaCore’s tools can make to develop and verify correct and secure software.
SPARK Pro offers an integrated approach to the entire software design and verification lifecycle.
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.
Integration in IDEs
The SPARK Pro toolset is fully integrated with GNAT Studio and GNATbench IDEs, so that errors and warnings can be displayed within the same environment as the source code thereby providing a smoother workflow for the developer. Alternatively, the tools can be run in command-line mode, for example to generate the reports required for certification evidence.
Data Flow Analysis
SPARK Pro detects common programming errors that can be the cause of insecurities or incorrect behavior, including references to uninitialized variables. Advanced data flow analysis can be used to check that access to global variables conforms to contracts specified by a software architect, thereby ensuring that the software conforms to its architectural design.
Information Flow Analysis
For more critical applications, dependency contracts can be specified to constrain the information flow allowed in a program (how global variables and formal parameters are used by a subprogram). Violations of these contracts - potentially representing violations of safety or security policies - can then be detected even before the code is compiled.
Absence of Run-Time Exceptions
SPARK Pro can check that a program is free from run-time exceptions such as divide-by-zero, numeric overflow, buffer overflow or out-of-bounds array indices. The mathematical proof system on which SPARK Pro is based guarantees that this analysis is sound, so that even before a program is executed or tested a large class of potentially hard-to-detect errors can be eliminated from your software.
Property Checking
For more critical applications, key safety or security properties can be expressed in the same contract notation as is used in Ada 2012 (for example, subprogram pre- and postconditions). Using a proof system that is mathematically sound, the SPARK Pro toolset can automatically check whether a program will satisfy these properties for all possible inputs and execution paths - as if the program had been exhaustively tested but without ever having to compile or run the code.
Functional Correctness
With its extended contract language, SPARK allows a comprehensive formal specification of a program’s required functional behavior; i.e., a specification of its Low-Level Requirements. The SPARK Pro tools will attempt to prove that a program meets its functional specification, thus providing the highest possible level of assurance for the correct behavior of critical systems.
A CWE Compatible Tool
SPARK Pro has been designated as CWE-Compatible by the MITRE Corporation's Common Weakness Enumeration (CWE) Compatibility and Effectiveness Program and can detect a multitude of code weaknesses, including several that are among, or are in the same class as, the CWE’s Top 25 Most Dangerous Software Errors.
SPARK Pro uses advanced proof technology to verify properties of programs written in the SPARK formally analyzable subset of Ada. The tool can prove properties including validity of data/information flow, absence of run-time errors, system integrity constraints (such as safe state transitions), and, for the most critical software, functional correctness with respect to formally specified requirements. SPARK Pro is a sound static analysis tool -- it will detect all violations of a property that it is attempting to verify -- with a very low false alarm rate.
SPARK Pro will prevent or detect the following CWE weaknesses:
| CWE weakness | Description |
|---|---|
| CWE 119, 120, 123, 124, 125, 126, 127, 129, 130, 131 | Buffer overflow/underflow |
| CWE 136, 137 | Variant record field violation, Use of incorrect type in inheritance hierarchy |
| CWE 188 | Reliance on data layout |
| CWE 190, 191 | Numeric overflow/underflow |
| CWE 193 | Off-by-one error |
| CWE 194 | Unexpected sign extension |
| CWE 197 | Numeric truncation error |
| CWE 252, 253 | Unchecked or incorrectly checked return value |
| CWE 366 | Race Condition |
| CWE 369 | Division by zero |
| CWE 456, 457 | Use of uninitialized variable |
| CWE 466, 468, 469 | Pointer errors |
| CWE 476 | Null pointer dereference |
| CWE 562 | Return of stack variable address |
| CWE 563 | Unused or redundant assignment |
| CWE 682 | Range constraint violation |
| CWE 786, 787, 788, 805 | Buffer access errors |
| CWE 820 | Missing synchronization |
| CWE 821 | Incorrect synchronization |
| CWE 822, 823, 824, 825 | Pointer errors |
| CWE 835 | Infinite loop |
Capgemini Engineering and AdaCore have formed a long-term partnership with the intent of taking the SPARK language and toolset to a new level in technical capability.
Customer Projects: SPARK Pro
NVIDIA
AdaCore enhances security-critical firmware with NVIDIA
NVIDIA plans to upgrade select security-critical firmware software, rewriting it from C to Ada and SPARK to increase verification efficiencies to achieve compliance with the functional safety standard ISO-26262.
QinetiQ
Security and Defence Contractor QinetiQ Selects AdaCore’s Mentorship Service to Upgrade to the Latest Version of the SPARK Technology
QinetiQ is looking to SPARK to address software tool obsolescence by modernising the development environment for its Trials Control System (TCS).
DENSO
DENSO Using SPARK Technology for Automotive Research Project
AdaCore and the University of Nagasaki successfully completed a joint research project for DENSO, Application of Formal Methods to Help Achieve Freedom from Interference, with the goal of simplifying the development of safety-critical automotive applications in an ISO 26262 context.
TOYOTA ITC
TOYOTA ITC Japan Selects SPARK Pro Language and Toolset for High-Reliability Research Project
TOYOTA InfoTechnology Center (ITC) Japan selected the SPARK language and SPARK Pro toolset for a research project to develop a vehicle component implementation that can be proven to be free of run-time errors.
Secunet
SPARK Pro Adopted by secunet
To develop a robust multi-level security workstation, Secunet Security Networks chose the SPARK Pro development environment. The security station concurrently handles information of different security domains, maintains confidentiality and integrity of all processed data, and enforces Multiple Independent Levels of Security (MILS) on a single hardware platform.
NATS
GNAT Pro Chosen for UK’s Next Generation ATC System
iFACTS is the future of air traffic control. The combination of Praxis’ experience in critical systems engineering and the high integrity of SPARK Ada enabled the development of this vitally important and sophisticated system.
Vermont Technical College
SPARK Going to the Moon
The GNAT Pro and SPARK language toolsets have been selected for the Lunar IceCube project by Vermont Technical College. Lunar IceCube is a 6-Unit CubeSat mission sponsored by NASA through their NextSTEP initiative. The mission will prospect for water and other lunar volatiles in all forms (solid, liquid, and vapor) from a highly elliptical orbit with a low point of 100 kilometers (60 miles) where the data will be gathered, and a high point of 5,000 kilometers (3,100 miles).
JTEKT
Electric Power Steering System Supplier JTEKT Selects SPARK Pro for Safety-Critical Automotive Software
JTEKT demonstrated how to leverage the SPARK Ada language subset and formal methods to facilitate unit testing and verification of the system’s C code to ensure that it was correct.
Expert Support
Integral to every one of our products are the consulting and support services we provide to our customers. While every company says they offer excellent support, for us it‘s a critical part of our business model and something we take very seriously.