Broaden the specification's scope to embedded systems with simpler hardware and reduced functionalities #75
Conversation
…th details of the deployment model
This section has been updated to introduce the concept of COVE on a system without Smmtt.
There are two updates here to the second line in the tabel labeled Memory Confidentiality. The first is to change MMU to xMMU because the IO/MMU may also be affected. The second is to make this optional. The line above it and this line should probably be combined. The previous line subsummes this line. IF you prevent non-TCB components from reading TEE memory it does not matter if the TEE memory is encrypted.
Update to integrate deployment model 3 at the appropriate locations
For some use cases local attestation is arequrement because the system running the TVM will/may not have connectivity to a remote verifyer.
Additions/changes made to allow for deployment model 3. In deployment model 3 Smmtt is not required so some text had to be modified.
Reformatting of the source and minor syntax corrections.
A more through descripion of how local attestation worked for PEF. something like this needs to be in Appendix D.
Added a few sentences to make it clear that processors without Smmtt can support COVE.
Add some text describing the requirements for mutual local attestation. By mutual we mean that the embedded platform can verify that the VM/TVm is authorized to run on the platform. The VM/TVM must also be able to verify that the platform configuration is correct.
Signed-off-by: Wojciech Ozga <[email protected]>
Signed-off-by: Wojciech Ozga <[email protected]>
Local attestation for embedded systems should not require both of the properties previously listed. When a system is disconnected and the creator will only their firmware to run, mutual verification is not required.
Signed-off-by: Wojciech Ozga <[email protected]>
Signed-off-by: Wojciech Ozga <[email protected]>
…ix D) Signed-off-by: Wojciech Ozga <[email protected]>
Not necessarily if the non-confidential VMs are run as a nested VM. But TSM does have to some additional H-mode state to enable that.
Agreed. I was just trying to understand the challenges of formal verification between running different models. It seems it boils down to more complex TSM code/additional privilege state management vs more code in M-mode. As per my understanding from your and @wojciechozga's response, the later is easier. But if we can axiomatize hardware implementation and verifying only a subset of TSM functionality is okay, it shouldn't matter. Isn't it ? |
…e_to_tvm() call. Signed-off-by: Wojciech Ozga <[email protected]>
Signed-off-by: Wojciech Ozga <[email protected]>
I think this is a reasonable summary.
I believe that by verifying only a subset of TSM functionally you mean that only the functionality that affects TVM. I do not think that this is a good approach. Because the VMs and TVMs would be sharing the same TSM the side channel issue discussed below has to be considered. If by nested VMs you mean running a second level hypervisor that services all non confidential VMs. That could possibly work (assuming the correct hardware support). However, it is more complex than what we have proposed. The other issue is that unless we change the hardware implementation, the second level hypervisor would possibly have to get services from the TSM. In addition to proof complexity, once the TSM is servicing anyone other than TVMs we open up the possibility of side channels. In particular we would have to show that there is no way to leak information between the TVS and the VMs (or second level hypervisor). Essentially, you need to show that nothing the VMs do will influence the TVMs and that none of the VM request will be influenced by the TVMs. I believe that it is possible to build a system with this approach where this is true. But it puts an additional architecture and proof burden on the system that the approach we have proposed does not have. The TSM only services one call from the VMs. That call results in the VM either being terminated because it fails attestation or becoming a TVM. Properly chosen cryptographic algorithms and key length (and key material) means that try fail semantics to break into the system would take too long to be practical. Our current proof approach is not without side channel issues. We have to show that TVMs do not leak information to one another because they share the same TSM. Our approach to this might also work for an approach where the TSM services both, but that is a complexity we are avoiding. My statement on the required additional proof work is only an observation of the amount of work to be done and not a judgement as to whether it can be done. We are still in the process of proving the current approach so we do not know whether we will be successful, but we suspect so. We want to add some additional capabilities but not until we have a proven base. |
Signed-off-by: Wojciech Ozga <[email protected]>
There was a problem hiding this comment.
after thinking some more, had a couple questions on the promote abi @wojciechozga
Signed-off-by: Wojciech Ozga <[email protected]>
Signed-off-by: Wojciech Ozga <[email protected]>
Signed-off-by: Wojciech Ozga <[email protected]>
Signed-off-by: Wojciech Ozga <[email protected]>
Syntax changes for clarification. Signed-off-by: Guerney D. H. Hunt <[email protected]>
|
I reviewed the changes an made a few minor corrections for clarity. |
Co-authored-by: Ravi Sahita <[email protected]> Signed-off-by: Wojciech Ozga <[email protected]>
There was a problem hiding this comment.
seems ok to merge now (will merge today afternoon unless any objections)
@atishp04 @eckhard-delfs-qualcomm @wojciechozga @gdhh
Guerney and I introduce in this PR changes to the CoVE spec that make the spec suitable for broader number of use cases, like embedded systems, simpler processors, systems designed under the formal verification regime, such as assured confidential execution (ACE) that we develop as open source project: https://github.com/IBM/ACE-RISCV
Single-step TVM creation. This would be an alternative to the currentMulti-step TVM creation. To make it possible we propose to add a new COVH call: covh_promote_to_tvm()