NEW YORK, PARIS, and CEDAR RAPIDS, Iowa, September 17, 2012 – Design East Boston 2012 – AdaCore today announced the successful usage of its SPARK Pro and GNAT Pro High-Security products by Rockwell Collins in the development of the SecureOneTM Guard, a high assurance cross domain guard for military tactical systems. The SecureOne Guard has strict requirements for reliability and security. In order to meet these needs, Rockwell Collins selected SPARK Pro and GNAT Pro High-Security as key development tools for the project.
Rockwell Collins selected the GNAT Pro High-Security and Spark Pro development tools to support the redeployment of the cross domain guard software from the UCDMO Baseline-approved TurnstileTM Cross Domain Guard to a Multiple Independent Levels of Security (MILS) Real Time Operating System (RTOS) as part of the SecureOne project development. The SecureOne Guard is one of the five SecureOne cross domain technologies for high assurance military tactical systems.
“Software at the highest security assurance levels needs to be developed with the most trustworthy languages and tools,” said Robert Dewar, AdaCore President and CEO. “The SPARK programming language, and its supporting toolset, meets these requirements, allowing formal demonstration of security-related properties, such as absence of run-time exceptions. We are pleased that Rockwell Collins, a longstanding AdaCore customer, chose our SPARK Pro tools and GNAT Pro High-Security technology to develop the SecureOne components.”
About SPARK Pro and GNAT Pro High-Security
SPARK Pro provides the foremost language, toolset and design discipline for the engineering of high-assurance software. It combines the renowned SPARK language and verification tools fromAltran Praxis with the GNAT Programming Studio (GPS) development environment from AdaCore. SPARK is a language specifically designed to support the development of software used in applications where correct operation is vital either for reasons of safety or security. SPARK Pro prevents, detects and eliminates defects early in the life-cycle as the source code is developed.
GNAT Pro High-Security (previously known as GNAT Pro High-Integrity Edition for MILS) is a robust and flexible Ada development environment that includes tools and libraries to support all EALs from 1-7 depending on the application’s security requirements. The optional SPARK Pro toolset component of GNAT Pro High-Security was designed to support formal proof of correctness to meet high security requirements for levels EAL 5 and higher. At its core is the SPARK language (designed by Altran Praxis), a deterministic and semantically clear subset of the Ada programming language augmented by semantic contracts to clearly specify a component’s preconditions, postconditions, and invariants.
About SecureOne
SecureOne is a family of high assurance cross domain technologies, providing trusted multi-classification information sharing for military tactical systems. Using SecureOne, users can securely access both unclassified and classified data on the same equipment while benefiting from reduced size, weight and power.
For further information about SecureOne please visit:
http://www.rockwellcollins.com/sitecore/content/Data/News/2011_Cal_Yr/GS/FY11GSNR28-SecureOne.aspx
About AdaCore
Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, a 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; see http://www.adacore.com/home/company/customers/ for 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, railroad systems, and medical devices, and in security-sensitive domains, such as financial services and military communications. The SPARK language, designed by Altran Praxis, and the SPARK Pro toolset, available from AdaCore, are especially useful in such contexts.
AdaCore has North American headquarters in New York and European headquarters in Paris. www.adacore.com
