When Software Must Be Safe and Secure

The GNAT Pro High-Integrity Edition for MILS is a product designed specifically to meet high-security requirements of Evaluation Assurance Levels (EAL) 5-7 and can also be used for applications at lower levels (EAL 1-4). The product provides a full-Ada support library and several specialized run-time libraries that simplify certification. It optionally includes the SPARK Pro tool set, supporting both semi-formal and formal proofs of correctness. SPARK Pro can be used at lower EALs to increase confidence in higher reliability or to specifically meet a Protection Profile (PP) for EAL 5 and higher. The High-Integrity Edition for MILS includes a specialized version of GNAT Pro with a graphical user interface for the SPARK Pro tool set, language sensitive editors, compile system, debugger, various testing tools, and specialized run-time libraries to aid in security certification.

EAL Applicability 1-3, 4, 5-7

The GNAT Pro High-Integrity Edition for MILS includes tools and libraries to support all EALs from 1-7.

Limited testing and proof of correctness are required for EAL 1-3. For such systems GNAT Pro High-Integrity Edition for MILS includes a full Ada run-time library and development support tools. To meet EAL 4 the High-Integrity Edition for MILS includes several specialized run-time libraries that have been previously certified to the DO-178B avionics safety standard; formal studies have shown that use of such libraries can reduce the cost for security certification for this level. For EAL 5 and higher the High-Integrity Edition for MILS with SPARK Pro provide the necessary capabilities to meet these top security requirements. Applications at these levels must be developed in a manner to exactly specify their semantic operation. Tools must be available to formally prove correctness, and run-time libraries must be available that are verifiable to the same (or higher) level as the desired security classification of the application.

How AdaCore products meet the requirements of different EAL levels

* Also available for applications needing to meet EAL 1-3 using the SPARK language subset for development.
** Also available for applications needing to meet EAL 4, but this capability is not required by the EAL.

Language

The optional SPARK Pro toolset component of the GNAT Pro High-Integrity Edition for MILS was designed to meet high security requirements. At its core is the SPARK language, 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. SPARK Pro supports formal proof of correctness, helping to meet security requirements for levels EAL 5 and higher.

Libraries

GNAT Pro High-Integrity Edition for MILS includes several run-time libraries, supporting multiple EALs depending on the application’s security requirements. For EAL 1-3 a full Ada run-time library is provided. Using SPARK Pro at these levels will provide the benefit of increasing confidence in the reliability of the application developed.

For EAL 4 more testing is required than in lower levels. This level has been shown to map to the DO-178B Level A avionics safety standard. Support is provided through GNAT Pro’s Ravenscar and Cert run-time libraries, specifically developed to meet this safety standard and level.

EAL 5 and higher require semi-formal or formal methods to prove correctness. Both the application and run-time library must be written using such methods. For these top levels the GNAT Pro High-Integrity Edition for MILS includes the Zero Foot Print (ZFP) run-time library. The SPARK Pro tool set accompanied by the ZFP run-time library provide the appropriate mix of features and provable correctness for applications needing to meet an EAL of 5 or higher.

Target Platforms

Wind River VxWorks MILS Platform

• VxWorks for MILS