The following are some examples of how SPARK is being used in the software community and in Academic projects and courses around the world.
Have something you’d like to see listed here? Send us an email about it: info@adacore.com
Ironsides
Dr. Martin C. Carlisle, the director of the Academy Center for Cyberspace Research at the United States Air Force Academy has developed a secure DNS server using Ada and the SPARK formal methods tool set.
IRONSIDES is an authoritative DNS server that is provably invulnerable to many of the problems that plague other servers. It achieves this property through the use of formal methods in its design, in particular the language Ada and the SPARK formal methods tool set. Code validated in this way is provably exception-free, contains no data flow errors, and terminates only in the ways that its programmers explicitly say that it can. These are very desirable properties from a computer security perspective.
libsparkcrypto
Written by Alexander Senier of secunet Security Networks AG, libsparkcrypto is a formally verified SPARK implementation of several widely used symmetric cryptographic algorithms, including SHA, AES and RIPEMD. For the complete library, proofs of the absence of run-time errors like type range violations, division by zero and numerical overflows are available.
SPARKSkein
Skein is a new family of cryptographic hash functions designed for speed, security and simplicity.
Produced by Altran and AdaCore, SPARKSkein is a reference implementation of the Skein algorithm, written and verified using the SPARK language and toolset. This implementation is designed to be easily readable and completely portable to a wide variety of machines. It is has been subjected to a complete proof of type safety using the SPARK proof tools, thereby guaranteeing that it is free from such run time exceptions as buffer overflow or division by zero.
Echo – A Practical Approach to Formal Verification
At the University of Virginia, Dr. John Knight and his student, Xiang Yin, have created a practical approach to formal verification called Echo. In Echo verification, a program is verified to conform to its specification using the SPARK proof tools.
Echo’s strategy of splitting the formal verification process down the middle and attacking it from both sides dramatically reduces the effort needed to complete a formal verification, enabling Dr. Knight and his students to complete verification of systems as large as 10,000 lines of SPARK code.
CubeSat
A CubeSat is a miniaturised satellite with dimensions of 10×10x10cm which can be doubled or tripled in length. Its combination of size and standardised components make it a much cheaper method of space research than traditional satellites. Consequently it has been rapidly adopted by universities and research institutions around the world for projects covering areas as diverse as earthquake detection and wildlife tracking.
SPARK will be used to develop the software behind a CubeSat project being led by Professor Carl Brandon of Vermont Technical College. The proposed CubeSat will be a lunar lander with four mini-thrusters on the bottom to maximize control and maneuverability. This will be the first CubeSat that can be launched from a geostationary orbit to successfully land on the moon.
The CubeSat electronics are based on a Texas Instruments (TI) MSP430 processor and the software will control navigation, communications, scientific instruments, camera and the CubeSat’s propulsion system.
Tokeneer
Developed by Altran Praxis under contract from the US NSA, Tokeneer is a complete demonstration of high-assurance software engineering. This development and research work has now been made available by the NSA to the software development and security communities in an effort to prove that it is possible to develop secure systems rigorously in a cost effective manner.
HOL/SPARK
Written by Stefan Berghofer of secunet Security Networks AG, HOL/SPARK is a plug-in for the Isabelle proof assistant. The HOL/SPARK plug-in provides an interactive environment for proving verification conditions generated from SPARK programs as an alternative to the standard SPARK proof tools.
SparkSure Proof Tools
Phil Thornley, of independent consultancy SparkSure, has written and made available a suite of tools for assisting with SPARK proofs. These include: SPARKRules, a utility program for managing proof libraries; VC_View, a tool to assist with interpretation of VCs, and; PCHIF, a tool that assists with the management of the Proof Checker command history.
SPARKUnit
Written by Alexander Senier of secunet Security Networks AG, SPARKUnit is a unit test framework for the SPARK programming language. It enables the developer to create unit tests in SPARK which can be analysed by the SPARK Examiner. This allows for testing of SPARK operations with preconditions and flow analysis of test cases.
ViCToR
Designed by Dr Paul Jackson at the University of Edinburgh, ViCToR is a framework for translating SPARK-generated verification condiditions into the SMTLib language, and then applying modern SMT-based provers to them. ViCToR forms the core of the SPARKBridge technology included in recent releases of the SPARK Toolset.
Kansas State University
In the Computing and Information Sciences Department at Kansas State University, Dr. John Hatcliff teaches SPARK as part of the Software Specifications module – a course which presents cutting-edge tool-based specification and verification technologies./p>
Swansea University
In the Department of Computer Science at Swansea University, Dr. Anton Setzer uses SPARK to illustrate the principles of high integrity software engineering for critical systems.
Get a first hand look at the SPARK programming language from the following code samples we’ve assembled. You can view each example online or download the files and work with them locally. Have fun!
-
All you can SPARK on a database
This small database example (around 300 loc) presents a tour of SPARK capabilities, regarding the various types of analysis (data and control coupling, security, proof of absence of run-time errors, proof of complex functional contracts) and architecture of SPARK code (abstraction and refinement, integration with foreign code and non-SPARK constructs). This example was the basis for a series of video demos which show the step-by-step mixed development and verification of the database code. -
Linear Search
This very simple implementation of a linear search over an array in SPARK contains the main SPARK annotations for data-flow, information-flow, abstraction of state, proof of absence of run-time errors and proof of functional contracts. The SPARK tool-set proves all VCs. -
Permutations
Using a simple variable length array type, provide an operation which, given a length N, returns a random permutation of the Integers in the range 1 .. N, generated using a Knuth shuffle. Illustrates the use of an incomplete specification (spec for Random_Integers.Get states only that it returns an Integer) and of rules files. -
Slice Sums
This example provides operations for computing the sum of the elements of a slice of an array of integers and for finding the bounds of a slice of a given array having a maximal sum. It illustrates some typical SPARK techniques for working with overflow checking and with loop invariants. -
Stable Marriage
Given, for each member of two groups of the same size, a ranking of the members of the other group, use the Gale-Shapely algorithm to find a matching between the two groups such that no unmatched couple exists who each rank the other higher than their assigned match. Illustrates some fairly nontrivial invariants. -
VSComp2010
This archive contains solutions in SPARK to all 5 problems from the first Verified Software Competition held in 2010 at VSTTE conference. Solutions range from the very simple, with a single loop, to the much more complex, with backtracking over nested loops (n-queens problem) and an axiomatization of lists in FDL (linked-lists problem). While some solutions are partial, all VCs are proved automatically by the SPARK tool-set.
Learn more about the commercially supported version of SPARK – SPARK Pro