基于博弈的计算语义模型及其应用

可在www.sciencedirect.com在线获取理论计算机科学电子笔记286（2012）191-211www.elsevier.com/locate/entcs一种系统级游戏语义丹河吉卡伯明翰大学尼科斯·策韦莱科斯伦敦大学玛丽皇后摘要博弈语义（Game Semantics）是编程语言中的一种类迹指称语义，其中术语的合法可观察行为的概念是通过术语（Proponent）及其上下文（Opponent）之间的博弈规则组合定义的。一般来说，一种语言的计算特性越丰富，语义游戏规则的约束就越少在本文中，我们考虑的后果，这种放宽规则的限制，通过给予对手的omnifirmity，也就是说，允许发挥没有组合限制的任何移动。然而，我们施加了一个认识上的限制，不授予对手全知，使支持者可以有未公开的秘密行动。我们介绍了一种基本的类C语言编程语言，并为它定义了这样一种语义模型。是一个有吸引力的操作和游戏语义的简单组合，我们展示了某些痕迹如何解释系统级攻击，即在编程语言本身之外可实现的似是而非的攻击。 我们还展示了如何允许Proponent有秘密，确保一些可取的等价，编程语言被保留下来。保留字：游戏语义学，全能的对手，无所不知的对手1介绍游戏语义通过解决PCF [2，7]的完全抽象的长期开放问题而变得突出，并且通过用于定义许多其他完全抽象的编程语言模型，巩固了其作为建模编程语言的成功方法的地位博弈语义学的方法是将计算建模为术语与其上下文之间的形式化交互，称为博弈因此，语义游戏有两个参与者：代表术语的支持者（P）和代表上下文的反对者（O）。相互作用被正式地描述为一系列的游戏动作，称为游戏策略，一个术语被相应的策略所模拟，即所有可能的游戏策略的集合为了定义游戏语义，我们需要定义游戏规则是什么，玩家的能力是什么。1571-0661 © 2012 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.08.013192D.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）191对于PCF游戏来说，规则特别整洁，与所谓的“礼貌对话原则”相对应策略的合法性约束可以作为移动序列的组合条件来施加。策略也有一些组合条件，这些组合条件会影响参与者而不是博弈。它们是一致性条件，规定如果在某些策略中P采取某种行动，在其他策略中它也会采取类似的行动。最简单的条件是决定论，它规定，在任何策略中，如果两种打法在某个P移动之前是相等的，那么它们随后的P移动也必须是相同的。放松对策略和策略的一些组合约束，优雅地从PCF模型引导到更具表现力的编程语言模型例如，放松一个名为无罪的条件会导致带有状态的编程语言模型[3]，放松括号会导致带有控制的编程语言模型[10]，而在没有交替的情况下，我们会获得并发语言[6]。贡献在本文中，我们认为会发生什么，如果在一个游戏语义，我们删除组合约束O与传统的博弈模型不同，我们的构造是不对称的：P的行为方式由编程语言及其固有的局限性决定，而O可以表示看似合理的行为，然而，在语言或一些明显的扩展中，这种行为在语法上可能无法实现。 我们将看到这样一个模型，从技术意义上说，格式良好，它所引起的对等概念是有趣和有用的。我们研究这样一个轻松的游戏模型，使用一个理想化的无类型的类C语言。可用移动的概念使用类似于安全协议模型中使用的秘密概念进行建模，正式表示为使用名称。这导致了对手的概念，它是全能的，但不是无所不知的：它可以以任何顺序进行任何可用的移动，但有些移动可以隐藏起来。这类似于Dolev-Yao攻击者的安全模型。我们展示了在这个语义模型中的不等价性如何捕获系统级攻击，即环境系统的行为，虽然不能在语言本身中实现尽管环境系统允许令人惊讶的攻击，我们注意到，许多有趣的等价仍然成立。这提供了证据表明，语义对等的问题可以制定出一个句法上下文的传统框架之外。从技术上讲，该模型是以游戏语义的可操作版本（如Laird的[ 12 ]）表示的D.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）1911932系统级语义2.1语义和操作语义我们介绍一个简单的无类型的类C语言，它的表达能力足以说明基本概念。一个程序是一个模块列表，大致对应于C中的文件。模块是函数或变量声明的列表。导出的变量或函数名是全局可见的，否则其作用域是模块。在扩展的类BNF符号中，我们写：Prog：：= ModHdr：：=导出x;导入x;Mod：：= Hdr DclDcl：：= declx=n; Dcl|decl函数|ϵ头文件Hdr是程序导出和导入的名称列表，x是一个从无穷多个名字的集合N中选取的标识符（或标识符x的列表），n∈Z。与C语言一样，函数只能在全局范围内使用，并且以非curry形式存在：函数：：=x（x）{localx;StmreturnExp;}一个函数有一个名字和一个参数列表。在函数体中，我们有一个局部变量声明列表，后面是一个以return语句结束的语句列表。我们定义语句和表达式如下（n∈Z）。Stm：：= 0 |if（Exp）then {Stm} else {Stm}; Stm |Exp = Exp; Stm| Exp (Exp∗); StmExp：：= Exp * Exp|经验值|Exp（Exp）|（Exp，Exp）|new（）|n |X语句有分支、赋值和函数调用。 为了简单起见，迭代不包括在内，因为我们允许 递 归 调 用 。 表 达 式 是 算 术 和 逻 辑 运 算 符 、 变 量 解 引 用 （ variabledereferencing，简写为REREFERENCE）、配对、变量分配以及整数和变量常量。函数调用可以是表达式或语句。 因为语言是无类型的，所以语句和表达式之间的区别是任意的，只是为了方便而使用。如果decl f（x）{e}是模M中的一个声明，我们定义f @ M = e [x]，解释为“M中f的定义是e，参数为x”。一个框架由下面的语法给出，其中op∈ {=，*，;}，op∈{，−}。t：：= if（Q）then{e}else{e}|Qope|VopQ|操作系统|Qe|v Q| （v，Q）|(v, Q)我们用Q表示框架的我们用Fs表示帧列表的集合，即帧栈。我们用v表示值，定义如下。我们的语义设置是名词集合[5]（见附录A），在多排序的名称N=Nλ NφNκ194D.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）191其中三个分量中的每一个分别是位置名称、函数名称和函数延续名称的可数也就是说，我们的对象可以包含N中的无限多个元素，并且它们带有将名称排列应用于它们的规范概念。对于一个对象x和一个置换π，将π应用于x的结果表示为π·x。我们用a、b等来定义函数名，特别是函数名，我们可以用f等;对于每一个名称集合X，我们分别记λ（X），φ（X）和κ（X）作为它对位置，函数和连续名称的限制.对于任何包含名称的对象x，我们写ν（x）作为它的支集，即所有出现在其中的名字的集合存储被定义为一对具有有限域的部分函数s∈Sto=（Nλ~fn（Z Nλ Nφ））×（Nκ~fnFs× Nκ）存储的第一个组件将整数值（数据），其他位置（指针）或函数名称（指向函数的指针）分配给位置。第二个存储continuations，由系统用来恢复挂起的函数调用。我们将存储s的两个投影记为λ（s），κ（s）。由于符号的滥用，我们可以写s（a）而不是λ（s）（a）或κ（s）（a）。由于名称是排序的，因此这是明确的。s的支集ν（s）是出现在它的定义域或值集中的名字的集合。对于所有的商店s、s和名称集合X，我们使用以下符号：（限制于）在X上定义的s的子存储：sTX ={（a，y）∈s|a∈ X};（RESTRIcT-FROM）s的子存储不定义在X上：s\ X=sT（dom（s）\X）;（UPDATE）更改s中的值：s[a<$→x] ={（a，x）}<$（s\ {a}）;更一般地说： s[s] =s（s\dom（s））;（EXTENSION）s±sifdom（s）dom（s）;（CLOSURE）Cl（s，X）是包含X和所有可达名字的最小名字集从X 通过s以传递封闭的方式，即X C1（s，X），如果（a，y）∈s且a∈Cl（s，X）则ν（y）∈Cl（s，X）.我们将值定 义 为名称、整数或值的元组：v：：=（）|一|n|（v，v）. value（）是元组操作的单位。我们给出了一个语义的语言使用框架堆栈抽象机。将标识符作为名称是很方便的，因为它提供了一种简单的方法来处理指向函数的指针，就像C语言一样。抽象机器的程序配置具有以下形式：中国|P s，t，e，k ∈ N×N×Sto× Fs×Exp× NκN是一组已使用的名称;PN是一组公共名称;s是程序状态;t是一个被称为帧堆栈的帧列表;e是正在计算的表达式;k是一个延续名称，目前将保持不变。1元组是结合的，为了简单起见，我们识别元组直到结合性和单位同构，所以（v，（v，v））=（（v，v），v）=（v，v，v）和（v，（））= v等。1D.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）191195e = v是一个值。中国|P s，t（if（Q）then {e 1} else {e 2}），v，k − → <$N |P ∈ s，t，e1，k ∈，如果v∈Z\{0}中国|P s，t（if（Q）then {e 1}else {e 2}），v，k − → <$N |P = s，t，e 2，k = 0，如果v =0中国|P s，t（Q op e），v，k − → N |P ∈ s，t ∈（v op Q），e，k ∈ op {=，n，;}中国|P s，t（v Q），v ′，k −→ N |P s，t，v ′′，k，v ′′= v v ′中国|P s，t（v;Q），v ′，k −→ N |P s，t，v ′，k中国|P s，t（a =Q），v，k −→ <$N |P s [a <$→ v]，t，（），k中国|P s，t（Q），v，k −→ N |P s，t，s（v），k中国|P s，t（Q; e），local x，k −→ <$N {a}|P ∈ s [a <$→0]，t，e [a/x]，k ∈，如果a/∈ N中国|P <$s，t <$（Q（e）），v，k <$−→ <$N |P s，t（v（Q）），e，k中国|P <$s，t<$（（Q，e）），v，k <$−→ <$N |P s，t（（v，Q）），e，k中国|P <$s，t <$（（v，Q）），v ′，k <$−→ <$N |P s，t，（v，v ′），k中国|Ps，t（f（Q）），v′，k−→<$N|P≠s，t，e[v′/x]，k≠，若f@M=e[x]（F）例e不是标准型。中国|P s，t，if（e）then {e 1} else {e 2}，k − → N |P s，t（if（Q）then {e 1} else {e 2}），e，k中国|P s，t，e op e ′，k −→ N |P ∈ s，t∈（Q op e ′），e，k ∈，如果op ∈ {=，n，;}中国|P ε s，t，ε e，k ε−→ε N |P s，tQ，e，k中国|P s，t，return（e），k − → N |P s，t，e，k中国|P s，t，new（），k −→ <$N <${a}|P ∈ s [a <$→0]，t，a，k <$，若a ∈Nλ\N中国|P s，t，e（e ′），k − → <$N |P s，t（Q（e ′）），e，k中国|P s，t，（e，e ′），k −→ <$N |P s，t（（Q，e ′）），e，kFig. 1. 操作语义抽象机器的变迁是配置集合上的关系它们是通过对e然后t的结构进行标准形式的案例分析来定义的，如图1所示。分支就像在C中一样，用true标识非零值，用false标识零值。二元运算符从左到右进行计算，这也与C语言一样。算术和逻辑运算符（*）具有明显的求值。解引用被给出了通常的求值，注意，为了使规则适用，它暗示v是一个位置和s（v）被定义。局部变量分配使用新的秘密名称扩展%s的域。局部变量是为函数体的作用域在本地新创建的。new（）操作符分配一个秘密的新位置名称，将其初始化为零并返回其位置。return语句被用作函数结束的语法标记，但它没有语义角色。结构规则，如函数应用和元组在按值调用语言中是常见的，即从左到右。函数调用也有一个标准的评估。函数体替换函数调用及其形式参数x以逐点的方式被参数v最后，非标准形式也有标准的从左到右求值。2.2系统语义传统的函数调用规则（F）仅适用于模块中有函数定义的情况。如果用于调用的名称不是已知函数的名称，则正常的操作语义规则不再适用。我们现在扩展我们的语义，使局部未定义函数的调用和返回成为程序和环境系统之间交互的机制。我们称196D.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）191（Ⅲ）（Sys（M）× L ×Prog（M））（）（）（Ⅲ）（Ⅲ）（Ⅲ）中国|Ps，t（f（Q）），v，k−−s−Tλ−（−P−′）→N{k}|P<$$>{k <$}<$s[k<$$> →（t，k）]<$s如果f@M没有定义，k∈/N，P∈=Cl（s，P∈V（v））调用f，v，k′系统级语义（SLS）。给定一个模M，我们将定义其SLS的转移系统记为M。它的状态是SM=SysM<$Prog M，其中Prog M是抽象-Sys M是前一节的机器配置，Sys M是系统配置集，其形式为：|Ps∈ N×N× Sto.SLS是在模块级别定义的，即缺少函数的程序，类似于大多数编程语言中通常被认为是编译单元 过渡关系δ M的SLS对一组标签L{n}进行操作，并且具有以下类型。δ<$M）（Prog<$M）× {λ}×Prog<$M））（Prog<$M）× L ×Sys<$M））L ={（s，callf，v，k）|s∈Sto，κ（s）= ε，f∈ Nλ，k∈ Nκ，v avalue}{（s，retv，k）|s∈Sto，κ（s）= n，k∈ Nκ，v a value}因此，在系统级，程序和系统配置可以交替调用和返回函数，就像P和O在游戏语义对于（X，（s，α）， X <$）∈δ<$M，我们记X−→αX <$，对于（X，X，X）∈δM。在程序和系统之间转移控制时，延续指针确保在返回时可以恢复正确的执行上下文。我们对如何使用延续施加了几个卫生条件。我们区分P-和S-连续名称。前者由程序创建，并存储以备函数返回时使用。后者由系统创建，不存储。这种区别的原因既有技术上的，也有直觉上的。从技术上讲，它将简化证明复合是定义良好的。混合S和P延续不会产生任何有趣的行为：如果P接收到一个它不知道的延续，那么P的抽象机器就不能评估它，这可以被解释为崩溃。但是S总是有足够的机会使执行崩溃，所以允许它似乎没有意思。然而，这在某种意义上是一个设计决策，并且可以允许具有稍微不同属性的替代语义以混杂的方式混合S和P延续第一个新规则，称为程序到系统调用，是：当调用非局部函数时，控制权转移到系统。在游戏语义中，这对应于一个Proponent问题，并且是一个可观察的动作。在此之后，所有可以从存储中的公共名称传递到达的名称也成为公共名称，因此它为系统提供了控制和信息它的可观察性由转换箭头上的标签标记，其中包括：SD.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）191197联系我们|P<$s<$$>−s′−→<$N<$ν（v，s<$）|Pv（v，s）s[s]，f，v，k若s（k）=（f，k），ν（v，s）<$N<$P，λ（v（v））retv，k′联系我们|P<$s<$$>−→<$N<${调用f，v，kS′k}ν（v，s）|P{∗k}<$ν（v，s）<$s[s]，f（Q），v，k∗∗⟩若f@M有定义，则k∈/dom（s），ν（f，v，s）<$N<$P，λ（ν（v））<$ν（s<$），sTλ（P）±s<$中国|Ps，−，v，k−s−Tλ−（−P→′） 联系我们|Pretv，k其中P=Cl（s，Pv（v））call，表示函数被调用，函数名（f），其参数(v) 以及存储代码指针的新鲜延续（k）;该转换还标记存储的可观察部分，因为它使用公知的名称。对应的规则是System-to-Program返回，对应于来自非本地函数的返回。这类似于游戏语义对手答案。在操作上，它对应于S从函数返回。这里要注意的是，在这种情况下，对S能做什么的唯一约束是认识性的，即由它所知道的东西所决定：(i) 它可以返回任何值v，只要它只包含公共名称或新名称（但不包含私有名称）;(ii) 它可以用任何值更新任何公共位置;(iii) 它可以返回到任何（公共）延续kk。然而，存储的私有部分（即具有N\P中的域）不能被S修改。所以S对它能对已知名字做什么和对已知名字做什么没有限制，但它不能猜测私有名字。因此，它不能对它不知道的名字做任何事情。如前所述，对延续的限制只是卫生的。有 两 个 相 反 的 传 输 规 则 System-to-Program call 和 Program-to-System return，对应于程序返回和系统发起函数调用：在S-P调用的情况下，是S从模块中调用一个公共命名的函数。与返回的情况一样，唯一的约束是函数f、参数v和状态更新s_n仅涉及公共或新鲜名称。由于已经解释的原因，延续上的卫生条件强制不存储延续名称。最后，P-S返回表示程序在函数调用之后向系统产生最终结果的操作。在构造返回值时使用的名称将被公开，存储的公共部分将被观察。与游戏语义类似，函数返回是Proponent答案，而系统调用是Opponent问题。198D.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）191MM（Ⅲ）∼对于任何模M，M∈：M·M）=（M）（M）。¢∗τ∗我们称之为功能组合。模块M的SLS的初始配置为S0 =1000N0|P00。它包含一个stores0，其中所有变量都被初始化为声明中指定的值。集合N0包含所有导出和导入的名称，所有声明的变量和函数.集合P0包含所有导出和导入的名称。当M在上下文中不清楚时，我们可以写P 对于P0，等等。3组合性模块M的SLS给了我们一个解释M，它是模块化的和有效的（即它可以被执行），所以在基于模块的SLS来制定模块的属性时不需要考虑上下文。从技术上讲，我们可以使用转换系统的标准工具来推理SLS，例如迹等价，互模拟或Hennessy-Milner逻辑。我们首先证明了SLS是一致的，通过证明一个组合性的prop-brief。 模块的SLS解释可以以与句法组合一致的方式在语义上组合。模块的语法组合是与未导出的函数和变量名称的重命名连接以防止冲突，我们将使用− · −表示。特别地，我们证明了我们可以定义一个语义SLS复合，使得对于存在τ-转换（= τ）的同构的适当概念，以下成立。设P在程序配置上变化，S在系统配置上变化。更进一步，假设一个扩展的约束名集合Nκn=NκNaux，其中Naux是一个可数无限的新辅助名集合如图2所示，我们归纳地定义了模块的语义组成（所有规则都有对称的、省略的相互部分）。我们使用一个额外的组件，包含那些已经在任何一个模块和外部系统之间通信的名称，我们使用一个辅助存储器，只包含位置值。后者记录位置名称的最后已知值，这些位置名称不是单个模块的私有值每个模块中的延续名都被分配了程序/系统极性（我们写k∈P/k∈S），从而指定了延续名是由模块还是从外部系统引入的。交叉调用和返回被分配τ-标签，并由辅助延续名称标记。当与外部系统进行交互时，我们也使用以下符号来更新，其中我们将私有名称集合v（S，S）\n写成Pr。• （n，s∈）P[v，k，s]=Cl（s∈[s]，v（v）∈N）<${k}，并将P的极性赋给k;• （v，k，s）S[v，k，s]=Π∪ν(v, s\Pr)∪ {k}, and assign S polarity tok.符号也适用于没有延续名k被包括在更新（忽略k）。模M和M的语义组合是D.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）191199（）（）（Ⅲ）（i）P −→ P′Ps S −→ P′s SΠ Π内部调动ν（P ′）<$ν（S）<$ν（P）.（二）调用f，v，k调用f，v，kP−s−−→S′S−s−−→Ps'S−−τ−→S′s'[λ（s）]P′Π ΠP′交叉呼叫k ∈ N aux\v（S）.（三）其他事项retv，kretv，kP−s−→S′S−s−→P′Ps'S−−τ−→S′s'[λ（s）]P′Π Π交叉返回k ∈ N aux.（四）调用f，v，k调用f，v，kP−s−−→S′S−s−−→P的调用f，v，k S′s'[λ（s）]−−s'−[s−]<$−−'→'S程序调用n′=（n，s′）P[v，k，s]且k ∈ N κ\v（S）.（五）retv，kretv，kP−s−→S′S−s−→Ps'S−retv，kS′s′[λ（s）]Ss−'[−s−]<$−程序返回n′=（n，s′）P[v，s]且k ∈ N κ.Scallf，v，k P系统调用−s−−→(vi)k∈ Nκ\（ν（S′）\εS），ε′=（ε，s′）S[v，k，s]，Ss'S′调用f，v，k P∈s'[λ（s）]S′λ（s）∈ dom（s），s′\∈ s和ν（v，s\Pr）\∈Pr=π.−s<$−Sretv，kP系统返回−s−→（vii）k∈ Nκ\v（S′），n′=（n，s′）S[v，s]，Ss'S′retv，k P∈s'[λ（s）]S′λ（s）∈ dom（s），s′\∈ s和ν（v，s\Pr）\∈Pr=π.−−s<$−因此由下式给出：图二、 语义组合规则s0MM=M0M其中，s0是将初始值分配给M，对于s也是如此，并且s包含所有导出和导入的名称。图2的规则的特征在于关于延续名称、2系统存储3和名称隐私的选择的副条件。后者源于名义博弈语义[1，11]，它们保证M和M不重叠（规则（i）），并且系统在复合模块中引入的名称不与M或M引入的任何名称重叠（规则（vi）-（vii））。他们防止在作文中出现错误的名字让我们把复合SLS中的四个参与者称为程序A、系统A、程序B、系统B。当我们使用X，Y作为程序或系统名称时，它们可以是A或B，但不同。每当我们说代理时，我们指的是程序或系统。 复合系统的状态是一对（代理X，代理Y），注意它们不能都是程序。复合转换规则反映了以下直觉。• 规则（i）：如果程序X进行了内部（操作）转换，则系统Y不是被转换的。• 规则（ii）-（iii）：如果程序X进行到系统X的系统转换，并且[2]也就是说，辅助名被精确地用于交叉调用和返回。3这些规则规定（规则（vi）-（vii））在每个外部系统转换中产生的存储必须：（a）在所有公共名称（即在公共名称中的名称）上定义，和（b）在所有其他名称上与旧名称一致。后者可以防止系统破坏姓名隐私。200D.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）191（）（）（）系统Y可以匹配到程序Y的转换，然后复合系统进行内部（τ）转换。 这是最重要的规则，它类似于通过“同步和隐藏”的游戏语义组合。它表示M调用（或返回）M中存在的函数。• 规则（iv）-（v）：如果程序X进行了一个系统转换，而系统Y不能匹配它，那么它是复合系统中的一个系统转换，一个非本地调用或返回。• 规则第㈥至㈦条：从复合系统配置（两个实体都在系统配置中），程序X或程序Y可以通过系统的调用或返回而变为活动状态。现在我们可以形式化并证明函数复合（证明见附录B）。定义3.1设G1，G2是分别对应于语义复合SLS和普通SLS的LTS。从G1的状态到G2的构形的函数R称为τ-同构，如果它将G1的初始状态映射到G2的初始构形，并且对G1的所有状态X和l∈ L，(i) 如果X−→τX <$，则R（X）=R（X <$），(ii) 如果X→X <$，则R（X）→R（X <$），(iii) 若R（X）−→Y且X−/→τ则X−→X <$且R（X <$）=Y，(iv) 如果X−→lX <$，则R（X）−→lR（X <$），(v) 若R（X）−→lY且X−/→τ则X−→lX <$且R（X <$）=Y。若存在τ-同构R：G1 → G2，则我们称G1→ τG2.命题3.2公式M，M，MM=τM·M。4关于SLS受认知约束的系统级语义为编程语言提供了一种安全的语义，这种语义由编程语言的逻辑属性和它所产生的等价概念所反映。我们将看到，模块的SLS中的某些跟踪属性对应于“违反保密性”，即不受欢迎的名称泄露，这些名称旨在保持秘密。在这种跟踪中，将系统称为攻击者并将其行为视为攻击是合理的。我们将看到，虽然攻击不能在给定的语言中实现，但它可以在现实的系统中通过系统级的动作来实施我们还将看到，已知在传统语义中保持的某些等价物在系统级模型中仍然保持。这意味着，即使存在一个无所不能的攻击者，不受一组规定的语言结构的约束，认知限制也可以阻止某些观察，不仅是编程上下文，而且是任何周围的计算系统。这是一个非常强大的等价概念，它体现了模块的防篡改性D.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）191201请注意，我们选择这些例子来说明SLS引起的属性的概念兴趣，而不是作为基于SLS的推理技术的数学能力的说明。因此，这些例子尽可能简单明了。4.1系统级攻击：违反保密性这个例子是受到一个被禁止的安全协议的启发，该协议被非正式地描述如下。考虑一个秘密，一个本地生成的密钥和一个从环境中读取的数据项。 如果本地密钥和输入数据相等，则输出秘密，否则输出本地密钥。在传统的进程演算语法中，协议可以写为是的在（a）段中。ifk = a then out（s）else out（k）.的确，秘密s没有被泄露，因为局部k不能被知道，因为它只在最后被公开。这一点可以用基于双向模拟的匿名技术来证明。让我们考虑一下协议的实现：public void prot;public voidread; publicvoid prot（）{locals， k，x; s= new（）; k= new（）; x=read（）;if（*x== *k）then *s else *k}我们有局部变量s保存我们使用系统提供的非本地函数read从系统获取一个名称，该名称不能是存储在s或k处的名称。使用不受信任的系统调用read（）将值读入x。如果将存储在s中的名称公开，是否会侵犯s与过程演算模型不同，答案是初始配置为“保护”，读作|波特，读“波特”。 我们用E来表示保护体。图3中示出了与被泄露的秘密相对应的转换。标记的转换是程序和系统之间的交互，解释如下：(i) 系统调用prot（）给出continuationk(ii) 程序调用read（）给出新的延续k(iii) 系统返回（从读取）使用k并产生新名称a2(iv) 程序返回（从prot）泄漏本地名称a1存储在k(v) 系统使用k**来伪造第二次从读取返回，使用刚刚学习的名称返回值为1(vi) 利用1，程序现在将存储在S中的秘密A0返回到环境。值2被省略，因为它们不影响过渡。202D.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）191调用prot（），k联系我们|P0−−→ N 0， k|P0， k，−， E，k−→ N 1，k，a0，a1|P0， k∈（s<$→a0， p<$→a1，x<$→0），（Q;if（x==p）thenselsep）（x=Q）（read（Q）），（），k调用read（），k"“−→nnN1，k， k，a0，a1|P1<$（s<$→a0，k<$→a1，x<$→0， k<$→（t，k））reta2，k“”−−−−−−−−−→N2|P1，a2<$（s<$→a0，k<$→a1，x<$→0， k<$→（t，k）），t，a2，k<$−→ N 2|P1，a2<$（s<$→a0，k<$→a1，x<$→a2，k′<$→（t，k）），−，a1，k<$reta1，k′−−→N2|P2，a2，a1<$（s<$→a0，k<$→a1，x<$→a2， k<$→（t，k））nreta1，k“”−−−−−−−−−→N2|P1，a2，a1<$（s<$→a0，k<$→a1，x<$→a2， k<$→（t，k）），t，a1，k<$−→ N 2|P1，a2，a1<$（s<$→a0，k<$→a1，x<$→a1，k′<$→（t，k）），−，a0，k<$reta0，k′−−→N2|P2，a2，a1，a0.Above，t=（Q;if（x== k）thenx=elsek）x=Q，N0=P0={prot，read}，N1=N0={s，k，x}，N2= N1<${k，k ′，a0，a1，a2}和P1= P0 <${k，k ′}。图三. 秘密泄露。关键步骤是（v），系统以一种可能非法的，或者至少是意想不到的方式使用延续这种攻击可以通过几种方式实现• 如果攻击者可以访问更具表现力的控制命令（如callcc），则可以简单地重放延续。• 如果攻击者对内存有低级别的访问权限，它可以克隆（复制和存储）延续k，即由名称k指向的内存。为了执行攻击，不需要理解实际的机器码或字节码，因为延续被视为黑盒。这意味着任何依赖于指令或地址空间混淆的技术（如随机化）都无法阻止攻击。• 如果攻击者可以访问类似fork的并发原语，那么它就可以利用它们进行攻击，因为这些原语复制了执行线程，创建了所有内存段的副本。请注意，传统Unixfork的行为比我们在系统模型中考虑的要丰富，但它可以通过配置克隆系统转换轻松地容纳在我们的框架中：联系我们|Ps→N + N|P + Ps [N/inl（N）]s [N/inr（N）] s• 攻击者4.2等价功能组合性为语义提供了内部一致性检查。这已经表明我们的语言从系统级的角度来说是D.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）191203Mw0MLM1M122212以上扩展到P为的模10M2 通过明确地填充缺失的的观点。 在本节中，我们想进一步强调这一点。 我们能做到这通过证明存在非平凡的等价物。我们可以证明很多这样的等价关系，但我们将选择一个简单但重要的，因为它体现了国家的地方性原则这个看似简单的例子首先在[13]中给出，并建立了一个局部变量不能被非局部函数干扰这是一个有趣的例子，因为它突出了命令式编程的全局状态模型的一个重大缺陷虽然当时没有指出，但状态的函子范畴模型大致在同一时间发展，为这种等价性提供了数学上清晰的解决方案，这直接遵循编程语言的类型结构[15]。我们通过检查他们的踪迹来比较SLSs。形式上，模M的迹的集合由下式给出：T（M）={（π·w）∈L<$ | S0−→→X，α∈PM。π（a）=a}其中，请注意，我们循环遍历，以便分解出初始私有名称的选择。定义4.1设M1，M2是具有公共公共名的模我们说M1和M2是等价的，当T（<$M1））=T（<$M2））时，设M1 = M2.两边都是公众人物接下来，我们引入一个方便的双相似性概念，精确地捕获跟踪等价性。对于每一个配置X，让我们写P（X）为X的公共名称集。定义4.2设R是配置之间的关系R是一个模拟，如果，无论何时（X1，X2）∈R，我们有P（X1）=P（X2），并且：• X1→X1≠（X1≠，X2）∈R;L• X1−→X，其中（π·X）−→X ∈R和（X ∈， X∈）∈R，对于某些情形，命名置换π，使得π（a）=a，对所有a∈P（X1）.R是互模拟，如果它和它的逆是模拟。模块M1和M2是互相似，记为M1<$M2，如果存在互模拟R，使得（S0，S02）∈R.引理4.3双相似性与迹等价一致。命题4.4迹等价是模合成−·−的同余。可以直接检查以下三个程序是否具有双相似SLS转换系统：exportf; import g; declf（） {local x;g（）; return *x;}exportf; import g; decl x; declf（） {g（）; return *x;}exportf; import g; declf（） {g（）; return 0;}直观地说，原因是在前两个程序中f-local（module-local，re-local）变量x对非局部函数g永远不可见，并且将保持其初始值P204D.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）191值，它是0。互模拟关系是直接的，因为三个LTS是相等的模无声转换和x的私有名称的置换。其他等价性，例如参数性[14]的形式也成立，通过互模拟简单证明等价性：出口公司，get;decl x;decl inc（）{x=（*x+1）%3;}decl get（）{return *x;}出口公司，get;decl x;decl inc（）{x=（*x-1）%3;} decl get（）{return-*x;}这两个程序，或者更确切地说是库，使用私有隐藏状态x，将模3计数器实现为ab数据结构。环境可以递增计数器（inc）或读取其值（get），但不能执行其他操作。第一个实现向上计数，第二个向下计数。5结论在本文中，我们提出了一个宽松的博弈语义概念，其中对手的行为是由认知约束而不是组合约束来定义的。这使我们得出了我们认为重要的两个结论。首先，我们要再次强调的事实是，操作语义可以扩展到一个相对简单的方式从处理程序处理条款，而不依赖于翻译或解释。这是一个已经隐含在跟踪语义[8]或环境互模拟[9]等技术中的想法。在这个过程中，操作语义变成了组合语义。术语的LTS指称解释自动出现，而不会失去其有效的呈现。然而，与以前的工作不同的是，我们不把这种操作语义学的扩展作为达到目的的手段，例如研究语境对等，但我们把它本身视为重要的第二，也是最重要的，我们想证明，一个有意义的和有用的上下文概念可以在语言的语法之外构建。这有几个优点。第一个是模块化，因为我们可以定义语言及其术语独立运行的环境;函数组合的原则是我们需要满足的一致性检查，以便两者能够一起工作。第二个是现实主义，因为现实生活中的语言允许，通过单独编译和外部函数接口等机制，程序在语法上是异构的，因此它们不能被通常的上下文概念所表征。 第三个是简单性，因为我们展示了如何有可能制定的方式，这是不计算的，但认识的环境限制，类似于既定的Dolev-Yao表征的安全环境。我们相信这有可能一个语义的基础，用于研究程序的安全属性（如信息流或防篡改编译），其方式较少依赖于语法的变幻莫测和更多的模块化。具有相似目标但不同理念的相关工作已经完成，D.R. Ghica，N.Tzevelekos/电子笔记理论计算机科学286（2012）191205在composite compiler correctness中执行[4]。尽管我们的观点主要是分析性的，对描述任意（如果不是无限制的话）环境的特征感兴趣，并在操作上检查这些环境中开放项的行为，但组合编译器正确性主要是一个综合问题，旨在定义机器代码上的约束，这些约束允许通过编译生成的代码与以任意方式生成的代码之间的安全组合。我们认为这两种方法是同一问题的两个方面，我们认为应该研究更好地理解它们之间的关系引用[1] S. Abramsky，D. R. Ghica，A. S. Murawski，C. H. L.王，我。D. B.斯塔克nu演算的名义博弈与完全抽象LICS，pp 150[2] S.阿布拉姆斯基河Jagadeesan和P. Malacaria。 PCF的完全抽象。信息计算，163（2），2000.[3] S. Abramsky和G.麦卡斯克线性，共享和状态：一个完全抽象的游戏语义与积极的表达理想Algol 电动注意Theor。Comput. Sci. ，3，1996.[4] N. Benton和C.- K.呵。双正交性、步进索引与编译正确性。载于IC