Enforcing High-Level Protocols in Low-Level Software

Abstract

The reliability of infrastructure software, such as operating sys-tems 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 stati-cally 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. 1.