SPARK (programming language)

SPARKis aformally definedcomputerprogramming languagebased on theAdaprogramming language, intended for the development ofhigh integrity softwareused in systems where predictable and highly reliable operation is essential. It facilitates the development of applications that demand safety, security, or business integrity.
Originally, there were three versions of the SPARK language (SPARK83, SPARK95, SPARK2005) based on Ada 83, Ada 95 and Ada 2005 respectively.
A fourth version of the SPARK language, SPARK 2014, based on Ada 2012, was released on April 30, 2014. SPARK 2014 is a complete re-design of the language and supportingverificationtools.
The SPARK language consists of a well-defined subset of the Ada language that usescontractsto describe the specification of components in a form that is suitable for both static and dynamic verification.
In SPARK83/95/2005, the contracts are encoded in Ada comments and so are ignored by any standard Ada compiler, but are processed by the SPARK "Examiner" and its associated tools.
SPARK 2014, in contrast, uses Ada 2012's built-in "aspect" syntax to express contracts, bringing them into the core of the language. The main tool for SPARK 2014 (GNATprove) is based on theGNAT/GCC infrastructure, and re-uses almost the entirety of the GNAT Ada 2012 front-end.
SPARK utilises the strengths of Ada while trying to eliminate all its potential ambiguities and insecure constructs. SPARK programs are by design meant to be unambiguous, and their behavior is required to be unaffected by the choice of Adacompiler. These goals are achieved partly by omitting some of Ada's more problematic features (such as unrestrictedparallel tasking) and partly by introducing contracts that encode the application designer's intentions and requirements for certain components of a program.
The combination of these approaches allows SPARK to meet its design objectives, which are:
Consider the Ada subprogram specification below:
In pure Ada this might increment the variableXby one or one thousand; or it might set some global counter toXand return the original value of the counter inX; or it might do absolutely nothing withXat all.
With SPARK 2014, contracts are added to the code to provide additional information regarding what a subprogram actually does. For example, we may alter the above specification to say:
This specifies that theIncrementprocedure does not use (neither update nor read) any global variable and that the only data item used in calculating the new value ofXisXitself.
Alternatively, the designer might specify:
This specifies thatIncrementwill use the global variableCountin the same package asIncrement, that the exported value ofCountdepends on the imported values ofCountandX, and that the exported value ofXdoes not depend on any variables at all and it will be derived from constant data only.
If GNATprove is then run on the specification and corresponding body of a subprogram, it will analyse the body of the subprogram to build up a model of the information flow. This model is then compared against what has been specified by the annotations and any discrepancies reported to the user.
These specifications can be further extended by asserting various properties that either need to hold when a subprogram is called (preconditions) or that will hold once execution of the subprogram has completed (postconditions). For example, we could say the following:
This, now, specifies not only thatXis derived from itself alone, but also that beforeIncrementis calledXmust be strictly less than the last possible value of its type (to ensure that the result will neveroverflow) and that afterwardsXwill be equal to the initial value ofXplus one.
GNATprove can also generate a set ofverification conditionsor VCs. These conditions are used to establish whether certain properties hold for a given subprogram. At a minimum, the GNATprove will generate VCs to establish that all run-time errors cannot occur within a subprogram, such as:
If a postcondition or any other assertion is added to a subprogram, GNATprove will also generate VCs that require the user to show that these properties hold for all possible paths through the subprogram.
Under the hood, GNATprove uses the Why3 intermediate language and VC Generator, and theCVC4,Z3, andAlt-Ergotheorem provers to discharge VCs. Use of other provers (including interactive proof checkers) is also possible through other components of the Why3 toolset.
The first version of SPARK (based on Ada 83) was produced at theUniversity of Southampton(with UKMinistry of Defencesponsorship) by Bernard Carré and Trevor Jennings. The nameSPARKwas derived fromSPADE Ada Kernel, in reference to theSPADEsubset of thePascal programming language.
Subsequently the language was progressively extended and refined, first by Program Validation Limited and then by Praxis Critical Systems Limited. In 2004, Praxis Critical Systems Limited changed its name to Praxis High Integrity Systems Limited. In January 2010, the company becameAltran Praxis.
In early 2009, Praxis formed a partnership with AdaCore, and released "SPARK Pro" under the terms of the GPL. This was followed in June 2009 by the SPARK GPL Edition 2009, aimed at theFOSSand academic communities.
In June 2010, Altran-Praxis announced that the SPARK programming language would be used in the software of US Lunar projectCubeSat, expected to be completed in 2015.
In January 2013, Altran-Praxis changed its name to Altran, which in April 2021 becameCapgemini Engineering(following Altran's merger withCapgemini).
The first Pro release of SPARK 2014 was announced on April 30, 2014, and was quickly followed by the SPARK 2014 GPL edition, aimed at theFLOSSand academic communities.
SPARK has been used in several high profile safety-critical systems, covering commercial aviation (Rolls-Royce Trentseries jet engines, theARINC ACAMS system, theLockheed Martin C130J), military aviation (EuroFighter Typhoon,Harrier GR9,AerMacchi M346), air-traffic management (UKNATS iFACTSsystem), rail (numerous signalling applications), medical (the LifeFlowventricular assist device), and space applications (theVermont Technical College CubeSat project).
SPARK has also been used in secure systems development. Users includeRockwell Collins(Turnstile and SecureOne cross-domain solutions), the development of the originalMULTOSCA, the NSATokeneerdemonstrator, the secunet multi-level workstation, the Muen separation kernel andGenodeblock-device encrypter.
In August 2010, Rod Chapman, principal engineer of Altran Praxis, implementedSkein, one of candidates forSHA-3, in SPARK. In comparing the performance of the SPARK and C implementations and after careful optimization, he managed to have the SPARK version run only about 5 to 10% slower than C. Later improvement to the Ada middle-end in GCC (implemented by Eric Botcazou of AdaCore) closed the gap, with the SPARK code matching the C in performance exactly.
NVIDIA have also adopted SPARK for the implementation of security-critical firmware.
In 2020, Rod Chapman re-implemented theTweetNaClcryptographic library in SPARK 2014.The SPARK version of the library has a complete auto-active proof of type-safety, memory-safety and some correctness properties, and retains constant-time algorithms throughout. The SPARK code is also significantly faster than TweetNaCl.