Security Networks AG, one of Germany’s largest IT security providers, has adopted the SPARK Pro development environment.
SPARK Pro, a Freely Licensed Open Source Software (FLOSS) product created by AdaCore and Altran Praxis, will be used by Secunet as a strategic technology to build highly robust security-critical applications.
The first Secunet project to apply SPARK Pro will be a multilevel workstation, an interactive system for concurrently handling information of different security domains. To maintain confidentiality and integrity of all processed data, multiple independent levels of security (MILS) are enforced on a single hardware platform.
SPARK Pro was launched in 2009 by Altran Praxis, an international specialist in embedded and critical systems engineering, and AdaCore, the leading provider of commercial software solutions for the Ada language. SPARK Pro provides the foremost language, toolset and design discipline for engineering high-assurance software. It combines Altran Praxis’ renowned SPARK language and verification tools with the GNAT Programming Studio (GPS) and GNATbench development environments by AdaCore.
“For the security-critical parts of our workstation we needed a formal verification technique that was as mature as manageable in a large-scale project,” said Alexander Senier, project manager of secunet's Multilevel Workstation.
“There is an increasing need for writing complex software that meets the highest standards of security. To fully answer this emerging requirement, one needs a state-of-the-art development environment that provides a way to formally verify security properties of the code,” said Cyrille Comar, Managing Director, AdaCore.
“The ability to meet multiple levels of certification within the same application is increasingly critical to the successful deployment of complex projects,” said Keith Williams, Altran Praxis Managing Director. “As Secunet is demonstrating, SPARK Pro provides the perfect solution for those developing advanced high-security software across the globe. We are delighted to be helping secunet with the development of this important new product line.”
Designed by Altran 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.