Enforcing high-level protocols in low-level software

TLDR

Infrastructure software reliability is often compromised by resource mismanagement, but the Vault language lets programmers specify resource‑management protocols that the compiler can statically enforce. We validate the utility of our approach by enforcing protocols present in the interface between the Windows 2000 kernel and its device drivers. Vault enforces protocols by statically checking that operations occur in a specified order, that prerequisites are met before data access, and that resources cannot be leaked.

Abstract

The reliability of infrastructure software, such as operating systems and web servers, is often hampered by the mismanagement of resources, such as memory and network connections. The Vault programming language allows a programmer to describe resource management protocols that the compiler can statically enforce. Such a protocol can specify that operations must be performed in a certain order and that certain operations must be performed before accessing a given data object. Furthermore, Vault enforces statically that resources cannot be leaked. We validate the utility of our approach by enforcing protocols present in the interface between the Windows 2000 kernel and its device drivers.