[seL4] Re: Inquiry to Verified Components

A very recent use case where attestation is used is in Intel SGX https://www.intel.com/content/www/us/en/developer/tools/software-guard-exten.... SGX is used on some Intel servers where the data in compute needs to be secure. Another example is TPM https://en.wikipedia.org/wiki/Trusted_Platform_Module, extensively used in Windows machines https://learn.microsoft.com/en-us/windows/security/information-protection/tp... . We plan to implement similar functionalities on embedded platforms with formal guarantees. Especially on ARM-based processors, such as Sabrelite. Hope this helps. Please let me know if you have any further questions. On Wed, Jan 25, 2023 at 4:09 PM Zenaan Harkness wrote:

Thank you for that explanation of the attestion process, I appreciate your clairty.

Do you have a real world use case you can share please?

Thank you, Zenaan

On 1/26/23, Sashidhar Jakkamsetti wrote:

...

Say we have two actors: (1) the device, aka prover, installed with sel4 and our attestation service, and (2) the device owner, aka, the verifier.

Verifier decides what applications can run on the prover. For example, there are two applications: app1 and app2. Once configured, the verifier deploys the prover at a remote location. Now when the verifier wants to connect to app1 to request a service, it sends an attestation request to our attestation process to check the status of app1, i.e., whether app1 is running and in good condition. As a response to the request, the verifier gets a signature indicating that app1 is alive and healthy, and also an encryption key that the verifier can use to further communicate with app1. Similarly, the same goes for app2.

We imagine attestation to be implemented like this: signature_app1 = ECDSA{signing_key, nonce, SHA2(binary_of_app1) || SHA2(encryption_key_of_app1)}, where signing_key is the secret key of the attestation process.

On Wed, Jan 25, 2023 at 2:05 PM Zenaan Harkness wrote:

...

On 1/26/23, Sashidhar Jakkamsetti wrote:

...

To briefly introduce what we are working on: We aim to build a remote attestation service for the processes running atop seL4, and for that, we are planning to spawn a separate (formally-verified) process that handles attestation. This attestation process needs to be high-assurance for obvious reasons because it contains a secret key that is used for implementing digital signatures. For more details on this, please refer to one of our old papers:

https://urldefense.com/v3/__https://arxiv.org/pdf/1703.02688.pdf__;!!CzAuKJ4...

...

,

...

which discusses a basic version of attestation (but without formal guarantees though).

Please briefly describe the use case for this implementation.

Thank you, Zenaan

-- Sashidhar Jakkamsetti University of California Irvine, Ph.D. https://sites.uci.edu/sashidharjakkamsetti/

-- Sashidhar Jakkamsetti University of California Irvine, Ph.D. https://sites.uci.edu/sashidharjakkamsetti/