Type-Safe Operating System Abstractions

Operating systems and low-level applications are usually written in languages like C and assembly, which provide access to low-level abstractions. These languages have unsafe type systems that allow many bugs to slip by programmers. For example, in 1988, the Internet Worm exploited several insecure points in Unix including the finger command. A call to finger with an unexpected argument caused a buffer overflow, leading to the shutdown of most Internet traffic. A finger application written in a type-safe language would have prevented its exploit and limited the points the Internet Worm could attack. Such vulnerabilities are unacceptable in security-critical applications such as the secure coprocessors of the Marianas network, secStore key storage from Plan 9, and self-securing storage. This research focuses on safe language techniques for building OS components that cannot cause memory or IO errors. For example, an Ethernet device driver communicates with its device through IO operations. The device depends on FIFO queues to send and receive packets. A mistake in an IO operation can overflow or underflow the FIFO queues, cause memory errors, or cause configuration inconsistencies on the device. Data structures such as FIFO queues can be written safely in safe languages such as Java and ML but these languages do not allow the access to the low-level resources that an OS programmer needs. Therefore, safe OS components require a language that combines the safety of Java with the low-level control of C. My research formalizes the concurrency, locks, and system state needed by the safety-critical areas of a device driver. These formal concepts are built on top of an abstract syntax and rules that guarantees basic memory safety using linear and singleton types to implement safe memory load and store operations. I proved that the improved abstract machine retains the property of soundness, which means that all well-typed programs will be able to execute until they reach an approved end-state. Together, the concurrency, locks, and state provide safety for IO operations and data structures. Using the OSKit from the University of Utah as a starting point, I developed a small operating system. I ported the 3c509 Ethernet device driver from C to Clay, a C-like type-safe language that uses a type system powerful enough to enforce invariants about low-level devices and data structures. The resulting driver works safely in a multi-threaded environment. It is guaranteed to obtain locks before using shared data. It cannot cause a FIFO queue to overflow or underflow and it will only call IO operations when invariants are satisfied. This type-safe driver demonstrates an actual working application of the theoretical components of my research. The abstract machine is powerful enough to encode a given OS specification and enforce a provably matching implementation. These results lead towards fundamentally secure computing environments