Modern computers rely on the correctness and security of low-level systems, such as garbage collectors, device drivers, embedded system code. Often, a small amount of low-level code (say, in a firewall, a network interface device driver, or secure coprocessor) is all that stands between a computer system and a hacker trying to break into the system. Even in the absence of malicious outsiders, buggy device drivers often cause annoying system crashes. Given their role as the foundation for higher-level services, one might expect low-level systems to benefit from the static and run-time checks provided by type-safe languages. However, systems programmers usually lean towards assembly language, C, or C++ rather than Java, ML, or Haskell, because they need efficient low-level control of memory. Java's array bounds checking, for example, prevents the buffer overflow attacks that so many C programs are susceptible to, but often imposes extra run-time overhead. Automatic garbage collection prevents dangling pointers, but implementing a garbage collector requires the ability to explicitly free heap objects, a privilege not usually granted to safe language programs. We have implemented a low-level, type-safe language called ``Clay'' that is powerful enough to express programs that could previously only be written in unsafe languages. It includes sophisticated type system support for safe memory deallocation and array bounds check elimination.
We demonstrated Clay's utility by writing an efficient Cheney-queue copying collector and a mark-sweep collector in the language, and we used the insights from these collectors to develop a new type-theoretic foundation for regions, based on linear memory types. We also used Clay to write safe operating system code that interacts directly with low-level entities, such as devices and interrupts. For example, our ethernet driver reads and writes directly to the registers on an ethernet card, but Clay's type system prevents illegal operations, such as writing to a non-existent register, writing to a register without first establishing the correct register window, accessing the device without holding the proper lock, or overflowing a queue.