ATTENTION: The software behind KU ScholarWorks is being upgraded to a new version. Starting July 15th, users will not be able to log in to the system, add items, nor make any changes until the new version is in place at the end of July. Searching for articles and opening files will continue to work while the system is being updated.
If you have any questions, please contact Marianne Reed at mreed@ku.edu .
A Verified Achitecture for Trustworthy Remote Attestation
dc.contributor.advisor | Alexander, Perry | |
dc.contributor.author | Jurgensen, Grant Alan | |
dc.date.accessioned | 2023-05-23T14:24:56Z | |
dc.date.available | 2023-05-23T14:24:56Z | |
dc.date.issued | 2022-05-31 | |
dc.date.submitted | 2022 | |
dc.identifier.other | http://dissertations.umi.com/ku:18223 | |
dc.identifier.uri | https://hdl.handle.net/1808/34202 | |
dc.description.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. | |
dc.format.extent | 54 pages | |
dc.language.iso | en | |
dc.publisher | University of Kansas | |
dc.rights | Copyright held by the author. | |
dc.subject | Computer science | |
dc.subject | Computation Tree Logic | |
dc.subject | Formal Methods | |
dc.subject | Remote Attestation | |
dc.subject | seL4 | |
dc.subject | Theorem Proving | |
dc.subject | Verification | |
dc.title | A Verified Achitecture for Trustworthy Remote Attestation | |
dc.type | Thesis | |
dc.contributor.cmtemember | Davidson, Drew | |
dc.contributor.cmtemember | Moore, Matthew | |
dc.thesis.degreeDiscipline | Electrical Engineering & Computer Science | |
dc.thesis.degreeLevel | M.S. | |
dc.identifier.orcid | https://orcid.org/0000-0001-6292-8558 | en_US |
dc.rights.accessrights | openAccess |
Files in this item
This item appears in the following Collection(s)
-
Theses [4088]