{"id":{"repo_id":"ku","oai_identifier":"oai:kuscholarworks.ku.edu:1808/37970"},"canonical_url":"https://search.dev.ndltd.org/etd/ku/oai:kuscholarworks.ku.edu:1808/37970","repository":{"repo_id":"ku","name":"University of Kansas","base_url":"https://kuscholarworks.ku.edu/server/oai/request"},"display":{"title":"VERIAL: Verification-Enabled Runtime Integrity Attestation of Linux","abstract":"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.","abstract_html":"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.","abstract_has_math":false,"creators":["Neises, Michael Christian"],"institution":"University of Kansas","degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":[],"advisors":["Alexander, Perry"],"committee_chairs":[],"committee_members":[],"year":2024,"date_issued":"2024-12-31","date_published":"2024-12-31","updated_at":"2026-07-24T02:45:54Z","subjects":["Computer science","Attestation","Confidentiality","Integrity","Introspection","Rootkit","seL4"],"languages":["en"],"rights":["This item is protected by copyright and unless otherwise specified the copyright of this thesis/dissertation is held by the author."],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["https://www.proquest.com/LegacyDocView/DISSNUM/31559675"],"render_values":[{"text":"https://www.proquest.com/LegacyDocView/DISSNUM/31559675","href":"https://www.proquest.com/LegacyDocView/DISSNUM/31559675","code":true}]}]},"links":{"outbound_url":"https://hdl.handle.net/1808/37970","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Alexander, Perry"]},{"key":"dc:creator","label":"Author","values":["Neises, Michael Christian"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2026-04-22T16:36:46Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2026-04-22T16:36:46Z"]},{"key":"dc:date.issued","label":"Date","values":["2024-12-31"]},{"key":"dc:publisher","label":"Institution","values":["University of Kansas"]},{"key":"dc:type","label":"Dc Type","values":["Dissertation"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Computer science","Attestation","Confidentiality","Integrity","Introspection","Rootkit","seL4"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["This item is protected by copyright and unless otherwise specified the copyright of this thesis/dissertation is held by the author."]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.other","label":"Dc Identifier Other","values":["https://www.proquest.com/LegacyDocView/DISSNUM/31559675"]},{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1808/37970"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["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."]},{"key":"dc:title","label":"Title","values":["VERIAL: Verification-Enabled Runtime Integrity Attestation of Linux"]}]}],"canonical_facts":{"dc:contributor.advisor":["Alexander, Perry"],"dc:creator":["Neises, Michael Christian"],"dc:date.accessioned":["2026-04-22T16:36:46Z"],"dc:date.available":["2026-04-22T16:36:46Z"],"dc:date.issued":["2024-12-31"],"dc:description.abstract":["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."],"dc:identifier.other":["https://www.proquest.com/LegacyDocView/DISSNUM/31559675"],"dc:identifier.uri":["https://hdl.handle.net/1808/37970"],"dc:language.iso":["en"],"dc:publisher":["University of Kansas"],"dc:rights":["This item is protected by copyright and unless otherwise specified the copyright of this thesis/dissertation is held by the author."],"dc:subject":["Computer science","Attestation","Confidentiality","Integrity","Introspection","Rootkit","seL4"],"dc:title":["VERIAL: Verification-Enabled Runtime Integrity Attestation of Linux"],"dc:type":["Dissertation"]},"updated_at":"2026-07-24T02:45:54Z"}