[seL4] Re: Inquiry to Verified Components

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://arxiv.org/pdf/1703.02688.pdf, which discusses a basic version of attestation (but without formal guarantees though).

Please briefly describe the use case for this implementation. Thank you, Zenaan