We define λseal, an untyped call-by-value λ-calculus with primitives for protecting abstract data by sealing, and develop a bisimulation proof method that is sound and complete with respect to contextual equivalence. This provides a formal basis for reas
A Bisimulation for Dynamic Sealing
EIJIRO SUMII and BENJAMIN C.PIERCE
University of Pennsylvania
We defineλseal,an untyped call-by-valueλ-calculus with primitives for protecting abstract data by sealing,and develop a bisimulation proof method that is sound and complete with respect to contextual equivalence.This provides a formal basis for reasoning about data abstraction in open, dynamic settings where static techniques such as type abstraction and logical relations are not applicable.
Categories and Subject Descriptors: D.3.3[Programming Languages]:Language Constructs and Features—abstract data types;D.3.1[Programming Languages]:Formal Definitions and Theory;F.3[Theory of Computation]:Logics and Meanings of Programs;E.3[Data]:Data Encryption;C.2.2[Computer-Communication Networks]:Network Protocols—protocol ver-ification
General Terms:Theory,Languages,Security
1.INTRODUCTION
1.1Dynamic sealing:Birth,death,and rebirth
Sealing is a linguistic mechanism for protecting abstract data.As originally pro-posed by Morris[Morris Jr.1973a;1973b],it consists of three constructs:seal creation,sealing,and unsealing.A fresh seal is created for each module that de-fines abstract data.Data is sealed when it is passed out of the module,so that it cannot be inspected or modified by outsiders who do not know the seal;the data is unsealed again when it comes back into the module,so that it can be manipulated concretely.Data abstraction is preserved as long as the seal is kept local to the module.
Originally,sealing was a dynamic mechanism.Morris also proposed a static variant[Morris Jr.1973b],in which the creation and use of seals at module bound-aries follow a restricted pattern that can be verified by the compiler,removing the need for run-time sealing and unsealing.Other researchers found that a similar effect could be obtained by enriching a static type system with mechanisms for type abstraction(see CLU[Liskov1993],for example).Type abstraction became the primary method for achieving data abstraction in languages from CLU to the present day.It is also well understood via the theory of existential types[Mitchell and Plotkin1988].
Recently,however,as programming languages and the environments in which they operate become more and more open—e.g.,addressing issues of persistence and distribution—dynamic sealing is being rediscovered.For example,Rossberg[Ross-berg2003]proposes to use a form of dynamic sealing to allow type abstraction to coexist with dynamic typing;Leifer et al.[Leifer et al.2003]use hashes of im-Author’s address:Eijiro Sumii,Department of Computer Science,University of Pennsylvania, 3330Walnut Street,Philadelphia,PA19104-6389.
Manuscript,December2003.
我要评论