Loading...
A Verified Achitecture for Trustworthy Remote Attestation
Jurgensen, Grant Alan
Jurgensen, Grant Alan
Citations
Altmetric:
Abstract
Remote attestation is a process where one digital system gathers and provides evidence of its state and identity to an external system. For this process to be successful, the external system must find the evidence convincingly trustworthy within that context. Remote attestation is difficult to make trustworthy due to the external system’s limited access to the attestation target. In contrast to local attestation, the appraising system is unable to directly observe and oversee the attestation target. In this work, we present a system architecture design and prototype implementation that we claim enables trustworthy remote attestation. Furthermore, we formally model the system within a temporal logic embedded in the Coq theorem prover and present key theorems that strengthen this trust argument.
Description
Date
2022-05-31
Journal Title
Journal ISSN
Volume Title
Publisher
University of Kansas
Collections
Files
Research Projects
Organizational Units
Journal Issue
Keywords
Computer science, Computation Tree Logic, Formal Methods, Remote Attestation, seL4, Theorem Proving, Verification