SPARK Pro Adopted by secunet

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 devel