A Safe OS Kernel
		          Thesis Proposal Talk

			    July 23, 2:00 PM
			       Moore B03

			       Lea Wittie

Operating systems and low-level applications are usually written in
languages like C and assembly which provide access to low-level
abstractions (e.g. bits and bytes). These languages have unsafe types
systems that allow many bugs to slip by programmers. For example, in 
1988, the Internet Worm exploited the finger command of Unix using a 
buffer overflow which resulted in the shut down of most internet traffic. 
Such vulnerabilities are unacceptable in security critical applications
such as the secure co-processors of the Marianas network (Nicol et al.), 
secStore key storage from Plan 9 (Bell Labs, Rob Pike et al.), and 
self-securing storage (Strunk et al.)

Writing an OS in a safe language would eliminate many vulnerabilities,
but typical safe languages (Java, ML) cannot give programmers access 
to the low-level resources they need. Therefore, we are creating a 
type-safe language that uses a type system powerful enough to enforce 
invariants about low-level devices and data structures. For example, 
an ethernet device driver needs queues to send and receive packets. The 
type system will ensure that the queues are FIFO and cannot underflow or 
overflow. This research builds on some recent type system advances 
including linear and singleton types.

Using the OSKit from the University of Utah as a starting point, we are
developing a small safe operating system in our language.

Joint work with Chris Hawblitzel