When Software Must Be Safe and Secure
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 specialized 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 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
GNAT Pro High-Security 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-Security includes a full Ada run-time library and development support tools. To meet EAL 4 GNAT Pro High-Security 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 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.
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.
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. 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 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.
Learn about some of the core tools and technologies included with GNAT Pro High-Security:
Wind River VxWorks MILS Platform
Often Security and Safety go hand in hand and GNAT Pro can provide an integrated solution. Learn about GNAT Pro's Specialized tools, services, and certification materials for developing applications that must meet the leading safety-critical standards. Learn More »