本文使用一种用于建模与分析软件设计的语言 Alloy来构建同源策略 SOP 模型。Alloy作为建模语言，并不能编写程序执行，但它可以编写模型，并通过自动生成并运行测试用例来对模型进行检查。感觉 Alloy 的中文资料不是很多，感兴趣的小伙伴可以看下官网。

原文作者

Eunsuk Kang、Santiago Perez De Rosso 和 Daniel Jackson。Eunsuk Kang 是麻省理工学院的博士研究生和软件设计小组成员。他在麻省理工学院（2010年）获得计算机科学硕士学位，并获得滑铁卢大学软件工程学士学位（2007年）。他的研究项目集中于开发软件建模和验证的工具和技术，并将其应用于安全和安全关键系统。

Santiago Perez De Rosso 是麻省理工学院软件设计组的博士生。他在麻省理工学院获得计算机科学硕士学位（2015年），并在ITBA获得本科学位（2011年）。他曾在谷歌工作，开发框架和工具，让工程师更有效率（2012年）。他现在大部分时间都在考虑设计和版本控制。

Daniel Jackson 是麻省理工学院电子工程和计算机科学系的教授，他领导着计算机科学和人工智能实验室的软件设计小组。他获得牛津大学物理硕士学位（1984年），麻省理工学院计算机科学硕士（1988年）和博士学位（1992年）。他是卡内基梅隆大学 Logic 公司的软件工程师（1984—1986年），卡内基梅隆大学计算机科学助理教授（1992—1997年），自1997年毕业于麻省理工学院。他对软件工程有着广泛的兴趣，尤其是在开发方法、设计和规范、形式方法和安全关键系统方面。

引言

同源策略（SOP）是现代浏览器安全机制的重要组成部分。它控制在浏览器中运行的脚本何时可以相互通信（粗略地说就是它们何时来自同一个网站）。SOP 最初是在 Netscape Navigator 中引入的，现在它在 Web 应用程序的安全性方面起着关键的作用；如果没有它，恶意黑客在 Facebook 上浏览你的私人照片、阅读你的电子邮件或清空你的银行账户就会容易得多。

但 SOP 还远远不够完美。有时，限制性太强；在某些情况下（如 mashup），来自不同来源的脚本应该能够共享资源，但却做不到。有时，它又没有足够的限制，留下了可以利用常见攻击（如跨站点请求伪造）的极端案例。此外，SOP 的设计经过多年的发展，让许多开发人员无法完全理解。

本文的目的是抓住这一重要但经常被误解的特征的本质。特别是，我们将尝试回答以下问题：

• 为什么需要SOP？它可以防止哪些类型的安全违规行为？

• SOP如何影响 Web 应用程序的行为？

• 绕过SOP的机制有什么不同？

• 这些机制有多安全？它们会带来哪些潜在的安全问题？

考虑到 Web 服务器、浏览器、HTTP、HTML 文档、客户端脚本等所涉及部分的复杂性，全面覆盖 SOP 是一项艰巨的任务。我们可能会被这些部分的粗糙细节所困扰（甚至在达到 SOP 之前就写完我们的 500 行代码）。但是，我们怎么能在不陈述关键细节的情况下做到精确讲解呢？

使用 Aolly 建模

本文与这本书中的其它章节有些不同。我们将构建一个可执行模型，作为 SOP 的简单而精确的描述，而不是构建一个可以工作的实现。与实现一样，可执行模型来探索系统的动态行为，但与实现不同的是，模型忽略了可能妨碍理解基本概念的低级细节。

我们采用的方法可能被称为“敏捷建模”，因为它与敏捷编程类似。我们逐步地工作，一点一点地组装模型。我们的演变模型在每一点上都是可以执行的。我们在演变过程中制定并运行测试，这样到最后我们不仅拥有模型本身，而且还拥有它所满足的属性集合。

为了构建这个模型，我们使用 Alloy，一种用于建模和分析软件设计的语言。 Alloy 模型不能在传统意义上的程序执行中执行。相反，可以（1）模拟模型以生成表示系统的有效场景或配置的实例，（2）检查模型是否满足所需属性。

除了上述相似之处，敏捷建模与敏捷编程在一个关键方面不同：尽管我们会运行测试，但实际上我们不会编写任何测试代码。Alloy 的分析器自动生成测试用例，需要提供的只是要检查的属性。不用说，这省去了很多麻烦（和文字）。分析器实际执行所有可能的测试用例，直到达到一定的大小（称为范围）；这通常意味着生成所有可能对象的所有启动状态，然后选择操作和参数应用到一些步骤中。由于执行了如此多的测试（通常是数十亿），并且由于涵盖了一个状态可以采取的所有可能配置（尽管在范围内），这种分析往往可以比传统测试更有效地暴露BUG （有时被称为“有界验证”）。

简化

因为 SOP 是在浏览器、服务器、HTTP等环境中运行的，所以一个完整的描述将十分复杂。因此，我们的模型（和所有模型一样）抽象掉了不相关的方面，比如网络数据包的结构和路由。同时它也简化了一些相关的方面，这意味着该模型不能完全考虑到所有可能的安全漏洞。

例如，我们将 HTTP 请求视为远程过程调用，而忽略了对请求的响应可能出现顺序错误这一事实。我们还假设 DNS（域名服务）是静态的，因此我们不考虑在交互过程中 DNS 绑定改变的攻击。虽然从原则上讲，我们可以扩展我们的模型以涵盖所有这些方面，但在安全分析的本质上，任何模型（即使它代表整个代码库）都不能保证是完整的。

路线图

以下是我们向前演化 SOP 模型的顺序。我们将首先构建三个关键组件的模型，这三个组件是我们讨论SOP所需要的：HTTP、浏览器和客户端脚本。我们将在这些基本模型的基础上构建，以定义 Web 应用程序的安全性意义，然后引入 SOP 作为一种尝试实现所需安全属性的机制。

然后我们将看到 SOP 有时会限制性太强，妨碍web应用程序的正常运行。因此，我们将介绍四种不同的技术，它们通常用于绕过政策施加的限制。

你可以按自己喜欢的顺序浏览这些部分。如果你不熟悉 Alloy，我们建议你从前三部分（HTTP、浏览器和脚本）开始，因为它们介绍了建模语言的一些基本概念。在你阅读本文的同时，我们也鼓励你使用 Alloy 分析器中的模型；运行它们，探索生成的场景，尝试进行修改并查看其效果。它可以免费下载。

Web模型

HTTP

构建 Aolly 模型的第一步是声明一些对象集。让我们从资源开始：

sig Resource {}

关键字 sig 将其标识为 Aolly 签名声明。这引入了一组资源对象；把它们想象成没有实例变量的类的对象，有标识但没有内容的blob。当分析运行时，这个集合将被确定，就像面向对象语言中的类在程序执行时用来表示一组对象一样。

资源由URL（统一资源定位符）命名：

sig Url {
  protocol: Protocol,
  host: Domain,
  port: lone Port,
  path: Path
}
sig Protocol, Port, Path {}
sig Domain { subsumes: set Domain }

在这里，我们有五个签名声明，介绍了一组 URL 和四个附加集，分别用于它们所包含的每种基本类型的对象。在 URL 声明中，我们有四个字段。字段类似于类中的实例变量；例如，如果 u 是一个URL，那么 u.protocol 将表示该 URL 的协议（就像Java中的点）。但事实上，我们将在后面看到，这些字段是关系。你可以将每个表看作是一个两列数据库表。因此，protocol 是一个表，第一列包含 URL，第二列包含协议。看起来无害的点运算符实际上是一种相当普遍的关系连接，因此你也可以为所有具有协议 p 的 URL 编写 protocol.p，稍后会有更多这方面的内容。

请注意，与 URL 不同，路径被视为没有结构，这是一种简化。关键字 lone（可以读作“小于等于1”）表示每个 URL 最多有一个端口。路径是 URL 中主机名后面的字符串，它（对于简单的静态服务器）对应于资源的文件路径；我们假设它总是存在的，但可能是一条空路径。

让我们介绍一下客户端和服务器，它们都包含从路径到资源的映射：

abstract sig Endpoint {}
abstract sig Client extends Endpoint {}
abstract sig Server extends Endpoint {
  resources: Path -> lone Resource
}

extends 关键字引入了一个子集，因此所有客户端的集合 Client 就是所有端点的集合 Endpoint 的子集。扩展是不相交的，因此没有端点同时是客户端和服务器。abstract 关键字表示签名的所有扩展都会继承它，因此它出现在 Endpoint 声明中，例如，表示每个端点必须属于其中一个子集（此时为 Client 和 Server）。对于服务器 s，表达式 s.resources 将表示从路径到资源的映射（声明中的箭头）。回想一下，每个字段实际上都是一个关系，第一列包含所有者签名，因此此字段表示 Server、Path 和 Resource 上的三列关系。

为了将 URL 映射到服务器，我们引入了域名服务器集合 Dns，每个服务器都具有从域到服务器的映射：

one sig Dns {
  map: Domain -> Server
}

签名声明中的关键字 one 意味着（为简单起见）我们将假设只有一个域名服务器，并且将有一个由表达式 DNS.map 给出的DNS映射。同样，和服务资源一样，这可能是动态的（事实上，在交互过程中存在依赖于更改 DNS 绑定的已知安全攻击），但我们进行了简化。

为了对 HTTP 请求建模，我们还需要 Cookie 的概念，让我们声明：

sig Cookie {
  domains: set Domain
}

每个 Cookie 的范围是一组域；这代表了这样一个事实： Cookie 可以应用于 *.mit.edu，它将包括后缀为 mit.edu 的所有域。

最后，我们可以将这些放在一起构建 HTTP 请求的模型：

abstract sig HttpRequest extends Call {
  url: Url,
  sentCookies: set Cookie,
  body: lone Resource,
  receivedCookies: set Cookie,
  response: lone Resource,
}{
  from in Client
  to in Dns.map[url.host]
}

我们在单个对象中建模 HTTP 请求和响应；url、sentCookies 和 body 由客户端发送，而 receivedCookies 和 response 则由服务器发回。

在编写 HttpRequest 签名时，我们发现它包含调用的通用特性，即它们来自和指向特定事物。所以我们实际上编写了一个声明 Call 签名的小 Alloy 模块，要在这里使用它，我们需要导入它：

open call[Endpoint]

它是一个多态模块，所以它是用端点实例化的，调用的对象集是 from 和 to。

HttpRequest 中的字段声明后面是一组约束。这些约束中的每一个都适用于HTTP请求集的所有成员。约束条件表示（1）每个请求来自客户端，（2）每个请求都被发送到 DNS 映射下 URL 主机指定的一个服务器。

Alloy 的一个显著特点是，无论模型多么简单或详细，都可以随时执行以生成示例系统实例。让我们使用 run 命令要求 Alloy 分析器执行到目前为止的 HTTP 模型：

run {} for 3    -- generate an instance with up to 3 objects of every signature type

一旦分析器找到系统的一个可能实例，它就会自动生成一个实例图，如下图。

fig-http-1.png

此实例显示了一个客户端（由节点 Client 表示）向 Server 发送 HttpRequest，服务器作为响应返回一个资源对象，并指示客户端在 Domain 中存储 Cookie。

尽管这是一个很小的例子，细节似乎很少，但它表明我们的模型存在缺陷。请注意，从请求（Resource1）返回的资源在服务器中不存在。我们忽略了一个关于服务器的明显事实；也就是说，对请求的每个响应都是服务器存储的资源。我们可以回到 HttpRequest 的定义并添加一个约束：

abstract sig HttpRequest extends Call { ... }{
  ...
  response = to.resources[url.path]
}

现在重新运行会生成没有该缺陷的实例。

我们可以要求分析器检查模型是否满足属性，而不是生成示例实例。例如，我们可能需要的一个特性是，当客户端多次发送相同的请求时，它总是会收到相同的响应：

check { 
    all r1, r2: HttpRequest | r1.url = r2.url implies r1.response = r2.response 
} for 3 

给定此check命令，分析器探索系统的所有可能行为（直到指定的界限），当发现违反属性的行为时，将该实例显示为反例，如下所示。

fig-http-2a.png

fig-http-2b.png

这个反例再次显示了一个由客户端发出的 HTTP 请求，但是使用两个不同的服务器(在Alloy visualizer中，相同类型的对象通过在名称后附加数字后缀来区分；如果给定类型只有一个对象，则不添加后缀。快照关系图中出现的每个名称都是对象的名称。因此，乍一看，Domain、Path、Resource、Url 都是指单个对象，而不是类型，这可能会令人困惑。）

请注意，虽然 DNS 将 Domain 映射到 Server0 和 Server1（实际上，这是负载平衡的常见做法），但只有 Server1 将 Path 映射到资源对象，导致 HttpRequest1 产生空响应：我们模型中的另一个错误。为了解决这个问题，我们添加了一个 Alloy fact记录 DNS 映射到单个主机的任何两个服务器都提供相同的资源集：

fact ServerAssumption {
  all s1, s2: Server | 
    (some Dns.map.s1 & Dns.map.s2) implies s1.resources = s2.resources
}

添加此 fact 后重新运行 check 命令时，分析器不再报告该属性的任何反例。这并不意味着这个属性已经被证明是正确的，因为在更大的范围内可能会有一个反例。但是属性不太可能为否，因为分析器已经测试了所有可能的实例，每个实例都涉及每种类型的3个对象。

但是，如果需要，我们可以在更大范围内重新运行分析，以增加信心。例如，在范围为10的情况下运行上述检查仍然不会产生任何反例，这表明该属性可能是有效的。但是，请记住，给定更大的范围，分析器需要测试更多的实例，因此可能需要更长的时间才能完成。

浏览器

现在，让我们在模型中引入浏览器：

sig Browser extends Client {
  documents: Document -> Time,
  cookies: Cookie -> Time,
}

这是我们第一个带有动态字段的签名示例。Alloy 没有内置的时间或行为概念，这意味着可以使用各种习惯用法。在这个模型中，我们使用了一个常见的习惯用法，在这个习惯用法中，你引入了 Time 的概念，并将其作为每个时变字段的最后一列。例如，表达式 b.cookies.t 表示在特定时间 t 存储在浏览器 b 中的 cookies 集。同样，documents 字段在给定时间将一组文档与每个浏览器关联。

文档是根据对 HTTP 请求的响应创建的。例如，如果用户关闭选项卡或浏览器，但我们将其从模型中删除，它们也会被销毁。文档有一个URL（文档的来源）、一些内容（DOM）和一个域：

sig Document {
  src: Url,
  content: Resource -> Time,
  domain: Domain -> Time
}

包含后两个字段的 Time 列告诉我们，它们可以随时间而变化，而省略第一个字段（src，表示文档的源URL）表明源 URL 是固定的。

为了模拟 HTTP 请求对浏览器的影响，我们引入了一个新的签名，因为并非所有 HTTP 请求都源自浏览器级别；其余的将来自脚本。

/* 从浏览器发送到服务器的HTTP请求 */
sig BrowserHttpRequest extends HttpRequest { doc: lone Document }{
    -- 请求来自浏览器
    from in Browser
    -- 请求时浏览器中存在正在发送的cookie
    sentCookies in from.cookies.start
    -- 发送的每个cookie都必须限定为请求的url
    matchingScope[sentCookies, url]

    -- 如果没有响应，则不会打开新文档
    some doc iff some response
    -- 将创建一个新文档以显示响应的内容
    documents.end = documents.start + from -> doc
    -- 新文档将响应作为其内容
    content.end = content.start ++ doc -> response
    -- 新文档将url的主机作为其域
    domain.end = domain.start ++ doc -> url.host
    -- 文档的源是请求的url
    some doc implies doc.src = url

    -- 浏览器会存储新的cookie
    cookies.end = cookies.start + from -> sentCookies
}

此类请求有一个新字段 doc，表示从请求返回的资源在浏览器中创建的文档。与 HttpRequest 一样，该行为被描述为一组约束。其中一些表示调用何时发生：例如，调用必须来自浏览器。有些约束调用的参数：例如，Cookie 必须被适当地限定范围。还有一些限制效果，使用一种常见的习惯用法，将调用后关系的值与调用前关系的值联系起来。

例如，要理解约束 documents.end = documents.start + from -> doc，请记住，在浏览器、文档和时间上，documents 是三列关系。字段 start 和 end 来自 Call 声明（我们还没有看到，但包含在末尾的列表中），表示调用开始和结束的时间。表达式 documents.end 在调用结束时提供从浏览器到文档的映射。因此，该约束表示，在调用之后，映射是相同的，只是表中的一个新条目映射 from 到 doc。

某些约束使用 ++ 关系覆盖运算符：e1 ++ e2 包含 e2 的所有元组，此外，其第一个元素不是 e2中元组的第一个元素的任何 e1 元组。例如，content.end = content.start ++ doc -> response 表示在调用之后， content 映射将更新为将 doc 映射到 response（覆盖 doc 之前的任何映射）。如果改为使用联合运算符+，则同一文档可能（错误地）映射到处于后续状态的多个资源。

脚本

接下来，我们将在 HTTP 和浏览器模型的基础上引入客户端脚本，这些脚本表示在浏览器文档（context）中执行的代码片段（通常是JavaScript）。

sig Script extends Client { context: Document }

脚本是一个动态实体，它可以执行两种不同的操作：（1）它可以发出 HTTP 请求（即Ajax请求）和（2）它可以执行浏览器操作来操作文档的内容和属性。客户端脚本的灵活性是 Web2.0 快速发展的主要催化剂之一，也是 SOP 最初创建的原因。如果没有 SOP，脚本将能够向服务器发送任意请求，或者自由修改浏览器中的文档，如果一个或多个脚本被证明是恶意的，这将是一个坏消息。

脚本可以通过发送 XmlHttpRequest 与服务器通信：

sig XmlHttpRequest extends HttpRequest {}{
  from in Script
  noBrowserChange[start, end] and noDocumentChange[start, end]
}

脚本可以使用 XmlHttpRequest 向服务器发送/接收资源，但与 BrowserHttpRequest 不同，它不会立即创建新页面或对浏览器及其文档进行其他更改。为了说明调用不会修改系统的这些方面，我们定义了谓词 noBrowserChange 和 noDocumentChange：

pred noBrowserChange[start, end: Time] {
  documents.end = documents.start and cookies.end = cookies.start  
}
pred noDocumentChange[start, end: Time] {
  content.end = content.start and domain.end = domain.start  
}

脚本可以对文档执行什么类型的操作？首先，我们引入浏览器操作的一般概念，以表示一组可由脚本调用的浏览器 API 函数：

abstract sig BrowserOp extends Call { doc: Document }{
  from in Script and to in Browser
  doc + from.context in to.documents.start
  noBrowserChange[start, end]
}

字段 doc 是指此调用将访问或操作的文档。签名事实中的第二个约束条件是，doc 和执行脚本的文档（from.context）必须是当前存在于浏览器中的文档。最后，BrowserOp 可以修改文档的状态，但不能修改存储在浏览器中的文档集或 Cookie(实际上，Cookie可以与文档关联并使用浏览器API进行修改，但我们现在省略了这个细节。）

脚本可以读取和写入文档的各个部分（通常称为 DOM 元素）。在一个典型的浏览器中，有大量用于访问 DOM 的 API 函数（例如 document.getElementById），但是枚举所有这些函数对于我们的目的并不重要。相反，我们将它们简单地分为两类：ReadDom 和 WriteDom，以及作为整个文档的整体替换的模型修改：

sig ReadDom extends BrowserOp { result: Resource }{
  result = doc.content.start
  noDocumentChange[start, end]
}
sig WriteDom extends BrowserOp { newDom: Resource }{
  content.end = content.start ++ doc -> newDom
  domain.end = domain.start
}

ReadDom 返回目标文档的内容，但不修改它；另一方面，WriteDom 将目标文档的新内容设置为 newDom。

此外，脚本可以修改文档的各种属性，如宽度、高度、域和标题。对于SOP的讨论，我们只对域属性感兴趣，我们将在后面的部分中介绍。

示例应用程序

如前所述，给定 run 或 check 命令，Alloy 分析器将生成与模型中系统描述一致的场景（如果存在）。默认情况下，分析器任意选择任何一种可能的系统场景（直到指定的界限），并为场景中的签名实例（Server0、Browser1等）分配数字标识符。

有时，我们可能希望分析特定 Web 应用程序的行为，而不是探索随机配置服务器和客户端的场景。例如，假设我们希望构建一个在浏览器中运行的电子邮件应用程序（如Gmail）。除了提供基本的电子邮件功能外，我们的应用程序还可能显示来自第三方广告服务的横幅，该广告服务由潜在的恶意参与者控制。

在 Alloy 中，关键字 one sig 引入了仅包含一个对象的单态签名；我们在上面看到了一个使用 Dns 的示例。此语法可用于指定具体的原子。例如，要说有一个收件箱页面和一个广告横幅（每个都是文档），我们可以写：

one sig InboxPage, AdBanner extends Document {}

通过此声明，Alloy 生成的每个场景都将至少包含这两个 Document 对象。

同样，我们可以指定特定的服务器、域等，并使用约束（我们称之为 Configuration）来指定它们之间的关系：

one sig EmailServer, EvilServer extends Server {}
one sig EvilScript extends Script {}
one sig EmailDomain, EvilDomain extends Domain {}
fact Configuration {
  EvilScript.context = AdBanner
  InboxPage.domain.first = EmailDomain
  AdBanner.domain.first = EvilDomain  
  Dns.map = EmailDomain -> EmailServer + EvilDomain -> EvilServer
}

例如，事实中的最后一个约束指定如何将 DNS 配置为映射系统中两个服务器的域名。如果没有此约束，Alloy 分析器可能会生成将 EmailDomain映射到 EvilServer的场景，我们对此不感兴趣（实际上，这种映射可能是由于一种称为DNS欺骗的攻击造成的，但我们将从我们的模型中排除它，因为它不属于SOP旨在防止的攻击类别。）

让我们介绍另外两个应用程序：在线日历和博客站点：

one sig CalendarServer, BlogServer extends Document {} 
one sig CalendarDomain, BlogDomain extends Domain {}

我们应该更新上面关于DNS映射的约束，以合并这两个服务器的域名：

fact Configuration {
  ...
  Dns.map = EmailDomain -> EmailServer + EvilDomain -> EvilServer + 
            CalendarDomain -> CalendarServer + BlogDomain -> BlogServer  
}

此外，让我们假设电子邮件、博客和日历应用程序都是由单个组织开发的，因此共享相同的基本域名。从概念上讲，我们可以认为 EmailServer 和 CalendarServer 具有子域 email 和 calendar，将 example.com 共享为公共超域。在我们的模型中，这可以通过引入一个域名包含其它来表示：

one sig ExampleDomain extends Domain {}{
  subsumes = EmailDomain + EvilDomain + CalendarDomain + this
}   

注意，由于每个域名都包含它自己，所以 this 是 subsumes的成员。

关于这些应用程序，我们在这里省略了其他细节（完整模型见 example.als）。但在本文的其余部分，我们将重新讨论这些应用程序，作为我们的运行示例。

安全属性

在讨论 SOP 之前，有一个重要的问题我们还没有讨论：当我们说我们的系统是安全的时，我们到底是什么意思？

毫不奇怪，这是一个很难回答的问题。出于我们的目的，我们将转向信息安全的保密性和完整性这两个经过充分研究的概念。这两个概念都讨论了如何允许信息通过系统的各个部分。粗略地说，机密性意味着关键数据块只能被认为是可信的部分访问，而完整性意味着可信部分只依赖于未被恶意篡改的数据。

数据流属性

为了更精确地指定这些安全属性，我们首先需要定义一段数据从系统的一部分流向另一部分意味着什么。到目前为止，在我们的模型中，我们已经将两个端点之间的交互描述为通过调用执行；例如，浏览器通过发出 HTTP 请求与服务器交互，脚本通过调用浏览器 API 操作与浏览器交互。直观地说，在每次调用期间，一段数据可能作为调用的参数或返回值从一个端点流向另一个端点。为了说明这一点，我们在模型中引入了 DataflowCall 的概念，并将每个调用与一组 args 和 returns 数据字段相关联：

sig Data in Resource + Cookie {}

sig DataflowCall in Call {
  args, returns: set Data,  -- 本次调用的参数和返回数据
}{
 this in HttpRequest implies
    args = this.sentCookies + this.body and
    returns = this.receivedCookies + this.response
 ...
}

例如，在 HttpRequest 类型的每次调用期间，客户端将SentCookies 和 body 传输到服务器，并接收 receivedCookies 和 response 作为返回值。

更一般地说，参数从调用的发送方流向接收方，返回值从接收方流向发送方。这意味着端点访问新数据段的唯一方法是将其作为端点接受的调用的参数或端点调用的调用的返回值接收。我们引入了 DataflowModule 的概念，并分配字段 accesses 以表示模块在每个时间步可以访问的数据元素集：

sig DataflowModule in Endpoint {
    -- 此组件拥有的数据集
    accesses: Data -> Time
} {
    all d: Data, t: Time - first |
        -- 只有在以下情况下，此端点才能在时间“t”访问一段数据“d”
        d -> t in accesses implies
            -- （1）它在上一时间步中已具有访问权限，或
            d -> t.prev in accesses or
            -- 有一些调用“c”，以“t”结尾，这样
            some c: Call & end.t |
                --（2）端点接收带有“d”作为其参数之一的“c”，或
                c.to = this and d in c.args or
                --（3）端点发送返回d的“c”
                c. from = this and d in c.returns

    -- 关于特定端点的限制
    this in Server implies Path.(this.resources) in initData
}

我们还需要限制模块可以作为参数或调用返回值提供的数据元素。否则，我们可能会遇到一些奇怪的情况，模块可以使用无法访问的参数进行调用。

sig DataflowCall in Call { ... } {
  -- 关于数据流调用的两个一般约束
  --（1）发送方必须能够访问任何参数
  args in from.accesses.start +
  --（除非是Ajax调用，在这种情况下，参数可能包括浏览器cookie）
      (this in XmlHttpRequest implies from.browser[start].accesses.start & Cookie else none)

  --（2）此调用返回的任何数据必须可供接收方访问
  returns in to.accesses.start
}

现在我们有了描述系统不同部分之间数据流的方法，我们（几乎）已经准备好陈述我们关心的安全属性。但请记住，保密性和完整性是与上下文相关的概念；只有当我们可以将系统中的某些代理称为受信任（或恶意）时，这些属性才有意义。同样，并非所有的信息都同等重要：我们需要区分我们认为是关键或恶意的数据元素（或两者都不）：

sig TrustedModule, MaliciousModule in DataflowModule {}
sig CriticalData, MaliciousData in Data {}

然后，机密性属性可以表示为关键数据流入系统不可信部分的断言：

// 任何恶意模块都不能访问私有数据
assert Confidentiality {
  no m: Module - TrustedModule, t: Time |
    some CriticalData & m.accesses.t 
}

完整性属性具有双重保密性：

// 任何恶意数据都不应进入受信任的模块
assert Integrity {
  no m: TrustedModule, t: Time | 
    some MaliciousData & m.accesses.t
}

威胁模型

威胁模型描述了攻击者在试图破坏系统安全属性时可能执行的一系列操作。建立威胁模型对任何安全系统的设计都是一个重要步骤；它允许我们识别关于系统及其环境的（可能是无效的）假设，并优先考虑需要缓解的不同类型的风险。

在我们的模型中，我们考虑一个可以充当服务器、脚本或客户端的攻击者。作为服务器，攻击者可能会设置恶意网页，以请求毫无戒心的用户进行访问，而这些用户可能会在 HTTP 请求中无意中将敏感信息发送给攻击者。攻击者可能会创建一个恶意脚本，调用 DOM 操作从其他页面读取数据，并将这些数据中继到攻击者的服务器。最后，作为客户端，攻击者可能会模拟普通用户并向服务器发送恶意请求，试图访问该用户的数据。我们不认为攻击者窃听不同网络端点之间的连接；虽然它在实践中是一种威胁，但 SOP 并不是为了防止它而设计的，因此它不在我们模型的范围之内。

检查属性

现在，我们已经定义了安全属性和攻击者的行为，让我们展示如何使用 Alloy 分析器自动检查这些属性，即使在攻击者在场的情况下，这些属性仍然有效。当使用 check 命令提示时，分析器将探索系统中所有可能的数据流跟踪，并生成一个反例（如果存在）来演示如何违反断言：

check Confidentiality for 5

例如，当根据机密性属性检查示例应用程序的模型时，分析器生成下面两幅图中的场景，其中显示了脚本如何访问一段关键数据（MyInboxInfo）。

fig-attack-1a.png

fig-attack-1b.png

这个反例包括两个步骤。在第一步中，EvilScript 在来自 EvilDomain 的 AdBanner 内执行，读取 InboxPage 的内容。在下一步中，EvilScript 通过调用 XmlHtttpRequest 向 EvilServer 发送相同的内容（MyInboxInfo）。这里的核心问题是，在一个域下执行的脚本能够从另一个域读取文档的内容；正如我们将在下一节中看到的，这正是 SOP 旨在防止的场景之一。

一个断言可能有多个反例。考虑下图，它显示了系统可能违反保密属性的另一种方式。

fig-attack-2.png

在这种场景下，脚本不读取收件箱页面的内容，而是直接向 EmailServer 发出 GetInboxInfo 请求。请注意，请求包含一个 cookie（MyCookie），其作用域与目标服务器的作用域相同。这是潜在的危险，因为如果 cookie 用于表示用户的身份（例如，会话 cookie），则脚本可以有效地伪装成用户，并诱使服务器使用用户的私有数据（MyInboxInfo）进行响应。这里，问题再次与脚本可用于跨不同域访问信息的自由方式有关，即在一个域下执行的脚本能够向具有不同域的服务器发出 HTTP 请求。

这两个反例告诉我们需要额外的措施来限制脚本的行为，特别是因为其中一些脚本可能是恶意的。这正是 SOP 的用武之地。

同源策略

在我们陈述 SOP 之前，我们应该做的第一件事是引入源的概念，它由协议、主机和可选端口组成：

sig Origin {
  protocol: Protocol,
  host: Domain,
  port: lone Port
}

为了方便起见，让我们定义一个函数，在给定 URL 的情况下，该函数返回相应的源：

fun origin[u: Url] : Origin {
    {o: Origin | o.protocol = u.protocol and o.host = u.host and o.port = u.port }
}

SOP 本身有两个部分，限制脚本（1）进行 DOM API 调用和（2）发送 HTTP 请求的能力。策略的第一部分规定，脚本只能读取和写入与脚本来源相同的文档：

fact domSop {
  all o: ReadDom + WriteDom |  let target = o.doc, caller = o.from.context |
    origin[target] = origin[caller] 
}

domSop 下不可能出现（上一节中的）第一个脚本场景这样的实例，因为不允许脚本对来自不同来源的文档调用 ReadDom。

该策略的第二部分指出，脚本无法向服务器发送 HTTP 请求，除非其上下文与目标 URL 具有相同的来源，从而有效地阻止了第二个脚本场景等实例。

fact xmlHttpReqSop { 
  all x: XmlHttpRequest | origin[x.url] = origin[x.from.context.src] 
}

正如我们所见，SOP 旨在防止恶意脚本操作可能产生的两类漏洞；没有它，网络将更加危险。

然而，事实证明，SOP 可能过于严格。例如，有时你确实希望允许两个不同来源的文档之间进行通信。根据上述来源的定义，来自 foo.example.com 的脚本将无法读取 bar.example.com 的内容，或向 www.example.com 发送 HTTP 请求，因为这些都被视为不同的主机。

为了在必要时允许某种形式的跨源通信，浏览器实现了各种放松 SOP 的机制。其中一些经过深思熟虑，一些则存在陷阱，如果使用不当，可能会破坏 SOP 的安全优势。在下面的部分中，我们将描述这些机制中最常见的，并讨论它们潜在的安全隐患。

绕过 SOP 的技术

SOP是功能性和安全性之间权衡的经典示例；我们希望确保我们的网站是健壮的和功能强大的，但是保护它的机制有时会成为障碍。事实上，当 SOP 最初引入时，开发人员在构建合法使用跨域通信（例如mashup）的站点时遇到了麻烦。

在本节中，我们将讨论 Web 开发人员为绕过 SOP 施加的限制而设计和经常使用的四种技术：（1）document.domain 属性松弛；(2） JSONP；(3） PostMessage；和（4）CORS。这些都是很有用的工具，但如果不小心使用，可能会使 Web 应用程序容易受到 SOP 最初设计用来阻止的攻击类型的攻击。

这四种技术中的每一种都非常复杂，详细描述需要专门的章节。所以这里我们只是简单介绍一下它们是如何工作的，它们带来的潜在安全问题，以及如何预防这些问题。特别是，我们将要求 Alloy 分析器检查每种技术是否会被攻击者滥用以破坏我们之前定义的两个安全属性：

check Confidentiality for 5
check Integrity for 5

根据分析器生成的反例，我们将讨论安全使用这些技术而不落入安全陷阱的指导原则。

域属性

作为我们列表中的第一项技术，我们将使用 document.domain 属性作为绕过 SOP 的方法。这种技术背后的思想是，只需将 document.domain 属性设置为相同的值，即可允许来自不同来源的两个文档访问彼此的 DOM。因此，例如，如果两个文档中的脚本都将 document.domain 属性设置为 example.com（假设两个源 URL 也具有相同的协议和端口），则 email.example.com 中的脚本可以读取或写入 calendar.example.com 中文档的 DOM。

我们将 document.domain 属性的设置行为建模为一种称为 SetDomain 的浏览器操作：

// 修改 document.domain 属性
sig SetDomain extends BrowserOp { newDomain: Domain }{
  doc = from.context
  domain.end = domain.start ++ doc -> newDomain
  -- 文件内容无任何更改
  content.end = content.start
}

newDomain 字段表示属性应设置为的值。不过有一个警告：脚本只能将域属性设置为其主机名的右侧完全限定片段(例如，email.example.com 可以将其设置为 example.com，但不能设置为 google.com。）我们使用一个事实来捕获关于子域的规则：

// 脚本只能将域属性设置为其主机名的右侧完全限定片段
fact setDomainRule {
  all d: Document | d.src.host in (d.domain.Time).subsumes
}

如果没有此规则，任何站点都可以将 document.domain 属性设置为任何值，这意味着，例如，恶意站点可以将域属性设置为你的银行域，在嵌套页面中加载你的银行帐户，并且（假设银行页面已设置其域属性）读取你银行页面的 DOM。

让我们回到 SOP 的原始定义，并放宽其对 DOM 访问的限制，以便考虑 document.domain 属性的影响。如果两个脚本将属性设置为相同的值，并且它们具有相同的协议和端口，那么这两个脚本可以相互交互（即，读取和写入彼此的 DOM）。

fact domSop {
  -- 对于每个成功的读/写 DOM 操作，
    all o: ReadDom + WriteDom | let target = o.doc, caller = o.from.context |
        -- 调用文档和目标文档来自同一来源，或
        origin[target] = origin[caller] or
        -- --两个文档的域属性都已修改
        (target + caller in (o.prevs <: SetDomain).doc and
            -- ...它们已匹配源的值。
            currOrigin[target, o.start] = currOrigin[caller, o.start])
}

这里，currOrigin[d, t] 是一个函数，它返回文档 d 的源，属性document.domain 在时间 t 将其作为其主机名。

值得指出的是，两个文档的 document.domain 属性必须在加载到浏览器后的某个时间进行明确设置。假设文档 A 是从 example.com 加载的，而 calendar.example.com 中的文档 B 的域属性被修改为 example.com。即使这两个文档现在具有相同的域属性，它们也无法相互交互，除非文档 A 也明确地将其属性设置为 example.com。起初，这似乎是一种相当奇怪的行为。然而，没有这一点，各种各样的坏事都可能发生。例如，站点可能会受到来自其子域的跨站点脚本攻击：文档 B 中的恶意脚本可能会将其域属性修改为example.com并操纵文档 A 的 DOM，即使后者从未打算与文档 B 交互。

分析：既然我们已经放宽了 SOP，允许在某些情况下进行跨源通信，SOP 的安全保障是否仍然有效？让我们让 Alloy 分析器告诉我们，攻击者是否会滥用 document.domain 属性来访问或篡改用户的敏感数据。

事实上，考虑到 SOP 的新的、宽松的定义，分析器生成了机密性属性的反例场景：

check Confidentiality for 5

该场景包括五个步骤；前三个步骤显示 document.domain 的典型用法，其中来自不同源的两个文档 CalendarPage 和 InboxPage 通过将其域属性设置为公共值（ExampleDomain）进行通信。最后两个步骤引入了另一个文档 BlogPage，该文档已被恶意脚本破坏，该脚本试图访问其他两个文档的内容。

在场景开始时，InboxPage 和 CalendarPage 具有两个不同值的域属性（分别为 EmailDomain 和 ExampleDomain），因此浏览器将阻止它们访问彼此的 DOM。文档中运行的脚本（InboxScript 和 CalendarScript）分别执行 SetDomain 操作，以将其域属性修改为ExampleDomain（这是允许的，因为 ExampleDomain 是原始域的超级域）。

fig-setdomain-1a.png

fig-setdomain-1b.png

完成此操作后，它们现在可以通过执行 ReadDom 或 WriteDom 操作来访问彼此的 DOM。

fig-setdomain-1c.png

请注意，当你将 email.example.com 和 calendar.example.com 的域设置为 example.com 时，你不仅允许这两个页面相互通信，还允许 example.com 作为超级域的任何其他页面（例如 blog.example.com）。攻击者也意识到了这一点，并构造了一个在攻击者的博客页面（BlogPage）内运行的特殊脚本（EvilScript）。在下一步中，脚本执行 setdomain操作，将 BlogPage 的域属性修改为 ExampleDomain。

fig-setdomain-2a.png

既然 BlogPage 与其他两个文档具有相同的域属性，它就可以成功地执行 ReadDOM 操作来访问它们的内容。

fig-setdomain-2b.png

此攻击指出了用于跨源通信的域属性方法的一个关键弱点：使用此方法的应用程序的安全性仅与共享同一基本域的所有页面中最薄弱的链接一样强。我们将很快讨论另一种称为 PostMessage 的方法，它可以用于更一般的跨源通信，同时也更安全。

带填充的JSON（JSONP）

在引入 CORS（我们将很快讨论）之前，JSONP 可能是绕过 XMLHttpRequest 上的 SOP 限制的最流行的技术，至今仍被广泛使用。JSONP 利用了这样一个事实，即 HTML 中的脚本包含标记（即<script>）不受 SOP* 的约束；也就是说，你可以包含来自任何 URL 的脚本，并且浏览器可以在当前文档中随时执行该脚本：

（*如果没有此豁免，就不可能从其他域加载 JavaScript 库，如JQuery）

<script src="http://www.example.com/myscript.js"></script>

脚本标记可以用来获取代码，但是我们如何使用它从不同的域接收任意数据（例如 JSON 对象）？问题是浏览器希望 src 的内容是一段 JavaScript 代码，因此简单地将其指向数据源（例如 JSON 或 HTML 文件）会导致语法错误。

一种解决方法是将所需数据包装在一个字符串中，浏览器将该字符串识别为有效的 JavaScript 代码；此字符串有时称为 padding（因此名为“带填充的 JSON”）。此填充可以是任意 JavaScript 代码，但按照惯例，它是要对响应数据执行的回调函数（已在当前文档中定义）的名称：

<script src="http://www.example.com/mydata?jsonp=processData"></script>

www.example.com 上的服务器将其识别为 JSONP 请求，并将请求的数据包装在 JSONP 参数中：

processData(mydata)

它是一个有效的 JavaScript 语句（即函数“processData”在值“mydata”上的应用），由浏览器在当前文档中执行。

在我们的模型中，JSONP 被建模为一种 HTTP 请求，在字段填充中包含回调函数的标识符。在接收到 JSONP 请求后，服务器返回一个响应，该响应将请求的资源（payload）包装在回调函数（cb）中。

sig CallbackID {}  // 回调函数的标识符
// 由于 <script> 标记而发送的请求
sig JsonpRequest in BrowserHttpRequest {
  padding: CallbackID
}{
  response in JsonpResponse
}
sig JsonpResponse in Resource {
  cb: CallbackID,
  payload: Resource
}

当浏览器收到响应时，它对有效负载执行回调函数：

sig JsonpCallback extends EventHandler {
  cb: CallbackID,
  payload: Resource
}{
  causedBy in JsonpRequest
  let resp = causedBy.response | 
    cb = resp.@cb and
    -- JSONP请求的结果作为参数传递给回调
    payload = resp.@payload
}

（EventHandler 是一种特殊类型的调用，必须在另一个调用之后的某个时间发生，由 causedBy 表示；我们将使用事件处理程序对脚本为响应浏览器事件而执行的操作进行建模。）

请注意，执行的回调函数与响应中包含的回调函数相同（cb = resp.@cb），但不一定与原始 JSONP 请求中的填充相同。换句话说，为了让 JSONP 通信正常工作，服务器负责正确地构造一个响应，其中包含原始填充作为回调函数（即，确保 JsonRequest.padding = JsonpResponse.cb）。原则上，服务器可以选择包含任何回调函数（或任何一段 JavaScript），包括与请求中的填充无关的回调函数。这突出了 JSONP 的一个潜在风险：接受 JSONP 请求的服务器必须是可信和安全的，因为它能够执行客户端文档中的任何 JavaScript 代码。

分析：使用 Alloy 分析器检查机密性属性会返回一个反例，显示 JSONP 的一个潜在安全风险。在此场景中，日历应用程序（CalendarServer）使用 JSONP 端点（GetSchedule）将其资源提供给第三方站点。为了限制对资源的访问，CalendarServer 仅在请求包含正确标识该用户的 cookie 时，才返回带有用户计划的响应。

注意，一旦服务器提供 HTTP 端点作为 JSONP 服务，任何人都可以向它发出 JSONP 请求，包括恶意站点。在这个场景中，EvilServer 的广告横幅页面包含一个 script 标记，该标记导致一个 GetSchedule请求，并使用一个名为 Leak 的回调函数作为填充。通常，AdBanner 的开发人员无法直接访问 CalendarServer的受害用户会话 cookie（MyCookie）。但是，由于 JSONP 请求被发送到 CalendarServer，浏览器会自动将 MyCookie 作为请求的一部分；CalendarServer 接收到带有 MyCookie 的 JSONP 请求后，将返回包装在填充 Leak 中的受害者资源（MySchedule）。

fig-jsonp-1.png

在下一步中，浏览器将 JSONP 响应解释为对 Leak（MySchedule） 调用。攻击的剩余部分很简单；Leak 可以简单地编程为将输入参数转发到 EvilServer，从而允许攻击者访问受害者的敏感信息。

fig-jsonp-2.png

此攻击是跨站点请求伪造（CSRF）的一个示例，显示了 JSONP 的固有弱点；Web 上的任何站点都可以通过包含 <script> 标记并访问填充中的有效负载来发出 JSONP 请求。可以通过两种方式降低风险：（1）确保 JSONP 请求从不返回敏感数据，或者（2）使用另一种机制代替 cookie（例如，秘密令牌）来授权请求。

PostMessage

PostMessage 是 HTML5 中的一项新功能，它允许来自两个文档（可能源不同）的脚本相互通信。它提供了一种比设置域属性更严格的方法，但也带来了自身的安全风险。

PostMessage 是一个浏览器 API 函数，它接受两个参数：（1）要发送的数据（message）和（2）接收消息的文档的源（targetOrigin）：

sig PostMessage extends BrowserOp {
  message: Resource,
  targetOrigin: Origin
}

要从另一个文档接收消息，接收文档会注册一个事件处理程序，浏览器会根据 PostMessage 调用该事件处理程序：

sig ReceivedMessage extends EventHandler {
    data: Resource,
    srcOrigin: Origin
}{
    causedBy in PostMessage
    -- “ReceiveMessage”事件被发送到具有正确上下文的脚本
    origin[to.context.src] = causedBy.targetOrigin
    -- 消息匹配
    data = causedBy.@message
    --发送方脚本的源作为“srcOrigin”参数提供
    srcOrigin = origin[causedBy.@from.context.src]
}

浏览器向 ReceiveMessage 传递两个参数：与正在发送的消息相对应的资源（data）和发送方文档的源（srcOrigin）。签名事实包含四个约束，以确保每个 ReceiveMessage 相对于其相应的 PostMessage 格式正确。

分析：再次询问 Alloy 分析器 PostMessage 是否是执行跨源通信的安全方式。这一次，分析器返回 Integrity 属性的反例，这意味着攻击者能够利用 PostMessage 中的弱点将恶意数据引入受信任的应用程序。

请注意，默认情况下，PostMessage 机制不限制允许发送 PostMessage 的用户；换句话说，任何文档都可以向另一个文档发送消息，只要后者已注册 ReceiveMessage 处理程序。例如，在以下由 Alloy 生成的实例中，在 AdBanner 中运行的 EvilScript 向目标源为 EmailDomain 的文档发送恶意 PostMessage。

fig-postmessage-1.png

然后，浏览器将此消息转发到具有相应源（在本例中为 InboxPage）的文档。除非 InboxScript 专门检查 srcOrigin 的值以过滤掉不需要的源的消息，否则 InboxPage 将接受恶意数据，可能导致进一步的安全攻击(例如，它可能嵌入一段 JavaScript 来执行 XSS 攻击。）如下图所示。

fig-postmessage-2.png

如本例所示，PostMessage 在默认情况下是不安全的，接收文档有责任额外检查 srcOrigin 参数，以确保消息来自可靠的文档。不幸的是，在实践中，许多网站忽略了此检查，从而使恶意文档能够作为 PostMessage^[1] 的一部分插入错误内容。

然而，省略源检查可能不仅仅是程序员无知的结果。对传入的 PostMessage 执行适当的检查可能很棘手；在某些应用程序中，很难预先确定预期从中接收消息的可信源列表(在某些应用程序中，此列表甚至可能会动态更改。）这再次凸显了安全性和功能性之间的紧张关系：PostMessage 可用于安全的跨源通信，但只有在已知可信源白名单的情况下。

跨源资源共享（CORS）

跨源资源共享（CORS）是一种允许服务器与来自不同源的站点共享其资源的机制。特别是，来自一个源的脚本可以使用 CORS 向具有不同源的服务器发出请求，从而有效地绕过 SOP 对跨源 Ajax 请求的限制。

简单地说，典型的 CORS 过程包括两个步骤：（1）希望从外部服务器访问资源的脚本在其请求中包括一个“源”头，该头指定脚本的源；（2）服务器包括一个“访问控制允许源”头作为其响应的一部分，指示允许访问服务器资源的一组源。通常，在没有 CORS 的情况下，浏览器首先会阻止脚本根据 SOP 发出跨源请求。但是，在启用 CORS 的情况下，浏览器允许脚本发送请求并访问其响应，但前提是“源”是“访问控制允许源”中指定的源之一。

（CORS 还包括 preflight 请求的概念（此处未讨论），以支持 GET 和 POST 之外的复杂类型的跨源请求。）

在 Alloy 中，我们将 CORS 请求建模为一种特殊类型的 XmlHttpRequest，具有两个额外字段 origin 和 allowedOrigins：

sig CorsRequest in XmlHttpRequest {
    -- 来自客户端的请求中的“origin”报文头
    origin: Origin
    -- 服务器响应中的“"access-control-allow-origin”报文头
    allowedOrigins: set Origin
}{
    from in Script
}

然后，我们使用 Alloy 事实 corsRule 来描述什么构成有效的 CORS 请求：

fact corsRule {
    all r: CorsRequest |
        -- CORS请求的原始报文头与脚本上下文匹配
        r.origin = origin[r.from.context.src] and
        -- 指定的源是允许的源之一
        r.origin in r.allowOrigins
}

分析： CORS是否会被滥用，从而使攻击者危害受信任站点的安全？当出现提示时，Alloy 分析器返回 Confidentiality 属性的简单反例。

在这里，日历应用程序的开发人员决定使用 CORS 机制与其他应用程序共享一些资源。不幸的是，CalendarServer 配置为在 CORS 响应中返回 access-control-allow-origin 报文头的 Origin（表示所有源的集合）。因此，允许来自任何源（包括 EvilDomain）的脚本向 CalendarServer 发出跨站点请求并读取其响应。

fig-cors.png

这个例子强调了开发人员在 CORS 中犯的一个常见错误：使用通配符值“*”作为“access-control-allow-origin”报文头的值，允许任何站点访问服务器上的资源。如果资源被认为是公共的并且任何人都可以访问，那么这种访问模式是合适的。然而，事实证明，许多站点甚至将“*”用作私有资源的默认值，无意中允许恶意脚本通过 CORS 请求访问它们^[2]。

为什么开发人员会使用通配符？事实证明，指定允许的源可能很棘手，因为在设计时可能不清楚哪些源应该在运行时被授予访问权限（类似于上面讨论的 PostMessage 问题）。例如，服务可以允许第三方应用程序动态订阅其资源。

总结

在本文中，我们着手构建一个文档，通过用一种称为 Alloy 的语言构建一个策略模型，提供对 SOP 及其相关机制的清晰理解。我们的 SOP 模型不是传统意义上的实现，不能部署使用，这与其他章节中显示的工件不同。相反，我们希望展示“敏捷建模”方法背后的关键要素：（1）从系统的小型抽象模型开始，并在必要时逐步添加细节，（2）指定系统预期满足的属性，（3）应用严格的分析来探索系统设计中的潜在缺陷。当然，本章是在 SOP 首次引入之后很久才编写的，但我们相信，如果在系统设计的早期阶段进行，这种建模可能会更加有益。

除了 SOP 之外，Alloy 还被用于对网络协议、语义 Web、字节码安全、电子投票和医疗系统等不同领域的各种系统进行建模和推理。对于这些系统，Alloy 的分析发现了设计缺陷和 BUG，在某些情况下，开发人员多年来一直没有发现这些缺陷和 BUG。我们邀请我们的读者访问 Alloy 页面，尝试构建他们喜爱的系统模型！

附录：在 Alloy 中重复使用模块

如本文前面所述，Alloy 不对所建模系统的行为进行假设。由于缺乏内置的范例，用户可以使用基本语言结构的一小部分核心对广泛的建模习惯用法进行编码。例如，我们可以将系统指定为状态机、具有复杂不变量的数据模型、具有全局时钟的分布式事件模型，或者任何最适合当前问题的习惯用法。常用习惯用法可以作为通用模块捕获，并在多个系统中重用。

在我们的 SOP 模型中，我们将系统建模为一组端点，这些端点通过一个或多个 call 相互通信。由于 call 是一个相当通用的概念，我们将其描述封装在一个单独的 Alloy 模块中，从依赖它的其他模块中导入——类似于编程语言中的标准库：

module call[T] 

在这个模块声明中，T 表示一个类型参数，该参数可以实例化为导入模块时提供的具体类型。我们将很快看到如何使用此类型参数。

通常可以方便地将系统执行描述为在全局时间范围内发生，这样我们就可以将调用描述为发生在彼此之前或之后（或同时发生）。为了表示时间的概念，我们引入了一个新的签名，称为 Time：

open util/ordering[Time] as ord
sig Time {}

在 Alloy 中，util/ordering 是一个内置模块，它对类型参数施加总顺序，因此通过导入 ordering[Time]，我们可以获得一组 Time 对象，其行为类似于其他全顺序集（例如，自然数）。

请注意，Time 没有什么特别之处；我们可以将其命名为任何其他方式（例如，Step 或 State），它根本不会改变模型的行为。我们在这里所做的就是在关系中使用一个额外的列，作为表示系统执行中不同点的字段内容的一种方式；例如，Browser 签名中的 cookies 。从这个意义上讲，Time对象只是用作索引的助手对象。

每个调用发生在两个时间点之间，即 start 和 end，并与发送方（由 from 表示）和接收方（to 表示）关联：

abstract sig Call { start, end: Time, from, to: T } 

回想一下，在我们对 HTTP 请求的讨论中，我们通过将端点作为其类型参数传递来导入模块调用。结果，参数类型 T 被实例化为 Endpoint，我们获得了一组与一对发送方和接收方端点关联的 Call 对象。一个模块可以多次导入；例如，我们可以声明一个名为 UnixProcess 的签名，并实例化模块 call 以获得从一个 Unix 进程发送到另一个 Unix 进程的一组不同的 Call 对象。

1. Sooel Son 和 Vitaly Shmatikov。The Postman Always Rings Twice: Attacking and Defending postMessage in HTML5 Websites. Network and Distributed System Security Symposium (NDSS), 2013。 ↩

2. Sebastian Lekies, Martin Johns, 和 Walter Tighzert. The State of the Cross-Domain Nation. Web 2.0 Security and Privacy (W2SP), 2011。 ↩