A Generic Model for Confinement and its Application

摘要

Confinement of objects is crucial to protect sensitive object references. However, static confinement schemes proposed so far have quite rigorous syntactic restrictions, and also, no similarity in concepts makes assessing of them a difficulty. In this paper, we present a generic framework for reasoning about confinement based on three parts: program states, partition for heaps and the confinement constraints. Particularly, the partition is made according to the system's requirement, whose flexibility leads to the generality of the model. A range of confinement schemes can be characterized in terms of their underlying partition for the heap in our model. As an illustration, we have encoded both confined types and ownership types, and proved the soundness of their type systems in our model that well typed programs are well confined under our formal definition.