Introduction

The FACE® approach (Future Airborne Capability Environment®) is a joint government-industry initiative to reduce system life cycle costs for airborne software through the reuse of portable source code components. Sponsored by the US Department of Defense and currently open to the “Five Eyes” countries (Australia, Canada, New Zealand, UK and the US) the FACE approach is administered by The Open Group’s FACE Consortium and is realized through several technologies based on open standards:

• a data modeling methodology that ensures a consistent interpretation of data (e.g., a coordinate system) shared by independently developed components,

• a design architecture based on sound software engineering principles and comprising tiered “segments” that separate platform-specific and platform-independent elements (see Figure 1 for a simplified version of the FACE architecture), and

• standard interfaces that are used or supplied by the software in the various segments.

Airborne application code will generally reside in the Portable Components Segment (PCS). It will communicate with other PCS components through interfaces defined in the Transport Services Segment (TSS). The portability of PCS source code is achieved through the use of standard interfaces: standard programming language features (C, C++, Ada 95, Ada 2012, and Java) implemented by the compiler, and standard APIs (POSIX and ARINC-653) supplied by the Operating System Segment (OSS).

Since airborne systems contain software components at varying levels of safety criticality, the FACE Technical Standard defines subsets of these programming languages and APIs, respectively referred to as capability sets and profiles. From most general to most restrictive these are:

• General Purpose

• Safety Extended

• Safety Base

• Security

There are separate profiles for Safety Base and Security, but a single capability set encompasses both. As an example of the restrictions, the POSIX function time() is allowed in the General Purpose, Safety Extended, and Safety Base profiles but prohibited in the Security profiles. As another example, for both Ada 95 and Ada 2012 the allowed exception handling features differ across the various capability sets. The General Purpose capability set supports the full exception model, Safety Extended prohibits the functions whose effect is implementation defined, and Safety Base / Security only allows last-chance handlers.

The interpretation of the profiles and capability sets depends on the segment. OSS software needs to provide, at minimum, the features and APIs permitted by the profile and capability set that it targets. On the other hand, PCS software can only use the features permitted by the targeted capability set and can only have external references to APIs permitted by the targeted profile and capability set.

Figure 1 shows a simplified version of the FACE software architecture. Software that is written to conform to the FACE requirements for a specific profile and capability set is known as a Unit of Conformance, or UoC. The Programming Language Run-Time is a compiler-dependent library of functions called from the object code.

Demonstrating that a UoC meets the requirements for its targeted profile and capability set entails verifying that the software successfully passes a Conformance Test Suite (CTS). As part of the official process, the UoC software supplier submits specified evidence to a representative of a FACE Verification Authority (an organization certified by the FACE Consortium). However, neither the current CTS (Version 3.2) nor the previous versions support UoCs written in Ada. To address this gap, the Operating System Subcommittee of the FACE Consortium’s Technical Working Group established the FACE Ada Conformance Tiger Team, led by AdaCore’s Ben Brosgol and Dudrey Smith. The solution developed by the Tiger Team has been accepted by the FACE Consortium as an Approved Correction to the CTS. This blog summarizes the approach, which applies to UoCs from all FACE segments except for the Operating System Segment (OSS). The OSS has special requirements in light of its intrinsic platform dependence.

FACE Conformance and the CTS

For standards related to safety or security, software certification includes demonstrating that the source code meets specified assurance requirements. As an example, the DO-178C standard for commercial airborne software defines verification processes based on review (manual source code inspection), analysis (evidence provided by static analysis tools), and requirements-based functional testing. The source code is one of the many artifacts made available to the certification authority’s agent (the DER, or Designated Engineering Representative) overseeing the certification process.

Conformance verification for FACE UoCs takes a different path and does not require the FACE Verification Authority to have access to the source code. There are several reasons for this approach:

• The software may be proprietary or classified, with restrictions that preclude exposing the source code.

• The FACE Technical Standard is a portability standard, and FACE conformance verification does not test for functional correctness. Although safety considerations are realized in the definition of the various profiles and capability sets, FACE conformance does not guarantee satisfaction of specific assurance properties. In contrast with safety properties, portability can be verified without making source code available.

The CTS uses link-time checks to verify conformance. It’s based on a simple principle: if you want to check whether UoC object code contains references to functions that are not permitted by the UoC’s targeted profile and capability set, then compile the source code against, and try to link the object code with, stubbed libraries for the permitted APIs. Ideally, these stubbed libraries (i.e., functions with dummy / empty implementations) would contain only the permitted functions, but in practice this is not possible. Thus the UoC object code is linked against stubbed libraries that contain at least the permitted APIs but which may also contain other functions.

If the link of the UoC against these stubbed libraries fails, then the unresolved references indicate calls on prohibited functions, and the UoC is deemed non-conformant. However, the inverse is not necessarily true: the link may succeed even when the UoC is non-conformant. This can happen for two reasons:

• The source code violates a capability set restriction on a syntactic feature that does not require run-time support. API subsetting does not help; uses of such restricted features are not detected by link-time tests.

• The source code calls a function from the toolchain’s compiler-specific run-time library. This is non-conformant, but such calls are permitted in the object code and pass the link-time test.

In the first case the UoC supplier needs to provide evidence of conformance based on source code inspection.

In the second case the UoC supplier will need to provide either source code inspection evidence or its equivalent (e.g. using a compiler option or directive to exclude the compiler-specific run-time). For Ada 2012, pragma Restrictions(No_Implementation_Units) will detect this violation at compile time. Alternatively, inspection evidence reflecting the separate compilation dependencies can confirm the absence of violations:

• All “with”ed units must be units either defined within the UoC or else allowed by the targeted capability set

• For each child unit defined within the UoC, its parent must also be defined in the UoC (thus the UoC is not allowed to define children of packages in the predefined environment)

In either case the source code itself does not need to be revealed.

More specifically, the stubbed libraries used by the CTS fall into several categories (see Figure 2):

• Gold Standard Library (GSL)

  • FACE specific interfaces

These include TSS functions for inter-UoC communication as well as functions derived from the data model.

• Profile interfaces

These are the POSIX or ARINC-653 functions allowed by the targeted profile

• Standard library subset

These are the functions from the standard language library allowed by the targeted capability set.

• Programming Language Run-Time

  • Standard library subset

This is a possibly extended version of the GSL standard language subset, depending on the toolchain.

• Compiler-Specific Run -Time

The UoC object code may contain API calls on functions from the compiler toolchain’s run-time library, for example for dynamic language features or specialized hardware features. The compiler-specific run-time subset is toolchain dependent and supports all features permitted by the target capability set.

FACE Conformance and Ada

The approach just described works well for C and C++, since run-time services for these languages are realized through standard APIs, and the compiler-specific run-time is relatively small. In contrast, Ada’s dynamic features (e.g., concurrency, memory management, exception handling) are realized in source code through standard language syntax that is compiled into calls on functions from the compiler-specific run-time library. Since this library may also support features that are not permitted, the UoC software supplier and the Verification Authority agent need to know, for any given restriction, whether the toolchain with its stubbed libraries detects the violation. The results may vary across toolchains; a violation detected by one toolchain might not be detected by another; in such cases the user of the second toolchain will need to supply inspection evidence.

One question for UoC software suppliers and Verification Authority agents is how to know, for any given requirement/restriction, whether a violation is detected by a link-time test or instead will require inspection evidence. The solution:

• a set of test cases, known as the Toolchain Capability Assessment Test Suite (TCATS) each of which is a legal program in full Ada but violates a capability set requirement, and

• a driver program tailorable to the specific toolchain, which attempts to compile and link each test program (using the same stubbed libraries as the CTS) and reports its result.

A second issue relates to the logistics of running the CTS. It currently does not support the detection of Ada capability set violations, and in any event the procedures for augmenting the existing CTS so that it properly exercises the Ada toolchain is dependent on the specifics of that toolchain. Thus a toolchain support package is required, provided by the toolchain vendor.

TCATS Suite

The TCATS tests are derived directly from the FACE Technical Standard and cover all of the capability set requirements, for each capability set and for both Ada 95 and Ada 2012. If the driver program successfully compiles and links a test program, then the toolchain did not detect the violation that the test program exercised. The UoC supplier will then need to verify the requirement by inspection. If the driver program failed to build the test program, then the toolchain successfully detected the violation, and the CTS’s link test can verify the requirement. (In fact, in almost all cases the violation would be detected by attempting to compile the program against the CTS’s stubbed libraries.) The output of the driver program is thus an indication, for each test case, whether the corresponding requirement needs to be verified by inspection or by test.

As an example, here is one of the test cases for the requirement that asynchronous transfer of control is excluded:

The name R02_01_SB_SE_GP indicates that the code is a test for requirement 2, that it is the 1st test case for this requirement, and that it applies to the Safety Base & Security (SB), Safety Extended (SE), and General Purpose (GP) capability sets. If it applied only to Ada 2012, it would have a “_12” suffix; the absence of such a suffix means that it applies to both Ada 95 and Ada 2012.

To make it easier to manage the logistics, the TCATS tests are complemented by a spreadsheet that maps FACE Technical Standard requirements to TCATS tests. The columns for each spreadsheet row display various properties of the test case:

• A unique ID for the requirement

• A unique ID for the test case

• A summary of the restriction being exercised by the test case

• The verification method to be used: test or inspection (left blank)

• The language version: Ada 95, Ada 2012, or both

• The capability set(s) that include the requirement

• A reference to the relevant section(s) in the Ada Language Reference Manual (LRM)

• The associated Conformance Verification Matrix (CVM) row(s)

• A summary of the requirement being tested

• If applicable, a standard pragma Restrictions directive that captures the restriction (this can aid the software supplier during development by detecting violations at compile time)

Here is an example of the worksheet rows for the restriction on Asynchronous Transfer of Control (for ease of display, the rows are split into two tables):

The ‘X’s in the Language Version and Capability Set columns show that the requirement applies to both Ada 95 and Ada 2012 and to all capability sets.

After running the TCATS driver program as described above, the FACE UoC Software Supplier can fill in the Verification Method column based on the results: either TEST if the violation was detected, or INSPECT otherwise. The FACE Verification Authority will do likewise, ensuring a common understanding of which requirements need to be tested and those that need to be verified by inspection.

CTS Toolchain Support Package

The toolchain support package comprises documentation as well as any additional items that are needed to run the CTS with a selected Ada toolchain.

The support package provided for the GNAT Ada toolchain consists of the following:

• CTS User Guide Supplement for Ada

This manual explains how to install the Ada-specific dependencies (in particular, the version of GNAT that will be used with the CTS for host-based conformance verification) and shows how to adapt the CTS User Guide to handle Ada. These adaptations include generating an Ada GSL and overriding the existing CTS Ada libraries.

• Library generation script

This script (a Python program driven by a Makefile) derives the Programming Language Run-Time (PLRT) for a given capability set by stripping symbols (for unwanted APIs) from GNAT GPL 2017’s full Ada run-time library. The user – i.e., the person running the CTS – invokes this script to create the relevant stubbed PLRT.

• Auxiliary files

The GNAT support package also includes a toolchain configuration file, the source code for configuration pragmas that are used in generating the stubbed libraries, and sample projects that can check for proper installation and setup.

The specific contents of the toolchain support package will depend on the toolchain vendor / technology, and the artifacts for the GNAT toolchain can serve as a model.

Ada Toolchain for Host-Based Conformance Verification

The CTS supports both host-based and target-based verification processes. Specific toolchains and Operating Systems have been authorized for host-based verification; a main requirement is for the toolchain to provide appropriate non-proprietary licensing. For Ada, a further desired property is that the toolchain support both Ada 95 and Ada 2012; otherwise, it would be necessary to have two separate Ada toolchains.

The GNAT GPL 2017 toolchain satisfies these criteria. It supports both Ada 95 and Ada 2012, is openly available for download, has appropriate open-source licensing (GNU GPL 3 with the GCC Runtime Library Exception), and runs on both Windows 10 and Linux.

Conclusions

The approach described in this blog extends the current FACE Conformance Test Suite (CTS) with a practical means to verify FACE non-OSS UoCs written in Ada. It takes into account that different toolchains will have different compiler-specific run-time libraries to support the language’s dynamic features. It is a natural extension of the process used for C and C++, using link-time tests as the basis for checking conformance. Just as with the other languages, there is no need for the FACE Software Supplier to expose the UoC Ada source code. Proprietary and/or classified information in the source code is still protected.

Although the specifics of the approach are unique to Ada, the use of a test suite such as the TCATS applies equally to the other languages supported by the FACE Technical Standard. An analog of the Ada TCATS can be prepared to determine which requirements need to be verified by inspection; this can help improve the FACE conformance procedures in general.

Almost all large-scale Ada applications include some C code. Although the CTS process supports verification of single-language UoCs, mixed-language situations are currently beyond its scope. Development of a solution is nearing completion, with work in progress on formulating practical procedures for verifying UoCs that combine Ada and C.

Future work includes incorporating Ada support directly in the CTS (versus requiring a superseding supplement), running the TCATS as part of the CTS, and accommodating automated production of inspection evidence as exemplified by the GNATcheck tool in AdaCore’s GNAT Static Analysis Suite.

Ada has a long and successful history of developing defense systems in general and airborne systems in particular, embodying sound software engineering principles that reduce the effort to produce portable, reliable, safe, and secure software. The availability of a practical approach to FACE conformance verification for non-OSS Ada UoCs fills a longstanding gap and will reduce the efforts necessary by both the supplier and verification authorities to demonstrate UoC FACE conformance. In brief, suppliers of Ada airborne software will have a well-defined path to FACE conformance, and providers of FACE conformant software will have an additional language option. Both results will be welcome developments for the defense community.

References

B. Brosgol. M. Frank, D. Binkley, and D. Smith; Verifying FACE Conformance for Non-OSS Ada UoCs; The Open Group FACE and SOSA Consortia 2024 Technical Interchange Meeting (TIM)

The Open Group; FACE Technical Standard, Edition 3.2 ; August 2023

The Open.Group; FACE Conformance Test Suite(s)

Acknowledgments

The author would like to thank his AdaCore colleagues Dudrey Smith, Michael Frank, and Dana Binkley, and also the other members of the FACE Ada Conformance Tiger Team, for their contributions to the work described here. A special note of thanks to the late Chris Edwards, formerly Chair of the FACE Consortium’s Technical Working Group, for posing the key questions that led to this work.