Confinement is used to prohibit safety-critical ob- jects from unintended access. Approaches for specifying and verifying confinement have been proposed in the last twenty years but their application has been help bac...Confinement is used to prohibit safety-critical ob- jects 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 confine- ment in object-oriented （00） programs. Instead of expressing the confinement requirements within a class for possible fu- ture usage, as with ownership types, we specify confinement requirements of the class in its usage class which actually in- tends to confine the parts, i.e., internal representations. Syn- tactically, an optional conf clause is introduced in class dec- larations for annotating the confined attribute-paths. A ＂same type and confinement＂ notation is introduced for expressing type and confinement dependence among variables, param- eters, and return values of methods, Based on the extension to a Java-like language and existing techniques of alias anal- ysis, we define a sound type-system for checking the well- confinedness of 00 programs with respect to the confinement specifications.展开更多
文摘Confinement is used to prohibit safety-critical ob- jects 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 confine- ment in object-oriented （00） programs. Instead of expressing the confinement requirements within a class for possible fu- ture usage, as with ownership types, we specify confinement requirements of the class in its usage class which actually in- tends to confine the parts, i.e., internal representations. Syn- tactically, an optional conf clause is introduced in class dec- larations for annotating the confined attribute-paths. A ＂same type and confinement＂ notation is introduced for expressing type and confinement dependence among variables, param- eters, and return values of methods, Based on the extension to a Java-like language and existing techniques of alias anal- ysis, we define a sound type-system for checking the well- confinedness of 00 programs with respect to the confinement specifications.
