Toward a Taxonomy of Typestate Systems: Soundness Without Alias Information

Abstract

External third-party APIs are commonly used in real-world programming. Specifications or protocols are given by the designer to direct the usage of those APIs combined. The violation of specifications may crash the program, or weaken or break the guarantees of the framework, which would be vital to some safety-critical systems such as encryption.

Typestate system is one of the approaches to check the valid use of APIs based on a given protocol. However, the soundness of the general typestate system relies on the soundness of external alias information. Obtaining whole-program alias information is often expensive and inefficient. One way to remove this dependency is to restrict the protocols. This work tries to examine the class of protocols that can be soundly checked without alias information. We formalize the notion of the protocol and the typestate system, from where we further construct some special classes of protocols. We identify the group of typestate systems called the accumulative typestate system, which is a superset of typestate systems that can be checked soundly without alias information. We also pin down two groups of accumulative typestate systems that are actually sound without alias information.