SPARK Pro adopté par Secunet pour le développement de logiciels de haute sécurité
L’environnement de développement à haut degré d’assurance a été choisi pour la réalisation de postes de travail fonctionnant sur plusieurs niveaux de sécurité
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 organisations – 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.
About Altran Praxis
Altran Praxis is a specialist systems and software house, focused on the engineering of systems with demanding safety, security or innovation requirements. Altran Praxis leads the world in specific areas of advanced systems engineering and innovation such as: ultra low defect software engineering, Human Machine Interface (HMI), safety engineering for complex or novel systems and tools (such as SPARK) /methods for systems engineering. It offers clients a range of services including turnkey systems development, consultancy, training and R&D. Key market sectors are aerospace and defence, rail, nuclear, air traffic management, automotive, medical and security. The company operates globally with active projects in the US, Asia and Europe. The headquarters of Altran Praxis are in Bath (UK) with offices in Sophia Antipolis, London, Paris, Loughborough and Bangalore. Altran Praxis is an expertise centre within, and wholly owned by, Altran which is a global leader in innovation engineering and employs 18,000 staff across the world.
www.altran-praxis.com
About AdaCore
Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, the state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore's flagship product is the GNAT Pro development environment, which comes with expert on-line support and is available on more platforms than any other Ada technology. AdaCore has an extensive world-wide customer base;
Read further information.
Ada and GNAT Pro see a growing usage in high-integrity and safety-certified applications, including commercial aircraft avionics, military systems, air traffic management/control, railway systems and medical devices, and in security-sensitive domains such as financial services.
AdaCore has North American headquarters in New York and European headquarters in Paris.
www.adacore.com
Press contacts:
Jamie Ayre
AdaCore
press@adacore.com
Leena Chauhan
Altran Praxis
press@altran-praxis.com
Gerry Grewal/Chrissie McGoldrick
Speed
altran-praxis@speedcommunications.com
Back to top