AdaCore Releases GNAT Pro High-Integrity Edition Version 6.3 For Wind River VxWorks MILS Platform

GNAT Pro High-Integrity Edition for MILS contains the GNAT Pro development environment with compile system, testing tools, and graphical user interface components, to support high-productivity software development. It provides specialised run-time libraries, corresponding to Ada language subsets for those features that can be certified to different EALs. For EALs 1-3, the High-Integrity Edition for MILS provides a full Ada run-time library and development environment for the creation and testing required for these lower-level security certification requirements. For EAL 4, it provides a Ravenscar-compliant run-time library originally created to be certifiable to the DO-178B airborne avionics safety standard. This safety standard has been shown to meet the security assurance requirements for EAL 4. Finally, the Zero Foot Print (ZFP) run-time library is provided, which supports security certification to EALs 5 through 7.

Security certification at EALs 5-7 requires semi-formal or formal approaches. General software application languages are typically not appropriate at these levels. As an option, GNAT Pro High-Integrity Edition for MILS provides the SPARK Pro tool set to support these top levels. The SPARK language is a fully deterministic and verifiable subset of the Ada programming language augmented by pre- and post-condition constructs that more fully specify the application’s logic and information flow. SPARK and the SPARK Pro tool set have been demonstrated in practice to meet the requirements for top security application development. The High-Integrity Edition for MILS thus provides a complete environment for applications that need to be certified at EALs 5-7.

“AdaCore has a long history in providing solutions for developers of high-integrity applications,” said Robert Dewar, President and CEO of AdaCore. “GNAT Pro has been used for avionics systems on aircraft, such as the new Boeing 787, which need to meet the highest level of safety requirements in DO-178B. Developers of high-security applications require the more stringent security objectives be met. To satisfy this need, we have introduced the GNAT Pro High-Integrity Edition for MILS. This product, integrated with the SPARK Pro language and tool set, offers a unique security solution, allowing developers using a MILS architecture to create and certify applications that can meet all EALs from lowest to highest.”

“Wind River VxWorks MILS platform provides a robust MILS architecture, enabling the creation of MLS (Multi-Level Secure) systems in which multiple applications from different domains execute securely on a single instance of silicon,” said Chip Downing, Director of Aerospace and Defense at Wind River. “GNAT Pro High-Integrity Edition for MILS adds the capability to accelerate the certification of Ada applications at high assurance levels on the VxWorks MILS foundation for a very powerful combination for developing secure applications.”