SPARK (programming language)

Last updated

SPARK
Sparkada.jpg
Paradigm Multi-paradigm
Developer Altran and AdaCore
Stable release
Community 2021 / June 1, 2021;17 months ago (2021-06-01)
Typing discipline static, strong, safe, nominative
OS Cross-platform: Linux, Microsoft Windows, Mac OS X
License GPLv3
Website About SPARK
Major implementations
SPARK Pro, SPARK GPL Edition, SPARK Community
Influenced by
Ada, Eiffel

SPARK is a formally defined computer programming language based on the Ada programming language, intended for the development of high integrity software used in systems where predictable and highly reliable operation is essential. It facilitates the development of applications that demand safety, security, or business integrity.

Contents

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 supporting verification tools.

The SPARK language consists of a well-defined subset of the Ada language that uses contracts to 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 the GNAT/GCC infrastructure, and re-uses almost the entirety of the GNAT Ada 2012 front-end.

Technical overview

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 Ada compiler. These goals are achieved partly by omitting some of Ada's more problematic features (such as unrestricted parallel tasking) and partly by introducing contracts which 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:

Contract examples

Consider the Ada subprogram specification below:

procedure Increment (X : in out Counter_Type);

In pure Ada this might increment the variable X by one or one thousand; or it might set some global counter to X and return the original value of the counter in X; or it might do absolutely nothing with X at 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:

procedure Increment (X : in out Counter_Type)   with Global => null,        Depends => (X => X);

This specifies that the Increment procedure does not use (neither update nor read) any global variable and that the only data item used in calculating the new value of X is X itself.

Alternatively, the designer might specify:

procedure Increment (X : in out Counter_Type)   with Global  => (In_Out => Count),        Depends => (Count  => (Count, X),                    X      => null);

This specifies that Increment will use the global variable Count in the same package as Increment, that the exported value of Count depends on the imported values of Count and X, and that the exported value of X does 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 that which 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:

procedure Increment (X : in out Counter_Type)   with Global  => null,        Depends => (X => X),        Pre     => X < Counter_Type'Last,        Post    => X = X'Old + 1;

This, now, specifies not only that X is derived from itself alone, but also that before Increment is called X must be strictly less than the last possible value of its type (to ensure that the result will never overflow) and that afterwards X will be equal to the initial value of X plus one.

Verification conditions

GNATprove can also generate a set of verification conditions or 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 the CVC4, Z3, and Alt-Ergo theorem provers to discharge VCs. Use of other provers (including interactive proof checkers) is also possible through other components of the Why3 toolset.

History

The first version of SPARK (based on Ada 83) was produced at the University of Southampton (with UK Ministry of Defence sponsorship) by Bernard Carré and Trevor Jennings. The name SPARK was derived from SPADE Ada Kernel, in reference to the SPADE subset of the Pascal programming language. [1]

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 became Altran 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 the FOSS and academic communities.

In June 2010, Altran-Praxis announced that the SPARK programming language would be used in the software of US Lunar project CubeSat , expected to be completed in 2015.

In January 2013, Altran-Praxis changed its name to Altran which in April 2021 became Capgemini Engineering (following Altran's merger with Capgemini).

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 the FLOSS and academic communities.

Industrial applications

SPARK has been used in several high profile safety-critical systems, covering commercial aviation (Rolls-Royce Trent series jet engines, the ARINC ACAMS system, the Lockheed Martin C130J), military aviation (EuroFighter Typhoon, Harrier GR9, AerMacchi M346), air-traffic management (UK NATS iFACTS system), rail (numerous signalling applications), medical (the LifeFlow ventricular assist device), and space applications (the Vermont Technical College CubeSat project).[ citation needed ]

SPARK has also been used in secure systems development. Users include Rockwell Collins (Turnstile and SecureOne cross-domain solutions), the development of the original MULTOS CA, the NSA Tokeneer demonstrator, the secunet multi-level workstation, the Muen separation kernel and Genode block-device encrypter.

In August 2010, Rod Chapman, principal engineer of Altran Praxis, implemented Skein, one of candidates for SHA-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. [2]

NVIDIA have also adopted SPARK for the implementation of security-critical firmware. [3]

In 2020, Rod Chapman re-implemented the TweetNaCl cryptographic library in SPARK 2014. [4] 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.

See also

Related Research Articles

<span class="mw-page-title-main">Ada (programming language)</span> High-level programming language first released in 1980

Ada is a structured, statically typed, imperative, and object-oriented high-level programming language, extended from Pascal and other languages. It has built-in language support for design by contract (DbC), extremely strong typing, explicit concurrency, tasks, synchronous message passing, protected objects, and non-determinism. Ada improves code safety and maintainability by using the compiler to find errors in favor of runtime errors. Ada is an international technical standard, jointly defined by the International Organization for Standardization (ISO), and the International Electrotechnical Commission (IEC). As of 2020, the standard, called Ada 2012 informally, is ISO/IEC 8652:2012.

<span class="mw-page-title-main">Garbage collection (computer science)</span> Form of automatic memory management

In computer science, garbage collection (GC) is a form of automatic memory management. The garbage collector attempts to reclaim memory which was allocated by the program, but is no longer referenced; such memory is called garbage. Garbage collection was invented by American computer scientist John McCarthy around 1959 to simplify manual memory management in Lisp.

<span class="mw-page-title-main">COBOL</span> Programming language with English-like syntax

COBOL is a compiled English-like computer programming language designed for business use. It is an imperative, procedural and, since 2002, object-oriented language. COBOL is primarily used in business, finance, and administrative systems for companies and governments. COBOL is still widely used in applications deployed on mainframe computers, such as large-scale batch and transaction processing jobs. However, due to its declining popularity and the retirement of experienced COBOL programmers, programs are being migrated to new platforms, rewritten in modern languages or replaced with software packages. Most programming in COBOL is now purely to maintain existing applications; however, many large financial institutions were still developing new systems in COBOL as late as 2006.

<span class="mw-page-title-main">GNU Debugger</span> Source-level debugger

The GNU Debugger (GDB) is a portable debugger that runs on many Unix-like systems and works for many programming languages, including Ada, C, C++, Objective-C, Free Pascal, Fortran, Go, and partially others.

<span class="mw-page-title-main">Design by contract</span> Approach for designing software

Design by contract (DbC), also known as contract programming, programming by contract and design-by-contract programming, is an approach for designing software.

In computer science, control flow is the order in which individual statements, instructions or function calls of an imperative program are executed or evaluated. The emphasis on explicit control flow distinguishes an imperative programming language from a declarative programming language.

<span class="mw-page-title-main">Program counter</span> Processor register that indicates where a computer is in its program sequence

The program counter (PC), commonly called the instruction pointer (IP) in Intel x86 and Itanium microprocessors, and sometimes called the instruction address register (IAR), the instruction counter, or just part of the instruction sequencer, is a processor register that indicates where a computer is in its program sequence.

Generic programming is a style of computer programming in which algorithms are written in terms of types to-be-specified-later that are then instantiated when needed for specific types provided as parameters. This approach, pioneered by the ML programming language in 1973, permits writing common functions or types that differ only in the set of types on which they operate when used, thus reducing duplication. Such software entities are known as generics in Ada, C#, Delphi, Eiffel, F#, Java, Nim, Python, Go, Rust, Swift, TypeScript and Visual Basic .NET. They are known as parametric polymorphism in ML, Scala, Julia, and Haskell ; templates in C++ and D; and parameterized types in the influential 1994 book Design Patterns.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

<span class="mw-page-title-main">Isabelle (proof assistant)</span> Higher-order logic (HOL) automated theorem prover

The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring — yet supporting — explicit proof objects.

<span class="mw-page-title-main">Semaphore (programming)</span> Variable used in a concurrent system

In computer science, a semaphore is a variable or abstract data type used to control access to a common resource by multiple threads and avoid critical section problems in a concurrent system such as a multitasking operating system. Semaphores are a type of synchronization primitive. A trivial semaphore is a plain variable that is changed depending on programmer-defined conditions.

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

In computer programming, a parameter or a formal argument is a special kind of variable used in a subroutine to refer to one of the pieces of data provided as input to the subroutine. These pieces of data are the values of the arguments with which the subroutine is going to be called/invoked. An ordered list of parameters is usually included in the definition of a subroutine, so that, each time the subroutine is called, its arguments for that call are evaluated, and the resulting values can be assigned to the corresponding parameters.

<span class="mw-page-title-main">For loop</span> Control flow statement for repeated execution

In computer science a for-loop or for loop is a control flow statement for specifying iteration. Specifically, a for loop functions by running a section of code repeatedly until a certain condition has been satisfied.

Beaujolais effect is the name given to a class of potential semantic errors in Jean Ichbiah's draft specifications for the programming language Ada. The name arose from Ichbiah's promise to give a bottle of Beaujolais nouveau red wine to anyone who could find such a situation in the draft language standard. At least one bottle was actually awarded for such a discovery.

The High Precision Event Timer (HPET) is a hardware timer available in modern x86-compatible personal computers. Compared to older types of timers available in the x86 architecture, HPET allows more efficient processing of highly timing-sensitive applications, such as multimedia playback and OS task switching. It was developed jointly by Intel and Microsoft and has been incorporated in PC chipsets since 2005. Formerly referred to by Intel as a Multimedia Timer, the term HPET was selected to avoid confusion with the software multimedia timers introduced in the MultiMedia Extensions to Windows 3.0.

Altran UK is a division of parent company Altran. Altran Praxis was a British software house that specialised in critical systems. This role is continued under the banner of high-tech engineering consultancy services provided by the rest of the Altran group.

In computer programming, a function or subroutine is a sequence of program instructions that performs a specific task, packaged as a unit. This unit can then be used in programs wherever that particular task should be performed.

PL/SQL is Oracle Corporation's procedural extension for SQL and the Oracle relational database. PL/SQL is available in Oracle Database, Times Ten in-memory database, and IBM Db2. Oracle Corporation usually extends PL/SQL functionality with each successive release of the Oracle Database.

<span class="mw-page-title-main">Incremental encoder</span>

An incremental encoder is a linear or rotary electromechanical device that has two output signals, A and B, which issue pulses when the device is moved. Together, the A and B signals indicate both the occurrence of and direction of movement. Many incremental encoders have an additional output signal, typically designated index or Z, which indicates the encoder is located at a particular reference position. Also, some encoders provide a status output that indicates internal fault conditions such as a bearing failure or sensor malfunction.

References

  1. "SPARK - The SPADE Ada Kernel (including RavenSPARK)". AdaCore. Retrieved 30 June 2021.
  2. Handy, Alex (24 August 2010). "Ada-derived Skein crypto shows SPARK". SD Times . BZ Media LLC. Retrieved 31 August 2010.
  3. "Securing the Future of Safety and Security of Embedded Software". 8 January 2020.
  4. "SPARKNaCl". 8 October 2021.

Further reading