VERIAL: Verification-Enabled Runtime Integrity Attestation of Linux

Runtime attestation is a way to gain confidence in the current state of a remote target. That confidence is valuable in safety-critical systems such as those involving health-care or finance. Layered attestation is a way of extending that confidence from one component to another. Solutions for layered attestation require strict isolation. Without that isolation, the boundaries between components are blurred, and trustworthy components become intermingled with untrustworthy ones. The seL4 is uniquely well-suited to offer kernel properties sufficient to achieve such isolation. While not the world’s only kernel with some formal verification, the seL4 is significantly more advanced than any other solution while uniquely offering the possibility of real-time computation. I design, implement, and evaluate introspective measurements and the layered runtime attestation of a Linux kernel hosted by the seL4. VERIAL can detect diamorphine-style rootkits with performance cost comparable to previous work.

Grantor dc:publisher

University of Kansas

Year dc:date.issued

2024

Author dc:creator

• Neises, Michael Christian

Advisor dc:contributor.advisor

• Alexander, Perry

• Computer science
• Attestation
• Confidentiality
• Integrity
• Introspection
• Rootkit
• seL4

Statement dc:rights

• This item is protected by copyright and unless otherwise specified the copyright of this thesis/dissertation is held by the author.

Language dc:language.iso

en

Dc Identifier Other

https://www.proquest.com/LegacyDocView/DISSNUM/31559675

OAI identifier oai:identifier

oai:kuscholarworks.ku.edu:1808/37970