sid-agrawal
commented
3 months ago This paper talks about how to implment TEE without TEE HW, the TLDR is that stuff is encrypted on Context switch.
Look at the following paper that came up during TII’s presentation at the 2023 seL4 summit
- TEEVseL4: Trusted Execution Environment for Virtualized seL4-based Systems
- MicroTEE: Designing TEE OS Based on the Microkernel Architecture
To model TEE on OSmosis:
- Look at the paper that uses VT-X
- Think of which memory regions need to be unmapped when the CPU enters the kernel.
- What about CPU state? Can the kernel read that?
- How can the kernel relay data between the driver and the TEE w/o having access to it?
- Think of how the driver in sDDF does this w/o access to the data.
We need to ascertain that the OSmosis model can capture the isolation guarantees provided by a Trusted Execution Environment (TEE). In its most basic form, a TEE is supposed to provide confidentiality and integrity for the code and data running inside the TEE from the OS. We will examine Intel SGX (Software Guard Extensions) and ARM’s Trust Zones. Both implementations of the TEE concept are sufficiently different, and modeling just these two should suffice in determining if OSmosis can adequately model TEE. In SGX, the process data is confidential from the OS. An entirely isolated OS instance in the TZ is confidential from the primary OS.
The following should be clear from the model depiction: • That the OS cannot access the data pages of the application • A lower-level software (e.g., firmware in ARM) is still trusted.
This issue relates to the conversation about whether data is interpreted discussed in #41