AdaCore (New York) and Altran Praxis (Bath, UK) have updated the SPARK open source development environment with the introduction of SPARK Pro 9 which provides increased security functionality, including the ability to verify and assure multiple independent levels of security (MILS) within the same application as well as support for the latest SPARK2005 language profile.
SPARK Pro was created one year ago by Altran Praxis and AdaCore to provides a language, toolset and design discipline for engineering high-assurance software. It combines Altran Praxis' SPARK language and verification tools, with the GNAT Programming Studio (GPS) and GNATbench development environments from AdaCore.
SPARK Pro 9 provides the ability to mix software of different security levels (such as classified and unclassified) within the same system. This MILS functionality is designed to meet the increasing trend in the aerospace and defence industries to combine multiple secure and non-secure elements into a single system to deliver smaller, more integrated solutions.
Over half the features added in SPARK Pro 9 are the result of customer feedback. As well as support for the advanced features of SPARK2005, the latest version of the SPARK language, closer integration between SPARK and GPS results in improved usability and faster development times.
Developed by Praxis, SPARK is a language specifically designed to support the development of software used in applications where correct operation is vital for reasons of safety, security, or both. The SPARK toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset also generates evidence for correctness that can be used to build a constructive assurance case in line with the requirements of industry regulators and certification schemes.
There are versions of SPARK based on Ada 83, Ada 95, and Ada 2005, so all standard Ada compilers and tools work out-of-the-box with SPARK.
Functions added include a new information-flow verification for safety and security policies, such as Bell-LaPadula, based on integrity labelling of variables, inputs and outputs. This facility allows users to confirm intended separation properties, and to prevent violations of the chosen information flow policy.
The ZombieScope tool has been added which detects dead statements, branches and paths in SPARK code, complementing the capabilities of the Simplifier and proof status summarizer POGS.
The Examiner now generates cross-reference information that can be consumed by GPS to drive navigation within annotations.
Function return annotations are now treated more like procedure post-conditions, being substituted into the VC hypotheses of the caller. This can dramatically improve the effectiveness of the theorem prover for those calling units, as well as reducing the manual work required by the user to provide rewrite rules.
A new output format for POGS has been included which is designed to be both easier to read and easier to search automatically. It also reflects the results of the ZombieScope tool.
All proof material is now in one manual, and a new global index (in both clickable PDF and HTML forms) simplifies finding topics in the entire manual set.
See also: Altran merges embedded operations