PhD Final Oral Proposal: Owen Hofmann, Nov. 30, 2012, 10 a.m, ACES 6.336

Contact Name: 
Lydia Griffith
Nov 30, 2012 10:00am - 11:30am

PhD Final Oral Proposal: Owen Hofmann

Date: November 30, 2012
Time: 10 a.m
Place: ACES 6.336
Research Supervisor: Emmett Witchel

Title: Rethinking Operating System Trust

Operating system kernels present a difficult security challenge. Despite their millions of lines of code and broad, complex attack surface, they remain a trusted component shared between all applications. If an attacker can combine an exploit for any application on a system with a kernel exploit or privilege escalation, the attacker can then control any other application, regardless of whether the second application was itself vulnerable.

This thesis presents two hypervisor-based systems: OSck, which increases the trustworthiness of a guest kernel by detecting kernel rootkits, and InkTag, which removes the need for an application to trust the kernel at all.  Vital to both systems is their use of information from a potentially malicious kernel. These systems rely on information from the kernel about its own functionality to make their implementation simpler, more efficient, and more secure. Importantly, although they rely on this information, they do not trust it. A kernel that lies about its functionality to appear benign will be detected, as will a kernel that simply acts maliciously.

OSck detects kernel rootkits: malicious software programs that are particularly difficult to detect because they modify internal kernel operation to hide their presence. Running concurrently with an operating system and isolated by the hypervisor, OSck verifies safety properties for large portions of the kernel heap with minimal overhead, by deducing type information from unmodified kernel source code and in-memory kernel data structures.

InkTag gives strong safety guarantees to trusted applications, even in the presence of a malicious operating system. InkTag isolates applications from the operating system and enables applications to validate that the kernel is acting in good faith, for example by ensuring that the kernel is mapping the correct file data into the application's address space.  InkTag introduces paraverification, a technique that simplifies the InkTag hypervisor by forcing the untrusted operating system to participate in its own verification. InkTag requires that the kernel prove to the hypervisor that its updates to application state (such as page tables) are valid, and also to prove to the application that its responses to system calls are consistent. InkTag is also the first system of its kind to implement access control, secure naming, and consistency for data on stable storage.