AdaCore Technologies for cyber security, part 4: Industrial scenario examples
July 18, 2018
Story
This part presents a number of security-related scenarios that may arise in real-world projects.
This is part four in a series of excerpts from a book written by Roderick Chapman and Yannick Moy that cover AdaCore Technologies for Cyber Security. This part presents a number of security-related scenarios that may arise in real-world projects. Each opens with a description of the context and the security issue, and then shows how either Ada or SPARK, in conjunction with the relevant AdaCore tool(s), can contribute. Each scenario is illustrated with one or more examples, drawn from experience with customers and industrial projects.
Read part three here. Note that the original content comes from AdaCore.
Scenario 1: Identifying and repairing security vulnerabilities in existing Ada codebases
In this scenario an existing system written in Ada has to be analyzed for security vulnerabilities, perhaps because of regulatory oversight or commercial/corporate obligations. This is typical of closed systems which become exposed to new threats by connecting them to other systems (ad-hoc networks, Internet, etc.)
The recommended approach comprises two steps:
- Use GNAT Pro and inspect the compiler warnings.
Even when GNAT Pro is not the main compiler on a project, it can still be used as a basic static analysis tool. GNAT Pro flags around 50 different classes of warnings which represent over 130 warning messages. Experience shows that a careful selection of warnings combined with a fix-all-warnings policy can significantly increase the quality of a code base. Warnings that cannot be fixed can be justified with pragma Warnings Off. Warnings can be treated as errors (thus stopping compilation) by enforcing the fix-all-warnings policy with switch -gnatwe.
- Submit the code base to CodePeer for analysis.
CodePeer can exhaustively detect all occurrences of many vulnerabilities from the CWE list: CWE-120 (“Classic Buffer Overflow”), CWE-190 (“Integer Overflow or Wraparound”), CWE-476 (“NULL Pointer Dereference”), CWE-571 (“Expression is Always True”), etc. Users have the choice to opt for an exhaustive report of all potential vulnerabilities (using the -level max switch) or, more commonly, to adjust the level of analysis to their needs, balancing soundness with the effort required to review all messages.
CodePeer can also include GNAT warnings in its messages by using the switch -gnat-warnings. This is particularly relevant for projects that do not use GNAT as the compiler, or else use an older version of GNAT that may lack some of the newer warnings. The GNAT warnings selected are described in the CodePeer User’s Guide.
Example of scenario 1 – GNAT Pro Compiler
GNAT Pro is the compiler for Ada developed by AdaCore, based on the GCC compiler architecture. The front end of GNAT Pro is written in Ada. It is a large software component with 458 units, 370 ksloc, and has been in development since 1992. The front end is compiled with warnings-as-errors (-gnawe) and a large set of warnings enabled (-gnatwa).
Since 2017, AdaCore has been running CodePeer on the GNAT Pro front end, with a fix-all-messages policy. These runs have resulted in the detection of a number of errors in the code, as well as code quality issues (e.g. dead code) which are opportunities for refactoring. CodePeer is run at level 1 for fast execution (less than 10 minutes on a developer machine) while minimizing false alarms. Remaining false alarms are justified with pragma Annotate in the code. CodePeer runs have been integrated in the continuous building environment and nightly regression testing.
Scenario 2: Ada software development practices for increasing security
This case covers a majority of ongoing software developments in Ada, where the strengths of the Ada language are combined with the AdaCore toolset to deliver high-quality software with lower error density than with other languages/toolsets.
Of particular importance, especially for high-integrity development, are the Ada features for encapsulation (packages / private types), reuse (generics), control of representation (data size and layout, addresses), strong typing (type constraints, predicates, invariants), and contract-based programming (preconditions and postconditions). Specific guidance is available for the use of Object-Oriented Programming in Ada [12].
Tools that are relevant in most contexts for high-integrity development are the GNAT Pro compiler for warnings and style checking, the GNATcheck coding standard checker, GNATmetric for metrics computation, GNATstack for memory usage analysis, GNATtest for test harness generation, and CodePeer for static analysis.
Example of scenario 2 – Ada Web Server
The Ada Web Server (AWS) is an Ada implementation of the HTTP/1.1 protocol. It is a library that can be embedded in an application to allow communication with modern web browsers. AWS supports HTTPS (secure HTTP) using SSL. This is based on either OpenSSL or GnuTLS, two open-source SSL implementations.
Because AWS is security sensitive, special care is taken in its code to state explicitly the constraints that should be respected for the program to operate without errors, using Ada contracts on types and subprograms. For example, AWS code deals with time-zone string representation in many places. The code uses a predicate on this type to enforce that this representation remains valid:
subtype Time_Zone_String is String with
Dynamic_Predicate =>
(Time_Zone_String'Length = 0
or else
(Time_Zone_String'Length = 5
and then
Time_Zone_String (Time_Zone_String'First) in '-' | '+'
and then
Time_Zone_String (Time_Zone_String'First + 1) in '0' .. '2'
and then
Time_Zone_String (Time_Zone_String'First + 2) in '0' .. '9'
and then
Time_Zone_String (Time_Zone_String'First + 3) in '0' .. '5'
and then
Time_Zone_String (Time_Zone_String'First + 4) in '0' .. '9'
));
In the same vein AWS uses a Hex_String type which contains only
numbers and letters from 'a' to 'f'.
AWS also uses preconditions and postconditions on many subprograms. For example, when building an object containing a response to be sent back to the Web browser, the postcondition ensures at a minimum that the Build routine does not return an empty object, and that the Status_Code of the response is set according to the corresponding parameter:
function Build (Content_Type : String; UString_Message : Unbounded_String; Status_Code : Messages.Status_Code := …; Cache_Control : Messages.Cache_Option := …; Encoding : Messages.Content_Encoding := …) return Data with Post => not Is_Empty (Build'Result) and then Response.Status_Code (Build'Result) = Status_Code;
As another example, in the Session API, AWS uses a postcondition to ensure that the value of a session is empty if the corresponding key is unknown:
function Get (SID : Id; Key : String) return String with
Post => (not Exist (SID, Key) and then Get'Result'Length = 0)
or else Exist (SID, Key);
The benefit in expressing these constraints as type predicates and subprogram contracts is that they can be checked at run time, instead of informal comments as would be used in other languages. Another benefit is that these explicit contracts replace defensive programming in a way that makes it clear to clients of the API what is expected.
Scenario 3: Secure design through SPARK
This scenario illustrates a high-security system where maximum assurance is required. Such systems often contain few or no COTS components and can be both embedded and feature a “bare metal” implementation style with minimal or no operating system support.
At the high-end, a “bare metal” implementation, the use of SPARK and the Zero FootPrint (ZFP) Ada run-time library offer the ability to account for every byte of object code in the finished product.
For such systems, the recommended approach is to use SPARK in fully constructive mode with Verification-Driven Design (see section 2.4) to set objectives for each subsystem or module. All code should be proven free from run-time errors, and critical modules should be proven to satisfy application-specific security properties.
Example of scenario 3 – the Muen Kernel
Muen [21] is a high-assurance hypervisor for the x86_64 architecture, with the most critical components designed and verified using SPARK. Muen is also a Separation Kernel and supports strict partitioning and security policy enforcement for its clients.
The Muen system, including all the code, is freely available under version 3 of the GNU Public License (GPL).
Examples of scenario 3 – Crypto and Tokeneer
Several projects have used SPARK to develop critical cryptographic components, including cross-domain switches and reference implementations of cryptographic algorithms [19, 22, 23]. Some of these have been evaluated to the highest levels of assurance required by national regulators.
The Tokeneer project [24] was a demonstration of high-integrity development in SPARK, funded by the US National Security Agency (NSA). The Tokeneer code and all documentation have been released under a permissive license and are freely available for study and research.
Scenario 4: Support for mixed criticality systems
This scenario covers systems with mixed assurance requirements, developed using a variety of technologies and programming languages.
The key is a sound security engineering and architectural design that separates critical from non-critical components, and that makes the most critical components as small as possible. The architecture should support a verification argument that top-level security requirements are indeed met.
Various implementation mechanisms can support such an architecture—distinct CPUs, multi-core CPUs, hypervisors and RTOSs can all offer the support required. The software might be several distinct “programs” which might be implemented in SPARK (for the most critical), Ada (for mission-critical components and infrastructure), C (for some low-level functions) and possibly other languages like C++, Java or Python for a user-interface component.
Example of scenario 4
The MULTOS CA [8] formed the root certificate authority and key generation facility for the MULTOS smartcard operating system. The CA facility stored the private signing keys that were used to digitally sign certificates for MULTOS applications, and so were subject to an extraordinary level of physical, procedural, and computer-based security.
The software architecture was similar to that described above. Great care was taken to isolate security-critical functions in a single security kernel component that was constructed and verified using SPARK. In another architectural simplification, the system was designed so that there was no concurrent execution of security-critical functions. The system’s software infrastructure was developed in Ada (using tasking for the non-critical, but naturally concurrent activities), while the GUI was implemented using C++ and the Microsoft Foundation Classes. A small number of C libraries were used, while a small amount of SQL code supported the system’s internal database.
Scenario 5: Introducing Ada in a C project
The introduction of Ada and/or SPARK can be a challenge for some projects, especially those with a large code base in C or some other language. This section deals with C in particular, since it is commonly used for embedded systems development.
In fact, “mixed language” development with Ada, SPARK, C, and assembler is standard practice among AdaCore’s customers. Projects often have libraries or components written in C which have long-standing provenance, so there is little desire (or technical merit) to rewrite them in Ada or SPARK [25].
Ada can be introduced into such an environment for new or modified subsytems, and linked with existing code. Ada has particularly strong support in this area, in terms of both language features and tooling. The Ada language definition devotes an entire annex to the matter of interfacing Ada code with other languages, with special sections for C and C++ among others.
The crucial step is to identify, isolate, and “wrap” C libraries, to provide an Ada interface for invoking them. Where a C library exports a function, for example, an Ada package would contain a corresponding subprogram declaration. Essentially, the idea is to produce a specification of the function in Ada, but to keep the implementation in the original language. The Ada specification can take advantage of Ada’s strong types, parameter passing modes, and contracts to their full extent. This may involve careful study of the C library’s documentation and implementation to understand fully what it does (and doesn’t) promise to its clients. These properties and assumptions can be documented as contracts in the Ada code, but these are formal in that they can be used for both dynamic and static checking.
Once C libraries are “wrapped” in this fashion, they can be called from new Ada or SPARK code as expected. (It also works in the other direction: Ada and SPARK can be called from C.) The contracts on the library binding will be verified, either dynamically at run time, statically using CodePeer or SPARK Pro, or both.
AdaCore’s tools support this style of development well. As a first-class member of the GCC family, GNAT Pro can compile Ada and C “out of the box”, following all of the guidance in the interfacing annex of the Ada standard. Additionally, GNAT Pro supplies a “binding generator” that can automate the process of turning a C “.h” file into an equivalent Ada package specification. Many of AdaCore’s other tools (e.g. GPS, GDB, and GNATcoverage) are also “multi-lingual” and work seamlessly with mixed-language code.
Example of scenario 5: Industrial mixed-language system
This project is a large, critical system using a combination of Ada, SPARK, and C [26].
While the critical functions are implemented in SPARK, the user-interface is constructed using the X11/Motif framework and libraries which express their API in C. Therefore, a “binding layer” was constructed to connect the SPARK code, via C, to the underlying libraries. The C layer is subject to static analysis using the MISRA guidelines [27] and a MISRA checking tool.
Some effort was spent to document the assumptions that the SPARK and C code make about each other’s behavior, and how these assumptions can be expressed as contracts and verified in practice. Further details of this project appear in [26], which is available from the authors.
