Coping with the reality: adding crucial features to a typestate-oriented language

Abstract

Detecting programming errors and vulnerabilities in software is increasingly important, and building tools that help with this task is an area of investigation, crucial for the industry these days. When programming in an object-oriented language, one naturally defines stateful objects that are non-uniform, i.e., their methods’ availability depends on their internal state. One might represent their intended usage protocol with an au- tomaton or a state machine. Behavioral types allow to statically check if all the code of a program respects the usage protocol of each object. In this thesis we present a tool that extends Java with typestate definitions. These typestates are associated with Java classes and define the behavior of instances of those classes, specifying the sequences of method calls allowed. This tool checks statically that method calls happen in order, following the specified behavior. The tool was implemented in Kotlin as a plugin for the Checker Framework. It is a new implementation of the Mungo tool and supports prevention of null pointer errors, state transitions depending on return values, assurance of protocol completion, drop- pable states, and association of protocols with classes from the standard Java library or from third-party libraries. Additionally, the tool integrates behavioral types with ac- cess permissions, allowing objects to be shared in a controlled way using a language of assertions. This language of assertions supports concepts like packing and unpacking, including unpacking of aliases objects, and transferring of permissions between aliases. To relieve the programmer from manually writing all the necessary assertions, the tool implements an inference algorithm which analyzes the code statically and, given the uses of objects, constructs all the required assertions.