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: firstname.lastname@example.org
Keccak is a family of sponge functions that can be used in a variety of cryptographic constructions, including hash functions. NIST selected Keccak as the winner of the SHA-3 contest, and is standardised by NIST in the FIPS 202 standard.
Developed by Daniel King, libkeccak is an implementation of several cryptographic constructions based on the Keccak permutation, including SHA-3 and SHAKE. It is written using the SPARK language and toolset, and its use of formal verification guarantees the absence of common runtime errors such as buffer overflows, numerical overflows, and division by zero.
The Institute for Internet Technologies and Applications (ITA) at the University of Applied Science Rapperswil (HSR) in Switzerland started the Muen Separation Kernel project to create an Open Source foundation for high-assurance platforms. To achieve a trustworthiness exceeding any other Open Source kernel or hypervisor, the absence of runtime-errors is formally proven using AdaCore's and Altran's SPARK language and toolset. A close cooperation with secunet Security Networks AG in Germany throughout the whole design and implementation process ensures that the Muen Separation Kernel meets the requirements of existing and future component-based high-security platforms.
Ironsides (SPARK 2005)
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 (SPARK 2005)
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.
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.
The initial version of SPARKSkein was in SPARK 2005. It has been translated to SPARK 2014 and is now available as a distributed example in the SPARK release.
Echo – A Practical Approach to Formal Verification (SPARK 2005)
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.
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 (SPARK 2005)
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.
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.
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.
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.
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.
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>