search

GaloisInc / VERSE-OpenSUT

Open System Under Test (SUT) for the VERSE demonstrator
BSD 3-Clause "New" or "Revised" License
2 stars 0 forks source link

readme

VERSE-OpenSUT

Open System Under Test (OpenSUT) is a fictitious airborne platform that represents a notional high-consequence national security system. OpenSUT is used for evaluation and evolution of VERSE tools.

Introduction

This is a companion to the VERSE Toolchain repository for TA1.

[ VERSE project proposal ]

How to contribute

Writing good requirements

First, read about how to write good requirements:

Then, each requirement consists of:

Description

Open System Under Test (OpenSUT) is a fictitious airborne platform that represents a notional high-consequence national security system. OpenSUT contains a Mission Protection System (MPS) which protects the (virtual) engine from getting outside of its safe operating conditions, a Mission Key Management system (MKM) that handles mission keys, platform attestation and provides various cryptographic services provided by the Platform Crypto. An autopilot provides basic flight control and waypoint following ability. The components communicate via point-to-point connections routed through a message bus.

Additional optional components might be included, depending on the direction from the client. Those include a camera that provides high-resolution video and a realistic amount of data, a system logger for logging system events at different classification levels, a mission processing system serving as the main mission computer, and external comms for communicating with a fictional remote operator for unmanned platform operation.

We are intentionally ambiguous about some details, such as whether the OpenSUT is a manned or unmanned platform (it does have a basic autopilot), or whether it is a fixed wing or a VTOL. Depending on timing and client needs, we can adapt OpenSUT as necessary. We intent to build OpenSUT in a way that is similar to industry standards, such as Open Mission Systems (OMS). This means having a publish-subscribe bus, and a well defined set of messages and interfaces.

OpenSUT components can be thought of as the application code, and each component runs inside a virtual machine. The components run on a one or more of host computers, where at least one is a multi-core CPU running multiple components, and one is a single core CPU hosting a Real-Time-Operating-System (RTOS) and running the autopilot. Running the components in such a virtualized environment, including virtualized hardware, mirrors the architecture of real platforms.

OpenSUT uses a standard linux with pKVM support as a hypervisor, and while we realize that a standard linux kernel is not real-time capable and is not a certifiable for airworthiness, it is a good open substitute for Lynx Secure that we intend to use for the proprietary SUT in Phase 2.

All CPUs are ARM64 architecture, because pKVM supports only that instruction set. For easy deployment, we will emulate the host computers in QEMU instances. Some auxiliary processes, such as a flight simulator, are expected to run directly on the user's machine, or in separate docker containers.

OpenSUT shall operate in the following scenarios:

Scenario 1: Boot OpenSUT to a known initial state

Measured boot

In this scenario, one or more components of OpenSUT boot using SHAVE Trusted Boot. It means that the application code is measured, hashed, and compared against a stored expected measure. Only if these values match, the application code is started. If they don't match, an error is thrown, the boot is aborted and an error message is possibly sent and logged. If the attestation of each securely booted component passes, the system will be in a known initial state, fully provisioned. Measured boot ensures that only the expected code is running on OpenSUT.

Attested boot

An optional - and more complex - attested boot may be added. During attested boot, the last known measure is stored in persistent memory, so it is known whether the system was booted from a known state in the past. Attestation requires a provisioned key, received from the Mission Key Management component, and the component attests its state to the Mission Key Management (MKM) component. The goal is to ensure that only the application code that has been signed by an external authority (e.g. the trusted component manufacturer) is running on the OpenSUT.

For the purpose of this scenario, we assume that each host computer contains a root of trust, a trusted boot that can bring up the hypervisor. In other words, we assume the host OS to be trusted (see the Threat model). Because hardware root of trust, trusted boot and attestation are all complex topics, only the application code will be attested in this scenario.

We expect the code to be signed with eXtended Merkle Signature Scheme (XMSS), as XMSS is commonly used for firmware signing, and is believed to be quantum safe.

Scenario 2: Load mission key

Once the platform is fully provisioned, load the mission keys to the Mission Key Management component. The loading could happen through a direct UART connection to the MKM, or through the message bus. In both cases, we expect the keys to be encrypted, such that they are never transported in plaintext.

The platform data have two different classification levels (low and high), the low data are unencrypted, while the high data are protected by the mission keys. The keys are used for the encryption of data both in transit (data sent between components) and at rest (e.g., stored in System Log). We expect the high key to be used for encrypting high data any time they are exchanged between components, and the low key is used to encrypt data logs.

We intend to use the standard symmetric keys (e.g. AES256), as well as asymmetric key for a post-quantum cryptographic algorithm (e.g., KYBER or Dilithium). We will choose an appropriate encryption scheme for the key transfer, key exchange, and for the data encryption.

Scenario 2A: No adversary on the bus

In this case, we assume there is no adversary on the bus, thus the messaging bus can be trusted. Because the bus is redundant, the messages are assumed to be always delivered correctly. In such case, mission keys can be exchanged directly between components.

Scenario 2B: Adversary on the bus

In this case, an adversary might be present on the bus, and is able to eavesdrop and alter/replay messages. As a result, a secure key distribution algorithm needs to be deployed for sharing mission keys.

Scenario 3: Execute a mission

After the OpenSUT boots up, initializes to a known state, and loads mission keys, a mission plan is uploaded. The OpenSUT's autopilot then takes off, flies the mission following a set of waypoints, returns to land, and lands at the same position as it started from.

Scenario 4: Decommission the OpenSUT

When a mission is completed, or when the OpenSUT is about to be shut down, ensure all data is properly saved to the System Log. The system logs are then exported, and the keys are erased from the Mission Key Management component. Erase all sensitive data from the OpenSUT.

If the optional System Log is not selected by the client, we can build a minimal logging system utilizing a system log service on the Guest Linux OS. Both encrypted high messages and plaintext low messages are saved in the system log. An external Management Interface can then query the system logs from the component. After retrieving them, all mission data are deleted.

Requirements

We will provide top level requirements, as well as refined requirements for each subsystem. Requirements shall be provided as a part of the Magic Draw SysML project, and exported into a plaintext format (likely Markdown) for easier viewing. We will track the requirements throughout the development process - ideally each line of the code, and each CN specification will be traceable to one of the top level requirements.

In Phase 1, we intend to verify the following properties of OpenSUT code:

The list of all properties we intend to address during the program, and the respective Phases are shown below:

properties_and_phases

OpenSUT will be delivered with an assurance case, assembled with Adelard's Assurance and Safety Case Environment (ASCE). New change requests will add and/or change the top-level and derived requirements.

The basic top-level requirements for OpenSUT are under active development, in the meantime we have requirements for the Mission Protection System (MPS) in the MPS's README

Models

OpenSUT follows the best practices of Rigorous Digital Engineering, providing rich models and executable specifications where applicable. The various models will include:

Domain Model

Domain model is a part of Domain Engineering, and is in its simplest form a glossary. For our purposes we can think of the domain model as an ontology. The domain model is expected to grow over time. Following are the most important OpenSUT domain concepts:

Assurance Case

From: https://csrc.nist.gov/glossary/term/assurance_case

A reasoned, auditable artifact created that supports the contention that its top-level claim (or set of claims), is satisfied, including systematic argumentation and its underlying evidence and explicit assumptions that support the claim(s).

Attestation

The process of providing a digital signature for a set of measurements securely stored in hardware, and then having the requester validate the signature and the set of measurements.

Hypervisor

The virtualization component that manages the guest OSs on a host and controls the flow of instructions between the guest OSs and the physical hardware.

Key Distribution

The transport of a key and other keying material from an entity that either owns or generates the key to another entity that is intended to use the key.

Mission Keys

Mission keys are a pair of cryptographic keys, issued and valid for a particular mission. First key is used for protecting high (or sensitive) data in transit (i.e. when passed between OpenSUT components), while the second key is used to protect high data at rest (i.e. in the system log). The keys are typically a combination of one symmetric key, and one asymmetric key.

pKVM

pKVM is a KVM-based hypervisor that isolates pVMs and Android into mutually distrusted execution environments. These properties hold in the event of a compromise within any pVM, including the host. Alternative hypervisors that comply with AVF need to provide similar properties.

Root of Trust

Highly reliable hardware, firmware, and software components that perform specific, critical security functions. Because roots of trust are inherently trusted, they must be secure by design. Roots of trust provide a firm foundation from which to build security and trust.

Trusted Boot

A system boot where aspects of the hardware and firmware are measured and compared against known good values to verify their integrity and thus their trustworthiness.

Virtual Machine

A simulated environment created by virtualization.

Threat Model

We are assuming that the underlying emulated hardware, and the host OS are trusted, while the hypervisor and the virtual machines and all application code is generally untrusted and thus needs to be verified (unless otherwise noted). While this might seem as a strong assumption, it reflects the fact that proving the correctness of the hypervisor is out of scope for VERSE. More details about our assumptions can be found in the EXPERIMENTAL SETUP document. Note that while our Scenario 1 assumes that anything below the application code is trusted, otherwise our minimal secure boot would not be sufficient. We realize that this is at odds with the generally untrusted hypervisor and guest VM OS. We make an exception, and assume that the hypervisor's boot sequence is trusted and it can reliably bring up the application code.

The hypervisor shall ensure space and time separation between components, so even if a single component is compromised, it can affect other components only through already available interfaces (e.g. a point-to-point connection). Note that neither the pKVM capable linux kernel, nor Lynx Secure has been formally verified, thus the time and space separation is only assumed at this point. However, pKVM is currently undergoing a formal verification (see this paper for details), and the Lynx Secure hypervisor holds a DO-178C DAL A certification​, ensuring a good quality of the code.

We assume that the connection between components that are on the same host computer to be trusted, but the message bus in general is untrusted. This will have some interesting implications for attestation, key distribution and data transfer. We will elaborate the threat model as we implement each scenario. See Scenario 2 for details.

SysMLv1 Model

The SysML model is created in Cameo/MagicDraw v2022, and contains:

Below is a simple top-level SysML block diagram of OpenSUT. Yellow blocks contain the application code, and are described in Components section. Red blocks denote optional components. Green blocks represent the hypervisor and pKVM virtual machine guests. Blue blocks represent the underlying ARM64 hardware. The connections between the application components are notional, as any cross-component communication will need to pass through the hypervisor and use virtualized devices.

OpenSUT-SysML-top-level-view

AADL Model

We will export the SysML model into AADL with the CAMET SysML2AADL bridge, in order to facilitate advanced analysis, such as:

Code

This repository provides both the model and the implementation of the OpenSUT. Our development practices and the branching structure are summarized in CONTRIBUTING.md. CI/CD will be added and expanded as our work progresses.

The main dependency will be a recent version of QEMU that can emulate an ARM64 platform, and a Linux-like OS that can at least run docker. We will use docker as much as possible to package the auxiliary processes, such as a flight simulator. We will provide documentation for installing dependencies and running OpenSUT scenarios.

The repository structure is as follows:

The majority of the code is written in C and will have properties written in CN.

Proofs

OpenSUT uses CN for testing and verification of the application C code. The results of the testing and verification runs (such as logs, counterexamples and other artifacts) are attached to each CI run, and re-generated when OpenSUT is executed locally. Thus a OpenSUT user can easily reproduce out verification results.

We will utilize automated code generation when appropriate, for example use the SysML model for partial test generation, or the AADL model to generate implementation stubs. For most components we have prior specification and models available, written in Cryptol, SAW and/or Frama-C. We convert these specifications into CN as a part of our work.

For example, below is a snippet of code from the Mission Protection System. Function get_actuation_state() which reads the actuation signal, has Frama-C specs, that were translated into CN:

// Reading actuation signals
//frama-c
/* @ requires i <= 1;
  @ requires device < NDEV;
  @ requires \valid(value);
  @ assigns *value;
  @ ensures (\result == 0) ==> (*value == 0 || *value == 1);
  @ ensures (\result != 0) ==> (*value == \old(*value));
*/
int get_actuation_state(uint8_t i, uint8_t device, uint8_t *value);
//CN
/*@ spec get_actuation_state(u8 i, u8 device, pointer value)
    requires i <= 1u8;
             device < NDEV();
             take vin = Owned<uint8_t>(value)
    ensures take vout = Owned<uint8_t>(value);
            ((return == 0i32) ? (vout == 0u8 || vout == 1u8) :
             (vout == vin))
@*/

Similarly, the function ActuateActuator() which controls the engine kill switch, has the following Frama-C and CN specifications:

//frama-c spec function
/*@
  @ // Refines MPS::Actuator::ActuateActuator
  @ logic boolean ActuateActuator(uint8_t input) =
  @   ((input & 0x1) != 0) || ((input & 0x2) != 0);
  @ }
*/

// CN spec function
/*@
function (bool) ActuateActuator(u8 input) {
  ((bw_and_uf(input, 1u8) != 0u8) || (bw_and_uf(input, 2u8) != 0u8))
}
@*/

//frama-c
/* @ assigns \nothing;
  @ ensures \result == 0 || \result == 1;
  @ ensures \result == 1 <==> ((vs & 0x01) || (vs & 0x02));
  @ ensures ActuateActuator(vs) <==> \result == 1;
*/
uint8_t ActuateActuator(uint8_t vs);
//CN
/*@ spec ActuateActuator(u8 vs)
    requires true
    ensures (return == 0u8 || return == 1u8);
      return == 1u8 ? (bw_and_uf(vs, 1u8) != 0u8 || bw_and_uf(vs, 2u8) != 0u8) : true;
      iff(ActuateActuator(vs), return == 1u8)
 @*/

In some cases (such as the Mission Computer) no existing specs are available. In those cases we will write CN specifications from scratch, and trace them towards the appropriate requirements.

Components

Below we describe each component of the OpenSUT. Component implementation, specs, tests and proofs will be in components folder and/or the architecture model. The Source field points to the relevant code that the component might depend on, or that might serve as an inspiration for the component implementation.

Note that for the baseline version of OpenSUT, we highlight the expected functionality of each component, and point to the relevant sources where appropriate. Often the baseline components we refer to are already high-assurance with some sort of specification and/or formal verification. In such cases, we don't necessarily expect to add more assurance to the component with the CN properties, but we intend to highlight how much faster we can achieve comparable level of assurance with VERSE tools.

Autopilot

Message Bus

Mission Key Management (MKM)

Mission Protection System (MPS)

Platform Crypto

[OPTIONAL] Camera

[OPTIONAL] External Comms

[OPTIONAL] Mission Processing

[OPTIONAL] System Log