SHF: SMALL: Practical Linear Types for Safe Protocols

University Of Pennsylvania, Philadelphia PA

Investigators

Abstract

Software errors frequently arise because a component of the program does not correctly follow a well-defined protocol for accessing some stateful resource. Common examples include programs that misuse resource handles provided by the operating system, incorrectly deallocate the same memory or other resource multiple times, or fail to properly sequence calls to a complex program module. Such protocol violations lead to software crashes or unintended behavior, potentially with disastrous consequences. The project objective is to develop programming language technology to allows software developers to conveniently describe protocols over stateful resources. This technology will uncover such bugs at design time by statically checking whether the program is appropriately following the desired protocols, thereby ruling out the wide class of software flaws. The new language mechanisms will be general purpose, practical, and suitable for use in a wide variety of applications ranging from memory management to traditional protocol implementation. The researchers will create a compiler infrastructure prototype and establish the correctness of the approach by a machine-checked proof of type soundness. The primary broader impact of the project is the development of technology to help eliminate such programming errors early in the software-design life cycle to decrease the cost of building correct, reliable software.