GNAT Pro High Security – For developing highly secure systems
GNAT Pro High-Security is designed to support development of applications that can meet the requirements of top Evaluation Assurance Levels (EAL) for stand-alone or within Multiple Independent Levels of Security (MILS) RTOS partitions 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 for lower EAL and several specialised run-time libraries that simplify certification for top EAL. 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.
GNAT Pro High Security includes a specialised 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 specialised run-time libraries to aid in security certification.
EAL Applicability 1-3, 4, 5-7
GNAT Pro High Security includes tools and libraries to support all EALs from 1-7.
- EAL 1-3: Limited testing and proof of correctness are required. For such systems, a full Ada run-time library and development support tools are included.
- EAL 4: Several specialised run-time libraries that have been certified to the DO-178B avionics safety standard are available.
- EAL 5-7: GNAT Pro High Security 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.
The optional SPARK Pro toolset component of GNAT Pro High-Security 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.
GNAT Pro High-Security includes several run-time libraries supporting multiple EALs depending on the application’s security requirements.
- 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.
- 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-7: 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 GNAT Pro High-Security 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.