学海网 文档下载 文档下载导航
设为首页 | 加入收藏
搜索 请输入内容:  
 导航当前位置: 文档下载 > 所有分类 > A bisimulation for dynamic sealing

A bisimulation for dynamic sealing

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.

第1页

TOP相关主题

我要评论

相关文档

    站点地图 | 文档上传 | 侵权投诉 | 手机版
    新浪认证  诚信网站  绿色网站  可信网站   非经营性网站备案
    本站所有资源均来自互联网,本站只负责收集和整理,均不承担任何法律责任,如有侵权等其它行为请联系我们.
    文档下载 Copyright 2013 doc.xuehai.net All Rights Reserved.  email
    返回顶部