基于类型的移动计算安全性与活性的π演算应用及其挑战

理论计算机科学电子笔记162（2006）333-340www.elsevier.com/locate/entcs基于类型的移动计算安全完整性、安全性和活性吉田伸子英国伦敦帝国理工学院计算机系摘要本文概述了一个想法，如何挑战集中在代码移动性的三个安全问题，通过发展的π演算和高阶π演算的类型的一般理论，以及如何将其应用于设计安全的并发和分布式编程语言。关键词：进程演算，类型，移动计算，安全和π演算1背景如今，移动代码的使用在整个计算场景中非常普遍，从公司的内部网络应用程序到将活动网络中的代码迁移到万维网中的动态内容，再到电话应用程序[51，36，43]。移动代码的主要好处之一（如Java和Java中所见）是允许可扩展性[12，50]，其中一段代码从源节点迁移到目标节点并链接到目标的运行时环境，以达到其目的。这样的可扩展性导致新功能的丰富库，包括不受网络带宽/延迟限制的远程计算资源的动态、紧密耦合的使用、其中与资源的实时交互是必不可少的多媒体应用、以及增量软件/服务添加/更新。移动计算的这种开放特性对软件安全提出了新的挑战：需要基础设施来管理安全机制，通过该机制，具有不同起源和功能的代码片段，体现不同的原则，可以在移动性和动态链接的情况下安全地交互。本文展示了我们如何开发基本技术来解决这些安全问题，1电子邮件地址：yoshida@doc.ic.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.115334N. Yoshida/Electronic Notes in Theoretical Computer Science 162（2006）333移动程序使用定义良好的数学模型，即类型化的移动过程，并将其应用于编程语言学科的建立[2，51]。本文的建议部分涉及到作者的EPSRC高级奖学金的主题。在下文中，我们首先讨论三个主要问题以及我们如何实现其目标。1.1移动计算让我们假设一个简单的电子商务移动代理，作为一个客户，通过不同的网站在互联网上移动，以执行商业交易。代理可以配备有购买列表和代表其所有者的订单作为其脚本（程序），并执行与虚拟商店的复杂交互。它还可能根据商品价格等因素改变其行为。然后，在代理商（客户）和商店（主机）之间的交互过程中出现了三个主要问题• 代理可能会危及主机的完整性;例如，代理可能会删除或修改敏感信息，例如商店的销售帐户• 代理可能侵犯主机的隐私或保密性;例如，代理可能将存储在主机处的信用卡号传送到公共信道。• 代理可能会干扰服务的可用性或活跃性[45];例如，在初始交互之后，代理可能不会返回确认，从而进入无限循环。然后主机无法继续进行（这是一种所谓的拒绝服务攻击）。请注意，双重地，代理可以从恶意或错误的主机引起的相同种类的威胁提供支持。本文概述了作者1.2基于类型的安全方法及存在的技术问题在20世纪90年代，大多数新软件都是用C、C++和Java等语言编写的在当前的应用程序中，类型系统保证的主要属性仍然是非常简单的类型可靠性：“良好类型的程序不会出错”，例如，如果整数被类型化为字符串，违反类型可靠性构成了真正的安全威胁，许多研究人员已经证明C和Java子集的类型可靠性可以检测到这样的威胁，例如。[7、11、33]。然而，从技术上讲，三个安全问题，数据的完整性，隐私和活性，并不容易通过简单的类型安全来保证;例如，在Java和C#的当前安全架构中，基本的类型检查在执行之前完成，但访问控制是以受限和临时的方式动态完成的，其结果对于大多数程序员来说是难以预测甚至解释的[8]。在这种背景下，一个尚未解决的紧迫问题然而，令人满意的是静态的，特别是基于类型的验证，N. Yoshida/Electronic Notes in Theoretical Computer Science 162（2006）333335用于简单类型安全。在研究层面上，顺序和函数程序中的静态类型系统已经成功地用于保证程序的终止，用于控制特权和能力（例如[41，8]），以及用于推理程序的信息流（例如[9]）。在这种情况下，最近的一个成功的研究开发是证明携带代码（PCC）的商业成就[40，14]，它静态地确保了移动代码的安全性。 重要的一点是，这种方法是由语义和类型支持的- Hoare逻辑作为一种规范逻辑和类型λ-演算（爱丁堡逻辑框架（LF）的变体[15]）用于表示移动代码的证书和正式检查不可信代码。这个框架打开了一个广泛的可能性，使用一个正式的foundation- tion控制代码的流动性，通过静态检查。另一方面，当前版本的PCC [14]不能将分布式、并发或非确定性程序作为可转移代码来处理。事实上，缺乏类型化、逻辑和语义的正式基础，甚至无法表达（更不用说证明）移动程序的所需安全属性，当它们包括非确定性、通信、并发和分布，与顺序程序相反。 作为另一个前-例如，由强规范化保证的资源保护是SwitchWare项目基于简单类型的λ-演算为主动网络开发其类型化编程语言（ActiveNetworks）[42]的主要原因之一。Jif [34]为Java的一个主要子集设计了一个保密类型规程，并研究了它在可能不受信任的主机上的实现。目前，合并的并发性，通信和程序分布还没有考虑在这些语言中，即使这些元素是现代软件必不可少的。从这些观察中，我们有以下问题：• 我们能否构建一个静态类型系统，超越简单的类型安全，将函数类型和顺序类型的累积理论扩展到移动进程？• 我们能不能使用不同的过程来设计安全的移动语言？• 我们能否将进程演算的理论应用于这一领域的实际应用？我们试图通过证明类型化移动进程的一般语义理论在实践中的有效性，对上述问题给出一个肯定的回答。该技术方案建立在访问控制的移动性[59，56，17]，保密性[27，60，22，29]和类型理论的活性和线性通信[4，3，57，30，37，18，54，30，10]的最新进展。2移动进程而不是使用特定的编程语言，主要的研究集中在π演算及其高阶扩展（称为HOπ演算[44，35，59]）。这有两个基本原因。首先，π演算可以忠实地嵌入主要的编程语言构造使用其单一的通信原语，名称传递。此外，当配备与游戏336N. Yoshida/Electronic Notes in Theoretical Computer Science 162（2006）333语义[1，32，26]，这些嵌入可以精确地捕获源语言的语义而不会丢失信息。我们已经获得了可表示性的关键结果，完全抽象的嵌入（直观地说，当将程序表示为π演算时，没有信息丢失）用于广泛的编程语言类领域：包括PCF [ 3 ]，具有求和和乘积类型的强规范化λ演算[ 57]，多态性[4]和控制[30]。此功能对于保密性分析特别有用。其次，HOπ-演算用参数化进程传递表示了程序移动性的一般形式通过在[59，56]中引入的类型结构，它可以表示现实计算中的各种安全问题。上述嵌入的忠实性也将推广到HOπ-演算。这些观察表明，通过使用这些形式主义开发高级类型系统，我们可以获得一种通用技术，该技术直接适用于各种语言，继承了并发理论和函数式和顺序式语言中类型规则研究的积累技术。自π演算研究的早期阶段以来，研究人员开发了一个框架，其中函数和过程可以统一推理。特别是，嵌入是关键：例如，从异步π-演算中λ-演算的新编码开始，我们可以形式化可以执行最佳约简的λ-演算[53];我们建立了异步π-演算的组合子理论[24，25]，可用于解释移动进程的表达性[55];我们通过将按值调用λ-演算编码到π-演算中发现了完全抽象的按值调用游戏语义[26]。最近从线性类型过程的Hennessy-Milner逻辑[16][19]，我们建立了具有一般别名的命令高阶函数的Hoare逻辑[28，5，31]，解决了Cartwright-Oppen和Moriss 25年前的一个开放问题这种逻辑可以推理出很难用现有的类霍尔逻辑验证的程序示例。3基于类型的方法和应用我们的目标是扩展HOπ的细粒度类型系统，不仅处理访问控制，而且处理移动程序中的保密性和活性，并最终将其用作设计安全移动系统语言的基础。下面列出了从基于类型的方法获得的可行性和最近的两个应用访问控制：在[59]中，我们提出了一个新的HOπ-演算类型系统，它可以确保资源的访问控制。在这个分类系统中，进程可以根据其预期用途被分配不同的类型。这不同于以前的工作类型的移动进程，其中所有的进程是由一个唯一的常数类型。此外，我最近发现了新的表达性存在和依赖类型，通过这些类型，[59]的原始可类型性被显着扩大[56]。由此产生的细粒度类型便于访问权限的管理，并提供主机保护，防止潜在的恶意移动代码。N. Yoshida/Electronic Notes in Theoretical Computer Science 162（2006）333337活性：在[57]中，我们提出了一个线性类型系统，可以保证π演算的强规范化（SN）。在[60]中，我们还研究了它对方程理论（互模拟）的影响因此，类型规则确保了活性属性的基本形式（参见。[45]）在指定的输出动作最终发生的地方。形式主义是足够一般的代表强正规化λ-演算是完全抽象的（这在实践中意味着可以表示远程过程调用的非平凡形式）。Secretary：在[27，22]中，我们提出了一个类型系统，其中安全的信息流是由静态类型检查来保证的这个打字系统被用作一种工具，Volpano和Smith的安全多线程命令式演算的编程语言分析[48]。我们的结果被Smith [47]用来扩大原始命令式语言的可类型性[48]。应用：第一个例子是形式化分布式Java的语义，精确地捕获多态分布式应用中的RMI和类加载活动[2]。我们使用HOπ演算来设计新的显式码移动性原语以及分布式对象运行时的表示此外，它已被用于验证Kelly等人的Java RMI聚合优化实现的正确性在20世纪80年代早期，分布式面向对象语言的设计者提出了同样的优化思想，但当时没有给出正确性的证明。π演算[23]的行为等价技术可以在25年后应用于它第二个例子是建立一个Web Services语言的高级类型系统：线性和会话类型正在适应Web服务编排描述语言（WS-CDL）的W3C官方标准化[51]，作者一直作为Robin Milner和Kohei Honda的特邀专家工作。4移动代码安全的综合框架为了实现这一目标，我们从三个不同的层面（基础语言、移动性和应用）来解决这些问题。对于基本语言和移动性，我们使用π-演算[38，20]和高阶π-演算[44，35，59]。对于应用程序级别，我们使用两种不同的形式：一种是Java的子集[11，33，6]，扩展了分布[2]，另一种是WS-CDL的核心语言[51]。（HO）π-计算程序的通用性是一个本质的问题，它对语言程序的使用，通过设置，可适用于个别的实用语言.具体而言，该任务分为以下三个线程：（基础语言级）建立了一个完整的π演算类型系统框架，该框架可以完全抽象地嵌入赋值、过程调用、多态、控件和对象等的框架应该特别捕获基本的活性属性，并通过保密性来增强。338N. Yoshida/Electronic Notes in Theoretical Computer Science 162（2006）333（移动水平）通过进一步扩展高阶π演算（HOπ演算）的类型系统，开发高阶π演算（HOπ演算）的基本类型系统-在[59]中引入，以研究更高级的访问控制和位置原语[17]。然后，我们合并它，以确保基于基础语言级别的结果的秘密性和活性，获得一个强大的类型化元语言的源代码的移动性。（应用层）在移动层类型化系统的基础上，设计了一个具有显式代码移动原语的多线程Java子集[2]及其类型化系统，该类型化系统能保证三个安全问题我们也设计WS-CDL的核心集[51]，并将其扩展为包含代码移动性原语。我们证明了他们的正确性（安全性）通过完全抽象的翻译成HOπ-演算。为了在PCC [40，14]的框架中使用，我们还计划构建自动验证工具，基于Hoare逻辑，用于具有一般别名的命令式高阶函数[28，5，31]。引用[1] Abramsky，S.，雅加迪桑河和Malacaria，P.，PCF的完整抽象，1994年。Info. &163（2000），409-470中所述。[2] A. Ahern和N. Yoshida，Formalising Java RMI with Explicit Code Mobility，OOSLA '05，第20届ACM SIGPLAN面向对象编程、系统、语言和应用会议，第403-422页，2005年10月。完整版本可查阅www.doc.ic.ac.uk/dcbl.html，伦敦帝国理工学院计算技术报告系，2005/01，2005年。[3] 伯杰，M.，Honda，K.和Yoshida，N.，序贯性与π演算，TLCA 01，LNCS 2044，pp.29[4] 伯 杰 ， M.， Honda， K.和 Yoshida ， N.， 通 用 性 和 π-演 算 ， FoSSaCs'03 ， LNCS ， Springer-Verlag ，2003。完整版本将发表在Journal of ACM Acta Informatica，ACM，2005年。[5] 伯杰，M.，Honda，K.和Yoshida，N.，逻辑分析在强制高阶函数中的别名，ICFP[6] Bierman，G.M.，帕金森，M.J和皮茨，A. M.，MJ：An Imperative Core Calculus for Java and Javawith Effect，UCAM-CL-TR-563，Cambridge，2003.[7] 王艳玲，陈文辉，陈文辉[8] 福尔内角和戈登，A.D.，堆栈检测：理论和变体，POPL，ACM，2002年。[9] Denning，D.和Denning，P.，安全信息流程序认证。ACM通讯，ACM，20：504[10] M. Dezani-Ciancaglini，N. Yoshida，A. Ahern和S. Drossopoulou，一种具有会话类型的分布式面向对象语言，可信全球计算国际研讨会，出现在Proc. TGC，计算机科学讲义，Springer-Verlag，2005年。[11]SLURP项目，伦敦帝国理工学院计算系http://binarylord.com/slurp/网站。[12] 格里姆河和Bershad ，B.，可扩展系统中访问控制策略、实施和功能的分离。在Comp.系统：19（1），2月，36[13] 同性恋，美国， 一框架为 的 形式化 的 π演算类型系统在伊莎贝尔/霍尔，Proc. TPHOLs01，Springer，LNCS，2001年。[14] Fox Project，http：：/www-2.cs.cmu.edu/www.example.com[15] 哈珀河，Honsell，F.，和Plotkin，G.，A framework for defining logics，Journal of the Association forComputing Machinery40（1），143N. Yoshida/Electronic Notes in Theoretical Computer Science 162（2006）333339[16] Hennessy，M. Milner，R.，非确定性和并发性的代数律，J. ACM 32（1），pp.137[17] Hennessy，M.，Rathke，J.和Yoshida，N.，SafeDpi：a language for controlling mobile code，FoSSaCs[18] 本田，K.，作曲过程，POPL[19] 本田，K.，从过程逻辑到程序逻辑，ICFP[20] Honda，K.和Tokoro，M.，异步通信的对象演算。ECOOP[21] 本田康平Vasconcelos和Makoto Kubo，基于结构化通信的编程语言原语和类型规则，ESOP[22] 本田，K.， Vasconcelos，V.和Yoshida，N，Secure Information Flow as Typed Process Behaviour，ESOP[23] Honda，K.和Yoshida，N.，基于约简的过程语义。FSTTCS373-387，Springer-Verlag，1993年12月。完整版本出现在TCS，pp. 437 -[24] Honda，K.和Yoshida，N.，移动过程的组合表示，POPL[25] Honda，K.和Yoshida，N.，陈文辉，“计算机软件的理论与应用”，第二届计算机软件学术会议论文集，第789期，第786 -805页，1994年4月[26] Honda，K.和Yoshida，N.按值调用计算的博弈论分析。TCS，221（1999），393[27] Honda，K.和Yoshida，N.，一种用于安全信息流的统一类型结构，POPL[28] 洪晓平，杨明，一种基于多形性高阶函数的复合程序逻辑，2004年第六届声明式程序设计原理与实践国际会议论文集，[29] Honda，K.和Yoshida，N.，通过流分析实现无干扰，58页，函数编程杂志，CPU，2005年3月。[30] 本田，K.，Yoshida，N.和Berger，M.，《π-演算中的控制》，Proc. CW'04，ACM出版社，2004年。[31] 本田，K.，Yoshida，N.和Berger，M.，An Observationally Complete Program Logic for ImperativeHigher-Order Functions，LICS[32] Hyland，M.和Ong，L.，“On Full Abstraction for PCF”：I，II and III. Info. &Comp.163（2000），285-408.[33] Igarashi，A.，皮尔斯湾和Wadler，P.，Featherweight Java：A Minimal Core Calculus for Java andGJ.TOPLAS，23（3）：396-450，May 2001.[34] Jif（Java+信息流）项目，http://www.cs.cornell.edu/jif/[35] Je Escherey，A.和Rathke，J.，高阶π演算的上下文等价性再访，MFPS XIX，蒙特利尔2003。[36] Knapik，M.和Johnson，J.，开发分布式系统的智能代理，McGraw Hill，1998年。[37] Kobayashi，N.，Pierce，B.，和Turner，D.，Linear types and π-calculus，POPL'96，358-371，1996.[38] 米尔纳河，Parrow，J.G.沃克，DJ移动过程的演算。信息与计算，100（1），第1 -77页[39] Sabelfeld，A. Meyers，A.基于网络的信息流安全，IEEE Journal on Selected Areas in Communications，21（1），2003年1月。[40] Necula，G.，携带证明代码。POPL[41] Pottier，F.，斯卡尔卡角史密斯，S。访问控制的系统方法。ESOP 01，LNCS 30340N. Yoshida/Electronic Notes in Theoretical Computer Science 162（2006）333[42] 主动网络的分组语言，SwitchWare项目，http://www.cis.upenn.edu/www.example.com.[43] RIFML，反应式智能框架，Enigmatec Corporation Ltd，http://www.enigmatec.net/网站。[44] Sangiorgi，D.，在进程代数中表达迁移：一阶和高阶范式。博士论文，爱丁堡大学，1992年。[45] Schneier，F，On Concurrent Programming，Springer，1997。[46] 瓦斯孔塞洛斯河谷和本田，K.，多元π-演算的主类型化方案。CONCUR[47] 史密斯，G.，一种新型的安全信息流系统，CSFW[48] 史密斯，G。和Volpano，D.，多线程命令式语言中的安全信息流，第355 - 364页[49] VerifiCard，欧洲Smard卡验证项目，http://www.verificard.org。[50] Wallach，D.S等人，Java的可扩展安全架构。SOSP，116[51] 编舞描述语言，W3-CDL，Web服务编舞工作组，http://www.w3.org/2002/ws/chor/网站。[52] Kwok Yeung和Paul Kelly，通过通信重构优化Java RMI程序，Middleware[53] Yoshida，N.，张文龙，张文龙，张文龙，1993.[54] Yoshida，N.，一元移动过程的图类型，FST/TCS371-386，Springer-Verlag，1996。完整版本为LFCS技术报告，LECS-LFCS-96-350，1996年。[55] Yoshida ， N. ， MinimalityandSeparationResultsonAsynchronousMobileProcesses ：Representability Theorems by Concurrent Combinators ， Journal of Theoretical ComputerScience，第274卷，第1期，2002年3月6日，第231-276页[56] Yoshida，N.，通道依赖类型的高阶移动过程，POPL[57] Yoshida，N.，Berger，M.和本田，K.，π-演算中的强正规化，Proc. LICS '01，pp.311-322，IEEE，2001。完整版本发表在Journal of Information and Computation，191（2004）145[58] 吉田， N. 和 轩尼诗， M.， 分型 和局部性 在 分布式更高 订单流程。Proc. CONCUR[59] Yoshida，N.和Hennessy，M.，将类型转换为进程、信息和amp;.Comp，174（2），pp. 143-179，学术出版社，2002年。Proc. LICS[60] Yoshida，N.，Honda，K.和Berger，M.，线性和互模拟，Proc. FoSSaCs