generated from riscv/docs-spec-template
-
Notifications
You must be signed in to change notification settings - Fork 23
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #75 from gdhh/main
Broaden the specification's scope to embedded systems with simpler hardware and reduced functionalities
- Loading branch information
Showing
12 changed files
with
545 additions
and
252 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,86 @@ | ||
[[appendix_d]] | ||
== Appendix D: M-mode TSM based deployment model | ||
|
||
This deployment model targets high-assurance systems whose design might be constrained | ||
by real-time and formal verification requirements. It trade offs a feature-rich design supporting | ||
dynamic resource allocation, for simpler implementation, where the correctness can be formally verified. | ||
|
||
[id=dep3] | ||
[caption="Figure {counter:image}"] | ||
[title= ": M-mode TSM based deployment model for CoVE"] | ||
image::img_11.png[align=center] | ||
|
||
=== Overview | ||
<<dep3>> shows that the deployment model supports a single confidential supervisor domain in which | ||
the TSM runs along with the TSM driver in the M-mode. This single confidential supervisor domain can run multiple | ||
TVMs that are isolated from each other using the MMU, i.e., G-stage page tables managed by TSM. TSM isolates the | ||
hosting supervisor domain (i.e., OS/VMM and non-confidential applications and VMs) from the confidential supervisor | ||
domain (TSM and TVMs) using a hardware memory isolation mechanism, like PMP. | ||
The Supervisor Domain Access Protection (Smmtt) extension is therefore not required in this model but not precluded. | ||
IO accesses to confidential memory must be prevented, for example, with IOPMP. | ||
|
||
[NOTE] | ||
==== | ||
Since the TSM is not required to run in the HS-mode, this deployment model supports systems that emulate the | ||
hypervisor extension or run TVMs and OS/VMM in S-mode. The latter requires use of a hardware memory isolation mechanism | ||
that enforces memory accesses to confidential memory while being only controlled by the TSM, e.g., PMP. | ||
==== | ||
|
||
=== Static memory partitioning | ||
The deployment model proposes static partitioning of memory into confidential and non-confidential to simplify | ||
formal reasoning about the correctness of the TVM execution and isolation. TSM performs this paritioning early | ||
during the boot of the platform, resulting in the following advantages: (1) simplified formal reasoning about the | ||
ownership of memory, (2) attestation that covers static system configuration (e.g., values of PMP registers), | ||
(3) reduced attack surface between OS/VMM and TSM due to narrower ABI. A possible negative consequence of | ||
static partitioning is underutilization of resources. Specifically, confidential memory created at platform | ||
initialization might be larger than the required amount of memory utilized by TVMs and the TSM during runtime. | ||
Lack of the conversion mechanism of confidential memory pages to non-confidential memory (enabled for example by Smmtt) | ||
prevents the hosting supervisor domain (OS/VMM, applications, and VMs) from using the memory over-provisioned by | ||
the confidential supervisor domain (TSM, TVMs). | ||
|
||
=== TVM creation | ||
To reduce the complexity of the TSM implementation, the TSM creates a TVM as a result of a single operation triggered with | ||
the `sbi_covh_promote_to_tvm()` call. Specifically, OS/VMM initializes and starts a regular VM, which early during the | ||
boot process requests to be promoted to a TVM. This call traps in the OS/VMM and is reflected to the TSM, which copies | ||
VM's data, the page table configuration, and the vCPU state into confidential memory. If the request fails, the promotion | ||
of a VM to a TVM fails and error is returned to the VM. When the request succeeds, OS/VMM marks the VM as a TVM, | ||
so that it can then properly resume its execution via TSM. | ||
|
||
=== Local attestation | ||
Embedded systems might operate without access to a network, which prevents use of remote attestation. For this | ||
reason, this deployment model also supports local attestation, in which the TSM attests to the integrity of the TVM image | ||
during its creation and allows its creation only when it contains a specfic `TVM attestation payload` (TAP). This | ||
payload carries a cryptographic proof issued with the expected attestation key specific to the TSM integrity | ||
and platform configuration. The pointer to TAP is passed in a call to promote a VM to a TVM. If it is zero, | ||
then remote attestation is used, otherwise local attestation is used. Local attestation is strongest when it is hardware enforced. | ||
|
||
Attestation for embedded systems utilizes one or both of the following properties: | ||
|
||
. The embedded platform must be able to verify that the TVM is authorized to run on the platform. | ||
. The TVM must be able to verify that the configuration of the hardware platform is acceptable/correct. | ||
|
||
Separate mechanisms may be used to achieve these goals. | ||
|
||
==== TVM Authorization | ||
The TSM must have a list of public keys of those authorized to sign VMs (TVMs) for execution on the platform. The attestation payload associated with the TVM will be | ||
signed with a private key. When the VM is being promoted to a TVM, TSM checks the signature inside the TAP. | ||
If the signature is not valid, the TSM will not convert the VM and will terminate execution of the | ||
VM. The method for provisioning these public keys into the TSM is outside the scope of this specification. | ||
|
||
==== Verifying Platform configuration | ||
When the creator of the (authorized) TVM does not want it to execute on improperly configured or unauthorized hardware, there should be a mechanism supported by hardware (and firmware) for verification. | ||
Assuming presence of the hardware root-of-trust for measurement and hardware root-of-trust for storage, the VM can be created with an encrypted disk and the key that is used to decrypt the disk can be sealed to the measurments of the platform. | ||
The creator of the VM using the specifications for the platform decides what values are required in order for the key to be released. | ||
When the request to promote VM to a TVM is called and local attestation is successful, the TSM unseals the key with help of the hardware root-of-trust. At the point when the TVM needs to decrypt its disk (e.g., for mounting the filesystem), the TVM utilizes an ABI call (`covg_retrieve_secret()`) to retrieve the decryption key from the TSM. | ||
|
||
=== Further recommendations | ||
Embedded systems with real-time requirements must have a fixed upper bounded execution time. This requires determining | ||
the maximal number of instructions that can execute between TVM context switches. From this reason, this deployment model | ||
recommends an uninterruptible TSM. <<depd2>> shows this operation mode, in which TSM running in M-mode exposes COVH and | ||
COVG ABI to OS/VMM and TVM, respectively. VM ECALLs trap directly to TSM due to the `medeleg` configuration and all | ||
interrupts during TVM execution trap in TSM due to the `mideleg` configuration. | ||
|
||
[id=depd2] | ||
[caption="Figure {counter:image}"] | ||
[title= ": TSM operation"] | ||
image::img_12.png[align=center] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.