search

CCC-Attestation / governance

Apache License 2.0
0 stars 5 forks source link

Formal specification and analysis of KBS attestation protocol #13

Closed muhammad-usama-sardar closed 7 months ago

muhammad-usama-sardar commented 8 months ago

Background material

Proposal

Formal specification and analysis of KBS attestation protocol in CoCo using ProVerif: The proposed level of abstraction for formal model is TLS layer.

The deliverables are:

High-level rationale

Reasons for KBS protocol

Proponents

thomas-fossati commented 8 months ago

cc @jdbeaney

wenhuizhang commented 8 months ago

KBS (Key Broker Service) is an essential feature typically employed for three main purposes:

  1. Full Disk Encryption at the initrd (initial ramdisk) Load Stage: This ensures that all data stored on the disk is encrypted and only accessible upon proper authentication at boot time, enhancing the security of the system right from the start.

  2. User Space Artifacts Encryption and Transmission at Runtime: KBS is used to encrypt sensitive user space data and artifacts, ensuring secure transmission and storage during application runtime. This protects data integrity and confidentiality against potential breaches or unauthorized access.

  3. Encryption of Sensitive Data When Transferred to Remote Storage or Untrusted Devices: KBS plays a crucial role in securing data in transit, encrypting sensitive information before it's sent to remote storage solutions or untrusted devices. This ensures that even if the data is intercepted, it remains protected and unreadable without the appropriate decryption keys.

Thus KBS-KMS communication protocol and its verification is very important, and currently we don't have a formal spec for KBS-KMS communication in the above 3 scenarios.

KeithMoyer commented 8 months ago

I think this type of effort, assuming it builds upon the previous formal analysis of the underlying primitives, is very valuable and is exactly where I was hoping this line of work would lead. I am supportive of this being pursued.

dcmiddle commented 8 months ago

This looks like valuable rigor for the CoCo project.

gkostal commented 8 months ago

I see the value in formally analyzing the KBS protocol. I support this effort.

thomas-fossati commented 8 months ago

[...] assuming it builds upon the previous formal analysis of the underlying primitives

@muhammad-usama-sardar could you please comment on @KeithMoyer's note above? I think this was the only clarification we felt we still needed confirmation upon.

muhammad-usama-sardar commented 8 months ago

I think this type of effort, assuming it builds upon the previous formal analysis of the underlying primitives, is very valuable and is exactly where I was hoping this line of work would lead. I am supportive of this being pursued.

@KeithMoyer Yes, the assumption is correct (for the final deliverable). The initial model will be TEE-agnostic just to understand KBS better without introducing the complexity of TEE-specific mechanisms. In the second stage, we will integrate Arm CCA and Intel TDX to analyze the security of composotion.

BTW I had good discussion with CoCo KBS team last Monday, and they welcomed the formal verification work. We plan to work in close collaboration with them to answer open questions.

jdbeaney commented 7 months ago

In the challenge response, the KBC generates the attestation evidence in the 'tee-evidence' field:

tee-evidence The attestation evidence is generated by the HW-TEE platform software and hardware in the KBC's execution environment. The tee-evidence formats depend on the TEE and are typically defined by the Attestation-Service.

Here is says the tee-evidence formats depend on the TEE and are typically defined by the Attestation-Service. If a particular TEE supports more than one evidence formats, is there a way for the Attestation-Service that evaluates the tee-evidence to declare the supported/required evidence formats. And, then have this declaration of supported/required evidence format to the TEE via the KBS challenge?

muhammad-usama-sardar commented 7 months ago

If a particular TEE supports more than evidence formats

Is there any TEE that has more than one evidence formats? In any case, both our current targets (Arm CCA and Intel TDX) have a single evidence format.

If a particular TEE supports more than evidence formats, is there a way for the Attestation-Service that evaluates the tee-evidence identify the supported/required evidence formats that can be provided to the TEE via the KBS challenge?

We believe yes because, in principle, there is no intrinsic limitation in CoCo's architecture.

jdbeaney commented 7 months ago

Yes, I foresee a single TEE supporting multiple evidence formats as the TEE capabilities expand and new measurements are added to the evidence. As well as changes to the evidence formats that align to emerging standards.

muhammad-usama-sardar commented 7 months ago

Yes, I foresee a single TEE supporting multiple evidence formats as the TEE capabilities expand and new measurements are added to the evidence. As well as changes to the evidence formats that align to emerging standards.

In the scope of this proposal, we will keep the ProVerif artifacts adaptable to such changes. This could be, for example, a non-deterministic choice of the n possible evidence formats that TEE supports, or a negotiation step to agree on a evidence format.

thomas-fossati commented 7 months ago

Re: voting. Being one of the proponents, I have to recuse.

jdbeaney commented 7 months ago

I support this effort.

dcmiddle commented 7 months ago

Looks like we have full consensus here. @muhammad-usama-sardar feel free to proceed.

muhammad-usama-sardar commented 7 months ago

Thanks everyone for the support; I look forward to another great project jointly with the SIG and CoCo KBS team. Please create a repo with the name formal-spec-KBS to proceed.

thomas-fossati commented 7 months ago

Awesome. I have created the repo [1] and added @muhammad-usama-sardar as a maintainer. Happy hacking!

[1] https://github.com/CCC-Attestation/formal-spec-KBS