Deputy: Dependent Types for Safe Systems Software

Programming language tools offer powerful mechanisms for improving the safety and reliability of systems code. This talk presents Deputy, a type system and compiler for enforcing type and memory safety in real-world C programs such as Linux device drivers and the Linux kernel itself. Deputy’s type system uses dependent types, a language mechanism that allows programmers to describe common C idioms in an intuitive fashion.

The Deputy project offers contributions to both systems and programming languages. From a systems perspective, Deputy is attractive because it can provide fine-grained safety guarantees in a modular and incremental fashion; for example, Deputy can be used to enforce type and memory safety in Linux device drivers without requiring changes to the kernel. The SafeDrive recovery system for Linux device drivers uses Deputy for isolation and failure detection, and as a result, it is both simpler and faster than previous systems for isolating software extensions. From a language perspective, Deputy shows how to reason about dependent types in imperative code. Deputy has fewer restrictions on mutation than previous systems, and it uses run-time checks and several inference techniques to ensure decidability and usability.