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 systems 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.
Shuling Wang Zongyan Qiu
LMAM and Department of Informatics School of Mathematical Sciences, Peking University
国际会议
南京
英文
57-64
2008-06-17（万方平台首次上网日期，不代表论文的发表时间）