LAPS : A General Framework for Modeling Alias Management Using Access Permission Sets

This thesis presents a general model of access control. It uses a simple notion of an access permission token, which gives permission to reference an associated object. Sets of permission tokens are used to model the maximum reach of an object, and reasoning about access to groups of objects. Links between sets are used to model propagation. Restricting access to an object is important for example when dealing with aliasing, multiple references to a single object. Aliasing is ubiquitous in object-oriented programming, and while practical and even necessary for many purposes, it is also a common source of errors. Since an aliased object may change at any time without notice to the other holders of references to that object, one can generally not guarantee that the state observed through a reference will be the same the next time it is observed. Many techniques for alias control, such as uniqueness and ownership types, have been proposed and implemented to limit and prevent the problems potentially caused by aliasing. However, they are often formulated in very specific settings, making formal comparison between different techniques difficult. This thesis presents a general framework that allows several common alias management policies to be implemented using the same mechanisms, allowing for easy comparison and unification of existing systems, as well as reasoning about new systems. The framework is formally implemented as LAPS, a small object-oriented language that uses access permission sets to express the aliasing policies of a program. Alias management concepts from several existing languages are translated into LAPS, showing how it can be used as a common platform for reasoning about access control properties of different systems