SPARK Pro Adopted by secunet

High-assurance development environment selected to implement multi-level security workstation

PARIS, BATH and NEW YORK, July 27th, 2010 – The company secunet Security Networks AG, one of Germany’s largest IT security providers, announced today that it 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 the 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 chosen by secunet because it was the only mature and commercially supported environment suiting the requirements for developing security-critical applications for secunet’s multi-level products. Moreover, SPARK Pro’s formal verification techniques provide the foundation necessary for achieving stringent high-robustness certifications of secunet’s multi-level systems.

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.

SPARK Pro provides increased support for security assurance, including the ability to mix software of different security levels (such as classified and unclassified) within the same system. This MILS functionality meets an increasing trend in the security and defense industries to combine multiple secure and non-secure elements into a single partitioned system to deliver smaller, more integrated solutions.

“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. “SPARK Pro was the only solution that met our requirements, combining trustworthy development tools with excellent support provided directly by the experts. As a strategically important technology SPARK Pro enables us to further enhance the security, certifiability and flexibility of our future high-security solutions.”

Founded in 1997, secunet is one of Germany’s leading providers of superior IT security. Working with its customers – enterprises, public authorities and international organizations – secunet develops and implements high-performance products and state-of-the-art IT security solutions. At secunet, more than 270 experts focus on issues such as cryptography (SINA), e-government, business and automotive security.

“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. “AdaCore and Altran Praxis have combined the best of their technology and expertise to answer this need through the product SPARK Pro. We are very pleased to see customers with such demanding requirements as secunet adopting it.”

“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.

Press Contacts
press@adacore.com

Leena Chauhan
Altran Praxis
leena.chauhan@altran-praxis.com