PLURAL: Checking Protocol Compliance under Aliasing

摘要

Enforcing compliance to API usage protocols is notoriously haxd due to possible aliasing of objects through multiple references. In previous work we proposed a sound, modular approach to checking protocol compliance based on types-tates that offers a great deal of flexibility in aliasing [1]. In our approach, API protocols are defined based on typestates. Every reference is associated with a permission, and reasoning about permissions is appropriately conservative for the "degree" of possible aliasing admitted by a permission.rnThis paper describes Plural, a tool to automatically enforce typestate-based protocols using permissions in Java. API developers can specify protocols with simple annotations on methods and method parameters. A static flow analysis tracks permissions in code that uses specified APIs and issues warnings for possible protocol violations.