|
A Type Safe OS Kernel
This project is exploring the use of type safe languages in writing an
OS Kernel. The languages use an advanced type systems to prevent data misuse
within Kernel memory. The project has focused on the needs of device drivers
since studies have shown that these contain most OS bugs.
Formal languages developed in this project include
Lambda-low which provides linear access to memory,
Lambda-concurrent which adds concurrency support (locks) to Lambda-low,
and Laddie (Language for Automated Device Drivers), a specification
language for the IO interface used between a driver and a device.
The formal languages are all implemented in concrete languages and
actual device driver code has been written in them and run in Linux on a
network card.
Lambda-low and Lambda-concurrent are implemented in Clay, a C-like
imperative language with linear access to memory, arithmetic constraints
on function pre- and post-conditions, and concurrency support. After
typechecking, Clay compiles to C++. Laddie is implemented as a declarative
language which compiles to Clay.
Clay Files
Laddie Files
Publications
- Lea Wittie, Chris Hawblitzel, Derrin Pierret.
Generating a Statically-Checkable Device Driver I/O Interface
APGES 2007.
- Chris Hawblitzel, Heng Huang, Lea Wittie, and Juan Chen.
A Garbage-Collecting Typed Assembly Language.
In TLDI, January 2007.
- Chris Hawblitzel, Edward Wei, Heng Huang, Erik Krupski, and Lea
Wittie.
Low-Level Linear Memory Management. In SPACE, January 2004.
Tech Reports
- Lea Wittie
Laddie: Language for Automated Device Drivers, Bucknell TR #08-2
- Lea Wittie
Clay User's Guide, Bucknell TR #08-1
- Chris Hawblitzel, Heng Huang, Lea Wittie, and Juan Chen.
A Garbage-Collecting Typed Assembly Language.
In Microsoft Technical Report TR-2006-169. (Gctal)
- Lea Wittie.
Type-Safe Operating System Abstractions, Ph.D. Thesis. In
Dartmouth Technical Report TR2004-526. (Lambda-concurrent)
- Chris Hawblitzel, Heng Huang, and Lea Wittie.
Composing a well-typed region.
In Dartmouth Technical Report TR2004-521.
- Heng Huang, Lea Wittie, and Chris Hawblitzel.
Formal Properties of Linear Memory Types.
In Dartmouth Technical Report TR2003-468. (Lambda-low)
Presentations
- "Generating a Statically-Checkable Device Driver I/O Interface",
APGES, Austria, October 2007.
- "Laddie: Language for Automated Device Drivers", PL Seminar,
Harvard University, May 2007.
- "Laddie: Language for Automated Device Drivers", Poster at
CRA-W, PL conference, Austin TX, May 2007.
-
Laddie: Language for Automated Device Drivers, NEPLS, April 2007.
-
Type-Safe Operating System Abstractions, Thesis Defense,
Dartmouth College, Hanover NH, June 2004.
- Sailing the C of Safer Languages, Job Talk, Spring 2004.
- A Type-Safe OS Kernel,
Thesis Proposal, Dartmouth College, Hanover NH, July 2002.
Links
Online Journals:
|
