Verifying FACE conformance for Ada software

Story

May 16, 2024

Benjamin Brosgol

AdaCore

Photo courtesy U.S. Department of Defense/U.S. Air Force.

The Future Airborne Capability Environment (FACE) approach is a government/industry initiative, managed by the FACE Consortium under the auspices of The Open Group. Its goal is to reduce software development/deployment costs through source code portability and reuse and thereby avoid vendor lock-in. A key element of the FACE approach is an official process and test suite for verifying that software conforms to the requirements specified in the FACE Technical Standard. However, this process currently does not easily accommodate Ada, a language with a long history of successful usage in safety-critical airborne systems, both military and commercial. There is a solution to this hurdle, however: a practical approach to FACE conformance verification for Ada code (both Ada 95 and Ada 2012), in particular for software that is not part of the underlying operating system.

First, a bit of background, or “FACE Conformance Verification 101.” The Future Airborne Capability Environment (FACE) Technical Approach is based on several elements:

a segmented software architecture that separates portable from platform-specific components
an expressive and language-agnostic data modeling technology that ensures a consistent interpretation for data communicated across components
tiered “profiles” and “capability sets” that impose safety-oriented restrictions on standard software interfaces and language features

Although it is focused on portability and does not address functionality or assurance requirements, the FACE approach accounts for the fact that in practice, an airborne system comprises components at varying levels of safety sensitivity. The FACE Technical Standard thus defines subsets of standard application program interfaces (APIs) – in particular POSIX and ARINC-653 – at several levels (called profiles). In increasing order of criticality, from most permissive to most restrictive, these are General Purpose, Safety Extended, Safety Base, and Security. Analogously, the FACE Technical Standard defines subsets of standard language features for C, C++, Ada 95, Ada 2012, and Java (“capability sets”): General Purpose, Safety Extended, and Safety Base/Security. As an example, the predefined generic package for unbounded strings can be used in the General Purpose capability set for both Ada 95 and Ada 2012, but because of its dependence on dynamic memory management it is excluded from the Safety Extended and Safety Base/Security sets.

To verify that a candidate software component – or in FACE terminology a Unit of Conformance (UoC) – meets the requirements defined in the FACE Technical Standard, the FACE Consortium has established a rigorous process that relies heavily on a Conformance Test Suite (CTS). The specifics depend on whether the UoC is part of the underlying operating system (OS), as the OS implementation is necessarily platform-dependent and does not have the portability requirements of application code. Going forward, we focus on portable components, with the term “UoC” referring to software that is not part of the OS.

Because the UoC might have proprietary or classified content, an underlying principle for FACE conformance is that the UoC supplier should not be required to expose the source code. This principle constrains the conformance procedures and makes it unlike other software assurance standards, such as DO-178C. Indeed, the key property checked by the CTS is that there are no uses of language features or external interfaces outside of the ones permitted by the capability set and profile targeted by the UoC. This property can largely be verified by link-time tests. In brief:

The UoC supplier compiles the source code with a toolchain (either a native or cross development environment). The header files (C and C++) or compilation unit specifications (Ada) should be the same as those used for the Gold Standard Library (see Figure 1).
The CTS generates the permitted run-time libraries for the toolchain’s target platform, based on the selected profile and capability set. These are stubbed libraries (interfaces only, null code bodies) comprising the following (Figure 1):

[Figure 1 ǀ Shown: Stubbed run-time libraries used by the FACE Conformance Test Suite.]

• FACE interfaces and data model

■ APIs for FACE services such as IO and inter-UoC data communication that are permitted by the targeted profile, together with APIs generated for the UoC’s data model

• POSIX or ARINC-653 library

■ The APIs from these standards that are permitted for the targeted profile

• Standard run-time subset

■ The APIs defined by the language standard that are permitted by the targeted capability set

• Compiler-specific run-time (CSRT) support

■ APIs that are invoked from the compiled code and which implement run-time functionality that is expressed in standard language syntax (e.g., threading, memory management, and exception handling)

The CTS attempts to link the UoC object code against these stubbed libraries.

The CTS generates a report with one of three possible outcomes:

Success. The submitted UoC object code links successfully against the above libraries and does not use features that are permitted but have usage restrictions. The UoC is considered to have met all FACE requirements that can be tested by the CTS. However, some FACE requirements are feature restrictions based on language syntax rather than run-time library support. If the UoC uses such a feature, it may still link successfully against the CTS libraries but is not necessarily FACE conformant. For such requirements the UoC supplier needs to demonstrate, by providing the results of source-code inspection, that the UoC meets the restriction(s) that are not detected by the CTS.
Inspection required. The submitted UoC object code links successfully against the above libraries and uses a feature that is permitted but has usage restrictions. In this case the UoC supplier needs to substantiate the usage through inspection (of design or code).
Failure. A failure is reported if the UoC object code fails to link. If there are link errors with unresolved symbols, then the UoC supplier will need to either make appropriate corrections for a subsequent conformance verification attempt, or else provide the relevant additional libraries to resolve the symbols and explain why these libraries should be permitted. (As an example of the latter, if the UoC contains code in both C and Ada that meet the FACE requirements, then the object code in either of these languages will fail to link against the libraries supplied for the other language. The UoC supplier can provide the needed libraries and must substantiate their inclusion.)

For a formal conformance verification, the UoC supplier needs to demonstrate a successful CTS execution and provide the necessary source inspection evidence to an agent from an organization approved by the FACE Consortium as an official Verification Authority.

The challenge for Ada

For C, and to a large extent for C++ (Java introduces some unique issues and is outside the scope of this discussion), the CTS process works effectively: the compiler-specific run-time subset is fairly minimal, for example including numeric routines implemented in software rather than hardware. But for Ada, this library is much more extensive. An Ada program expresses run-time functionality such as threading not by invoking a standard API (e.g., pthread_create) but rather by using standard programming language syntax that is compiled into calls on subprograms in the CSRT.

Furthermore, it is unrealistic to expect that the features supported by a CSRT will exactly match the features allowed in the targeted capability set. FACE conformance requires the library to supply at least the permitted functionality but permits it to provide more. The challenge for the CTS is to account for several factors:

The CSRT for a given Ada toolchain will support some features that are prohibited by the targeted capability set (this is also true for C and C++, since some capability set restrictions are unrelated to run-time APIs)
To show the absence of these features from the UoC, source inspection evidence is required
The specific features subject to inspection will vary across Ada toolchains

The CTS is flexible enough to be used for verifying FACE conformance for Ada UoCs; however, the process is not clearly defined. Ad hoc procedures need to be used to generate the relevant stubbed libraries, to demonstrate that these libraries are acceptable, and to determine what must be verified by inspection. The overall process has proved to be rather clumsy in practice.

Working within the Operating System Subcommittee of the FACE Technical Working Group, an Ada Conformance Tiger Team led by AdaCore has prepared a practical solution. The proposed approach uses the current CTS as supplemented by two main elements:

Toolchain assessment package. A test suite comprising Ada code that violates the FACE capability set requirements and a script that attempts to invoke an Ada toolchain to compile and link each test against applicable run-time libraries.
Toolchain support package. Documentation and other artifacts needed for adapting the CTS so that it generates the needed run-time libraries and performs the link-time testing of the submitted UoC object code

Toolchain assessment package

Toolchain Capability Assessment Test Suite (TCATS): This is a test suite derived from the FACE capability set requirements. In general, a given requirement specifies restrictions on one or more language features and thus yields multiple tests. Each test is a legitimate program in the full Ada language but exercises a feature that violates the requirement.

Comprising well over 100 tests, the TCATS covers all the capability sets and both Ada 95 and Ada 2012. An example illustrating a FACE requirement and one of the resulting TCATS tests is shown in Figure 2. The tests themselves are vendor-neutral, but the results of compiling and linking the tests will vary based on the toolchain and its CSRT.

[Figure 2 ǀ FACE Technical Standard requirement and TCATS test is shown.]

TCATS results worksheet (template): This Excel file is a spreadsheet that, when completed, will show how a given toolchain processes the TCATS. Each TCATS test is represented by a row in the spreadsheet. For each row, prefilled columns specify a unique ID for the test, the wording of the requirement from which the test was derived, and the capability set(s) and Ada language version(s) for which the test is to be used. An additional column – the result of submitting the test to the toolchain – is blank.

Toolchain invocation script: This script is a standard Ada program (both Ada 95- and Ada 2012-compatible) that takes as input a listing of all the TCATS test files and produces as output a text file documenting the toolchain’s ability to detect the restriction violations embodied in the tests. The script invokes an Ada toolchain on each test and checks whether the test was successfully compiled and linked. If a test fails to compile, or if it compiles but fails to link, then the script identifies the associated restriction as being verified by the CTS; otherwise, the restriction is noted as requiring verification by inspection. These results are captured in the output file.

The script invokes a nonproprietary Ada toolchain on one of the authorized host conformance verification platforms, namely the GNAT GPL 2017 edition on Windows 10. This version of the GNAT technology has appropriate licensing for use with the CTS, and it supports both Ada 95 and Ada 2012. The script is readily tailorable to other Ada toolchains and other native or cross platforms as needed.

The UoC supplier and the Verification Authority agent can use the script output to complete the toolchain capability worksheet. During official conformance verification, if the UoC successfully links against the CTS libraries, the Verification Authority can use this worksheet to determine which requirements still need to be verified by inspection.

Detecting source code invocations of compiler-specific run-time API

A UoC whose source code invokes functions from the CSRT is not FACE conformant, since the code would clearly be nonportable. However, there is no way for the CTS to detect violations, since CSRT functions can be invoked from a conformant UoC’s object code. Though nonconformant, a UoC whose source code invokes a CSRT function will thus link successfully. This issue is not unique to Ada; it applies to all the FACE supported languages. Detection necessarily requires source code inspection. For Ada, the UoC supplier must demonstrate two properties:

The only units referenced in the UoC’s “with” clauses are either other compilation units in the UoC, units from the standard run-time library permitted by the targeted capability set, or else units from the POSIX or ARINC-653 library permitted by the targeted profile.
The only units allowed as parents of child UoC units are other units in the UoC. The UoC is thus not allowed to define child units of CSRT packages, nor is it allowed to define child units of predefined Ada packages. (In the latter case, such child units could reference private declarations and therefore be non-portable).

The UoC software supplier thus needs to provide the following evidence:

The list of all top-level compilation units defined by the UoC
The list of all child units defined by the UoC
The list of all compilation units “with”ed by units in the UoC
Documentation showing that all the units in (3) are in (1), (2), or the Gold Standard Library for the targeted profile and capability set
Documentation showing that the root unit of each unit in (2) is a (package or generic package) unit in (1)

Toolchain support package

Given the constraint of no changes to the CTS software, the provider of the toolchain to be used for Ada conformance verification needs to supply the relevant supplementary artifacts (documentation, scripts, installation instructions, configuration files) to enable the UoC provider and the Verification Authority to conduct a conformance verification with the existing CTS. More specifically, the package provided for an Ada toolchain needs to include a CTS users guide supplement with detailed instructions on setting up the toolchain and running it from the CTS:

Installing and configuring the Ada toolchain
Generating the Ada Gold Standard Library and the toolchain’s Programming Language Run-Time, based on the targeted capability set and profile

Using this information, the UoC supplier and the Verification Authority can then run the CTS on an Ada UoC: this will entail linking the UoC object code against the Programming Language Run-Time and Gold Standard Library for the targeted capability set/profile and producing a conformance report, just as is done for other languages. The main difference with Ada is the use of the TCATS results worksheet to establish the requirements that need to be verified by inspection.

The larger picture

It is important for a developer to be able to check incrementally (as part of continuous integration/DevOps) that the UoC meets the restrictions imposed by the targeted profile and capability set. Ada offers two solutions:

Pragma Restrictions, a standard pragma in Ada 95 and Ada 2012, can be supplied with relevant arguments at each compilation to ensure that prohibited features are not used (i.e., the compilation unit will be rejected if it uses such a feature). For example, pragma Restrictions(No_Dependence => Ada.Strings.Unbounded) will detect uses of unbounded strings. As an aid to developers, if a FACE capability set restriction violation can be detected by a standard pragma Restrictions argument, the TCATS Results Worksheet template has an entry associating that argument with the relevant test(s).
A static analysis tool can be used to detect violations of FACE requirements, including those that are syntactic in nature and are not expressible via arguments to pragma Restrictions. An example of such a tool is GNATcheck, which is part of AdaCore’s GNAT Static Analysis Suite.

The approach to FACE conformance for Ada has exposed several issues that are relevant to the conformance procedures for other languages. One is the use of a test suite (TCATS) to determine whether a violation is detected by the toolchain and its CSRT. It is important for the UoC supplier and the Verification Authority to know with confidence which requirements will entail source code inspection, and a test suite such as the TCATS can serve this function. A second issue is the need to detect source code references to the CSRT. This is not testable by the CTS, and rules are required for C, C++, and Java with respect to the inspection evidence that the UoC supplier needs to provide.

Going forward

A well-defined and practical conformance-verification process for Ada is important for the successful adoption of the FACE approach within the defense community, and the solution described here will fill a current gap. It is incremental in nature, working with the existing CTS and using link-time tests as its basis. Although evolutionary, the Ada conformance approach is also innovative and has introduced several elements (a toolchain assessment package and a toolchain support package) that formalize aspects absent from or implicit in the procedures for other languages. Artifacts such as the TCATS and the rules for detecting source code references to compiler-specific APIs are relevant for other languages and may help guide future enhancements to the FACE conformance verification process.

As of early 2024, the Ada approach described here is under consideration within the FACE Consortium, and artifacts comprising sample toolchain assessment and toolchain support packages have been prepared and submitted. Although the final details may vary, a FACE conformance verification solution for Ada based on these packages is expected to be approved in the near future. Further enhancements include procedures for verifying mixed-language UoCs (in particular, when both Ada and C are used) and incorporating the TCATS as part of CTS execution.

Dr. Benjamin Brosgol is a senior member of the technical staff at AdaCore. He has been involved with programming language design and implementation throughout his career, concentrating on languages and technologies for high-integrity systems with a focus on Ada and safety certification (DO-178B/C). Dr. Brosgol is an active member of The Open Group FACE Consortium’s Technical Working Group, and in particular he has been involved with the development of the IDL-to-Ada mapping.

AdaCore • https://www.adacore.com/