Collaborative Research: SHF: Small: Lightweight Modular Typestate

University Of Washington, Seattle WA

Investigators

Abstract

Software reliability is of critical importance to society, and software verifiers can improve reliability by guaranteeing the absence of certain bugs. In particular, typestate verification prevents important classes of bugs by ensuring programs do not perform certain illegal operation sequences. However, despite over 30 years of research, typestate verification has not been widely adopted by developers. This project will develop techniques for lightweight typestate verification, leveraging new insights on the structure of typestate properties and common programming patterns. The project is expected to make typestate verification significantly easier for programmers to adopt, thereby improving the reliability of large-scale, real-world software systems. A key barrier to adoption of typestate analysis is handling of pointer aliasing, which in extant approaches necessitates either an expensive whole-program analysis or, in modular approaches, heavyweight code annotations. This project will achieve lightweight and modular typestate verification by developing algorithms that leverage typestate system characteristics and common aliasing patterns in modern code bases. For example, the project identifies accumulation typestate systems, in which an object's enabled methods only grow over time. An accumulation typestate system can be verified soundly even in the absence of alias information. The project also studies restricted aliasing patterns arising from modern coding patterns like fluent APIs, which can be precisely analyzed with lightweight, modular techniques. The project will apply these insights both to traditional typestate systems and to new properties that are inconvenient or impossible to express in existing typestate formalisms. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.