eCommons

 

LANGUAGE–BASED TECHNIQUES FOR BUILDING TIMING CHANNEL SECURE HARDWARE–SOFTWARE SYSTEMS

dc.contributor.authorZagieboylo, Drew
dc.contributor.chairMyers, Andrewen_US
dc.contributor.committeeMemberSuh, Gookwon Edwarden_US
dc.contributor.committeeMemberSampson, Adrianen_US
dc.date.accessioned2024-04-05T18:48:41Z
dc.date.available2024-04-05T18:48:41Z
dc.date.issued2023-08
dc.description240 pagesen_US
dc.description.abstractWe rely on a deep stack of abstractions to efficiently build software applications without having to completely understand the nuance of language run- times, operating systems, and processor architectures. Each layer in the stack relies on the guarantees of the layer below, with all software relying on the functionality provided by the hardware on which it executes. Similarly, when we build secure software, we define security in terms of high level application policies and rely on a stack of abstractions to enforce those policies. Therefore, all of software security relies on the guarantees provided by processor hardware. However, those guarantees offer less protection than we have traditionally assumed, and real processor implementations routinely exhibit vulnerabilities that undermine traditional assumptions about hardware behavior. Modern processors incorporate a host of optimizations to execute software as quickly and efficiently as possible; unfortunately, these optimizations are at the root of some serious security weaknesses. In particular, researchers have recently discovered easily exploitable timing-channel vulnerabilities that arise due to processor speculation, like Spectre, Meltdown, and the many variants that have since been uncovered. Concerningly, these vulnerabilities are not the result of cutting-edge, untested optimizations; they are fundamental to the de- signs of almost all processors in the last 20 years. The existence of these vulnerabilities highlights the need for a well-defined contract between software and hardware that does not allow the hardware to leak software’s secrets arbitrarily, especially via timing channels. Furthermore, we need tools to enable the construction and verification of secure processors that adhere to these new contracts. As functional processor correctness is al- ready a difficult verification problem, we likely need new approaches to prove processor security. This dissertation addresses the above concerns by applying Information Flow Control (IFC) to both the hardware–software interface and to Hardware Description Languages (HDL) themselves. By using IFC as the de facto language of security, we can define a hardware–software contract capable of providing timing-channel security without exposing extraneous details about processor internals. Intuitively, using IFC as a tool to then build processors also enables proving that real processor implementations refine this IFC contract. This dissertation also addresses the problem of constructing correct processors by introducing a high-level HDL that targets the design of efficient processor pipelines. By raising the abstraction of hardware design, we can more easily connect the implementation’s semantics to the hardware–software contract. We can also reason statically about complex optimizations such as speculation by providing abstractions that generate correct circuitry by construction. We hope that future processors and interfaces are designed with timing- channel security in mind, and that these new abstractions will percolate back up the software stack to make timing-channel security available and efficient for all applications.en_US
dc.identifier.doihttps://doi.org/10.7298/eayn-6942
dc.identifier.otherZagieboylo_cornellgrad_0058F_13786
dc.identifier.otherhttp://dissertations.umi.com/cornellgrad:13786
dc.identifier.urihttps://hdl.handle.net/1813/114817
dc.language.isoen
dc.rightsAttribution-ShareAlike 4.0 International*
dc.rights.urihttps://creativecommons.org/licenses/by-sa/4.0/*
dc.subjectComputer Architectureen_US
dc.subjectComputer Securityen_US
dc.subjectInformation Flow Controlen_US
dc.subjectProgramming Languagesen_US
dc.titleLANGUAGE–BASED TECHNIQUES FOR BUILDING TIMING CHANNEL SECURE HARDWARE–SOFTWARE SYSTEMSen_US
dc.typedissertation or thesisen_US
dcterms.licensehttps://hdl.handle.net/1813/59810.2
thesis.degree.disciplineComputer Science
thesis.degree.grantorCornell University
thesis.degree.levelDoctor of Philosophy
thesis.degree.namePh. D., Computer Science

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
Zagieboylo_cornellgrad_0058F_13786.pdf
Size:
843.98 KB
Format:
Adobe Portable Document Format