Deterministic and Modular Architecture for Embedded Vehicle Systems

February 1, 2024

The next generation of Army ground vehicle systems aim to provide the warfighter with advanced capabilities while ensuring cyber resiliency. One key technology, Ethernet, has enabled the modernization of military ground vehicles by providing a broad range of beneficial features. The scalability and high bandwidth of an Ethernet based system provides the ability to process large volumes of sensor data with low latency, however its inherent lack of determinism represents a significant disadvantage. A deterministic network requires that communication assurance is provided through bounded message latency, and this is required for many ground vehicle weapon and crew stations functions.

Traditional Ethernet based networks are unable to satisfy the strict safety and functional requirements for Army vehicle systems due to this lack of determinism. Modular Open System Approach (MOSA) initiatives such as the Ground Combat System Common Infrastructure Architecture (GCIA) seek to leverage open-standards such as Time Sensitive Networking (TSN) to achieve real-time, deterministic communication over Ethernet. TSN provides enhancements to regular Ethernet which enable logical segmentation of deterministic and traditional best-effort network traffic while simultaneously be transmitted on the same physical media.

This research presents a reference architecture which incorporates key elements from GCIA, including TSN, and complements them with embedded virtualization technologies to enhance the safety and security of the system. The seL4 microkernel is used to deploy virtualized guests and containers on a target representative of an embedded platform for ground vehicle electronics, the ARMv8. By utilizing seL4 and virtualized guests, a system designer can now combine the isolation provided by hypervisors with the logical segmentation provided by TSN to create a partitioned architecture that increases system assurance. Aspects of this architectural approach and technology have already been adapted across multiple programs within the U.S. Army DEVCOM Ground Vehicle Systems Center (DEVCOM-GVSC).

Background

In the last decade a key enabler for next generation automotive and industrial system hardware/software designs has been virtualization. Modern embedded systems that utilize the ARM, x86, or RISCV architectures are now equipped with virtual extensions. These extensions were the response to market pressures to minimize size, weight, power, and cost (SWaP-C).

Software designers are now able to architect a system capable of enforcing isolation of disparate compute domains while executing on the same hardware. They’re also able to provide a system capable of rapidly scaling and updating with an existing DevSecOps pipeline and adapt to new industry best practices by deploying improved capabilities (i.e. TSN).

One response to these demands in recent years is hypervisor-based technology, however traditional enterprise hypervisors do not provide the assurance or real-time performance needed to support mixed criticality applications. The seL4 microkernel can serve as an embedded hypervisor that can support the deployment of high assurance software through its unique and comprehensive formal verification.

Formal proofs of correctness make seL4 a strong candidate for building safety-critical and secure systems. Figure 1 illustrates the seL4 proof chain. The core of seL4’s verification is the functional correctness proof, which claims that the C implementation is free of implementation defects. The formal specification of the kernel’s functionality is expressed in a mathematical language called higher order logic (HOL). The HOL specification in this case is represented by the abstract model in Figure 1.

Figure 1. An architecture showing a seL4 Proof Chain.

The C implementation is then a refinement of the abstract model, meaning that the possible behaviors of the C code are a subset of those allowed by the abstract model. Kernel behavior is expressed by the abstract specification, thus preventing the kernel from behaving in ways that are not allowed by the specification. A kernel that is formally verified, such as seL4, can then shield itself from attacks such as stack smashing, nullpointer dereference, and any code injection or control flow-hijacking.

As a part of the formally verified proof, seL4 also provides a way to additionally verify the executable binary produced by the compiler. Verifying the executable binary is an additional security-critical step to prevent malicious compilers from performing such actions such as building a Trojan that opens a back door to the OS. Specifically, the binary is proved to be a correct translation of the proved correct C code.

The proof chain illustrated in Figure 2 is an automatic process that happens in multiple stages. A formal model of the processor’s Instruction Set Architecture (ISA) formalizes the binary in the theorem prover. The formalized ISA feeds the disassembler, written in the HOL4 theorem prover, to translate the low-level representation into a higher-level representation in a graph language that represents control flow. The formalized C program is then translated into the same graph language which allows for comparison of two programs to assess for equivalent representation.

Figure 2. Translation validation proof chain.

One of the goals of this project was to provide documented and reusable software modules that can be ported to various hardware platforms. Various hardware platforms can take the form of a different architecture alltogether (x86, ARM, RISCV, etc.) or it can mean a different platform within the same family of architecture. For example, this effort utilized a total of four development kits to develop the software capabilities discussed in this research. The four development kits used were all based on the Zynq architecture.

Security Properties and Hypervisor Design

Figure 1 illustrates the proofs between the abstract specification and the high-level security properties: confidentiality, integrity, and availability. These properties are subsets of the abstract specification and build in security to the kernel. seL4 provides the ability for a system architect to implement a hypervisor and virtual machine monitors (VMMs) capable of deploying isolated virtual machines (VMs) as notionally illustrated in Figure 3.

Figure 3. The seL4 Hypervisor Mode is outlined here.

The design paradigm depicted in Figure 3 demonstrates a high-level overview of the type of hardware and software configuration designed to meet SWAP-C requirements. At the lowest level of this architecture is the target hardware. In this case the target hardware used for this effort was the ARMv8, however, it can be applied to x86 and RISC-V as well. Software abstraction is applied to achieve a Type 1 hypervisor model. This type of software abstraction enables logical partitioning of compute domains in the form of guest VMs.

Army Use Cases and Objectives

The current state of combat ground vehicle design is undergoing a paradigm shift. Capabilities in the form of sensors, processors, and effectors are now designed to share hardware and compute resources all while maintaining a continuous update/upgrade cycle. Figure 4 illustrates major elements of the GCIA including the relevant network, I/O adapter, crewstation, and common compute components.

The scope of effort in this research enables GCIA, as the SmartIO platform to be used as a Crewstation, Common Compute or I/O Adapter and is TSN-enabled. SmartIO converts discrete I/O signals to TSN messages to be distributed to multiple end nodes. The end nodes in this case include both the virtualized guests executing in disparate compute domains — example given in Figure 3 — and other TSN end stations connected to the TSN bridge.

The military ground vehicle use-cases and scenarios where this type of modern, partitioned, and deterministic architecture is applicable are numerous and support the kinds of logical segmentation identified as a key objective in the DoD’s Zero Trust Strategy that was released in November 2022. Traditionally, military ground vehicle control applications and functions are implemented with technologies such as CAN, MIL-STD-1553, RS-422, and/or point-to-point discrete signals. These interfaces are all prime candidates to be integrated with, and eventually replaced with, this emerging architecture.

A ground vehicle system is entirely made up of complex subsystems. The reference architecture developed in this effort utilized a combination of virtualized I/O interfaces and TSN to enable the common compute i.e., SmartIO, to process, transmit, and receive sensor data distributed throughout the vehicle. Distributed processing and I/O in this context mean that the system must have the ability to route hardware peripheral data, such as CAN, throughout the entire system. Another benefit of conforming I/O with virtual interfaces is the reusability and portability of that software across different computing architectures (i.e. x86, RISC-V, etc.).

Virtualized conformant I/O also enables security enhancements for a more hardened posture. seL4 provides great access control of hardware components within VM(s) to prevent any undesired access from one subsystem to another. Finally, virtualized conformant I/O provides a lower attack surface by virtue of SWAP-C requirements. With one common compute platform the lower physical footprint results in a smaller attack surface for an Intrusion Detection System (IDS) to monitor.

Future Improvements

Figure 5. The UEI SmartIO platform, which is based on the AMD Zynq architecture was the target platform for this research effort.

TSN benchmarking indicated that there is a need to investigate how to obtain performance gains within the seL4 microkernel. Naturally, due to virtualization, there is an expectation of some performance degradation with respect to TSN benchmarking; however, the results indicate that beyond the effects of virtualization there are performance degradations because of the seL4 kernel. It is currently up for investigation to determine the root cause and initial discussions seem to indicate that the interrupt framework is the likely candidate to start such work.

As of now this implementation does not provide a way to boot into a failsafe mode if authentication fails during secure boot. One improvement to this design could include the option to boot from eMMC with the option to include a fallback image in the event of authentication failure. In the same vein, the addition of a Trusted Platform Module (TPM) would provide the ability for a system architect to deploy measured boot. Measured boot enables the embedded system to have a configurable secure boot mode that allows for the logging of failures to authenticate with the option to halt/proceed boot. A TPM also provides a system designer the means to implement advanced health monitoring techniques: remote attestation and real time introspection, to executing processes.

This article was written by Michael Doran, Embedded Software Engineer, DornerWorks, and Mark Russell, Embedded Systems Branch Chief, U.S. Army DEVCOM Ground Vehicle Systems Center. For more information, visit here .