Confinement framework for encapsulating objects

Confinement is used to prohibit safety-critical objects from unintended access. Approaches for specifying and verifying confinement have been proposed in the last twenty years but their application has been help back. We develop a novel framework for specifying and verifying object confinement in ob...

Full description

Saved in:
Bibliographic Details
Published in:Frontiers of Computer Science 2013-04, Vol.7 (2), p.236-256
Main Authors: SHU, Qin, QIU, Zongyan, WANG, Shuling
Format: Article
Language:English
Subjects:
aliasing
Computer Science
Confinement
object-oriented
ownership
Research Article
Safety critical
type system
well-confined program
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Confinement is used to prohibit safety-critical objects from unintended access. Approaches for specifying and verifying confinement have been proposed in the last twenty years but their application has been help back. We develop a novel framework for specifying and verifying object confinement in object-oriented (OO) programs. Instead of expressing the confinement requirements within a class for possible future usage, as with ownership types, we specify confinement requirements of the class in its usage class which actually intends to confine the parts, i.e., internal representations. Syntactically, an optional conf clause is introduced in class declarations for annotating the confined attribute-paths. A "same type and confinement" notation is introduced for expressing type and confinement dependence among variables, parameters, and return values of methods. Based on the extension to a Java-like language and existing techniques of alias analysis, we define a sound type-system for checking the wellconfinedness of OO programswith respect to the confinement specifications.
ISSN:2095-2228
2095-2236
DOI:10.1007/s11704-013-1259-7