姜恩淑是麻省理工学院软件设计小组的博士候选人和成员。他于 2010 年获得麻省理工学院计算机科学硕士学位，并于 2007 年获得滑铁卢大学软件工程学士学位。他的研究项目专注于开发软件建模和验证的工具和技术，并将其应用于安全和安全关键系统。
圣地亚哥·佩雷斯·德·罗索是麻省理工学院软件设计小组的博士生。他于 2015 年获得麻省理工学院计算机科学硕士学位，并于 2011 年获得 ITBA 的本科学位。他曾在 Google 工作，开发框架和工具以提高工程师的生产力（2012 年）。他目前大部分时间都在思考设计和版本控制。
丹尼尔·杰克逊是麻省理工学院电气工程与计算机科学系教授，并领导计算机科学与人工智能实验室的软件设计小组。他于 1984 年获得牛津大学物理学硕士学位，并于 1988 年和 1992 年分别获得麻省理工学院计算机科学硕士和博士学位。他曾是 Logica UK Ltd. 的软件工程师（1984-1986 年），卡内基梅隆大学计算机科学助理教授（1992-1997 年），并自 1997 年起在麻省理工学院任职。他对软件工程有着广泛的兴趣，尤其是在开发方法、设计和规范、形式化方法以及安全关键系统方面。
同源策略 (SOP) 是每个现代浏览器安全机制的重要组成部分。它控制浏览器中运行的脚本何时可以相互通信（大致上，当它们源自同一网站时）。SOP 最初是在 Netscape Navigator 中引入的，现在在 Web 应用程序的安全中发挥着至关重要的作用；如果没有它，恶意黑客就更容易浏览您在 Facebook 上的私人照片、阅读您的电子邮件或清空您的银行账户。
但是，SOP 远非完美。有时，它过于严格；在某些情况下（例如 Mashup），来自不同来源的脚本应该能够共享资源，但无法做到。在其他时候，它又不够严格，留下了一些可以使用跨站点请求伪造等常见攻击进行利用的特殊情况。此外，SOP 的设计多年来一直在不断发展，令许多开发人员感到困惑。
本章的目标是捕捉这一重要但常常被误解的功能的本质。特别是，我们将尝试回答以下问题
考虑到涉及的部分的复杂性——Web 服务器、浏览器、HTTP、HTML 文档、客户端脚本等等，全面涵盖 SOP 是一项艰巨的任务。我们很可能会陷入所有这些部分的细枝末节中（并在到达 SOP 之前就消耗完我们的 500 行）。但是，如果我们不表示关键细节，我们怎么能希望做到精确呢？
本章与本书中的其他章节略有不同。我们不会构建一个可运行的实现，而是构建一个可执行模型，作为 SOP 的简单而精确的描述。与实现一样，模型可以执行以探索系统的动态行为，但与实现不同的是，模型省略了可能妨碍理解基本概念的底层细节。
我们采用的方法可能被称为“敏捷建模”，因为它与敏捷编程有相似之处。我们增量工作，一点一点地组装模型。我们不断发展的模型在任何时候都是可以执行的。我们在进行过程中制定和运行测试，以便到最后，我们不仅拥有模型本身，还拥有它满足的一系列属性。
为了构建此模型，我们使用Alloy，这是一种用于建模和分析软件设计的语言。Alloy 模型不能以程序执行的传统意义上执行。相反，一个模型可以（1）模拟以产生一个实例，它表示系统的一个有效场景或配置，以及（2）检查以查看模型是否满足所需的属性。
尽管存在上述相似之处，但敏捷建模在一点上与敏捷编程不同：虽然我们将运行测试，但实际上我们不会编写任何测试。Alloy 的分析器会自动生成测试用例，而只需要提供要检查的属性即可。不用说，这节省了很多麻烦（和文本）。分析器实际上执行所有可能的测试用例，直到某个特定大小（称为范围）；这通常意味着生成最多包含一定数量对象的全部初始状态，然后选择要应用的操作和参数，最多执行一定数量的步骤。由于执行了如此多的测试（通常为数十亿次），并且涵盖了状态可以采用的所有可能配置（尽管在范围内），因此这种分析往往比传统测试更有效地暴露错误（有时被称为“有界验证”）。
由于 SOP 在浏览器、服务器、HTTP 等环境中运行，因此完整的描述将不堪重负。因此，我们的模型（像所有模型一样）抽象了不相关的方面，例如网络数据包如何构建和路由。但它也简化了一些相关的方面，这意味着模型无法完全解释所有可能的安全漏洞。
例如，我们将 HTTP 请求视为远程过程调用，忽略了对请求的响应可能乱序到达的事实。我们还假设 DNS（域名服务）是静态的，因此我们无法考虑 DNS 绑定在交互过程中发生更改的攻击。原则上，虽然可以扩展我们的模型以涵盖所有这些方面，但安全分析的本质是，任何模型（即使它表示整个代码库）都不能保证是完整的。
以下是我们将如何继续进行 SOP 模型的顺序。我们将首先构建三个关键组件的模型，以便我们能够讨论 SOP：HTTP、浏览器和客户端脚本。我们将在此基础上构建基本模型，以定义 Web 应用程序安全的含义，然后将 SOP 引入作为一种试图实现所需安全属性的机制。
然后我们将看到，SOP 有时可能过于严格，妨碍了 Web 应用程序的正常运行。因此，我们将介绍四种常用的绕过策略强加的限制的技术。
随意按任何顺序浏览各个部分。如果您不熟悉 Alloy，我们建议从前三个部分（HTTP、浏览器和脚本）开始，因为它们介绍了建模语言的一些基本概念。在阅读本章的过程中，我们也鼓励您在 Alloy Analyzer 中试用这些模型；运行它们，探索生成的场景，尝试进行修改并查看它们的影响。它是免费下载。
构建 Alloy 模型的第一步是声明一些对象集。让我们从资源开始
sig Resource {}关键字sig将此标识为 Alloy 的签名声明。这引入了一组资源对象；就像一个没有实例变量的类的对象一样，将它们视为具有标识但没有内容的块。当分析运行时，将确定此集合，就像面向对象语言中的类在程序执行时表示一组对象一样。
资源由 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（可以读作“小于或等于一个”）表示每个 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 映射，由表达式Dns.map给出。同样，与服务资源一样，这可能是动态的（实际上，有一些已知的安全攻击依赖于在交互过程中更改 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签名时，我们发现它包含了调用的一些通用特征，即它们是从特定的事物到特定的事物。因此，我们实际上编写了一个小的 Alloy 模块来声明Call签名，并且为了在这里使用它，我们需要导入它。
open call[Endpoint]这是一个多态模块，因此它使用Endpoint实例化，Endpoint是调用来源和目标事物的集合。（该模块的完整内容见附录：在 Alloy 中重用模块。）
在HttpRequest中的字段声明之后是一组约束。这些约束中的每一个都适用于 HTTP 请求集的所有成员。这些约束表示（1）每个请求都来自一个客户端，以及（2）每个请求都发送到 DNS 映射下 URL 主机指定的服务器之一。
Alloy 的一个突出特点是，无论模型多么简单或详细，都可以随时执行它以生成系统示例。让我们使用run命令来请求 Alloy Analyzer 执行我们迄今为止的 HTTP 模型。
run {} for 3 -- generate an instance with up to 3 objects of every signature type一旦分析器找到系统的一个可能实例，它就会自动生成该实例的图表，如图 17.1所示。
图 17.1 - 一个可能的实例
此实例显示一个客户端（由节点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命令，分析器将探索系统的所有可能行为（直至指定的边界），并且当它找到一个违反该属性的行为时，会将该实例显示为反例，如图 17.2和图 17.3所示。
图 17.2 - 时间 0 时的反例
图 17.3 - 时间 1 时的反例
此反例再次显示了客户端发出的 HTTP 请求，但使用了两个不同的服务器。（在 Alloy 可视化工具中，相同类型的对象通过在其名称后面附加数字后缀来区分；如果给定类型只有一个对象，则不添加后缀。快照图中出现的每个名称都是一个对象的名称。因此——也许一开始会令人困惑——名称Domain、Path、Resource、Url都指的是单个对象，而不是类型。）
请注意，虽然 DNS 将Domain映射到Server0和Server1（实际上，这是负载均衡的常见做法），但只有Server1将Path映射到资源对象，导致HttpRequest1导致空响应：我们模型中的另一个错误。为了解决这个问题，我们添加一个 Alloy事实，记录 DNS 映射到单个主机的任何两个服务器都提供相同的资源集。
fact ServerAssumption {
all s1, s2: Server |
(some Dns.map.s1 & Dns.map.s2) implies s1.resources = s2.resources
}在添加此事实后，当我们重新运行check命令时，分析器不再报告该属性的任何反例。这并不意味着该属性已被证明为真，因为在更大的范围内可能存在反例。但该属性不太可能是假的，因为分析器已经测试了每个类型包含 3 个对象的所有可能实例。
但是，如果需要，我们可以使用更大的范围重新运行分析以提高置信度。例如，使用 10 的范围运行上述检查仍然不会产生任何反例，这表明该属性可能有效。但是，请记住，在给定更大的范围时，分析器需要测试更多数量的实例，因此完成分析可能需要更长的时间。
现在让我们将浏览器引入我们的模型。
sig Browser extends Client {
documents: Document -> Time,
cookies: Cookie -> Time,
}这是我们第一个带有动态字段的签名的示例。Alloy 没有内置的时间或行为概念，这意味着可以使用各种习惯用法。在此模型中，我们使用了一种常见的习惯用法，其中您引入Time的概念，并将其作为每个时变字段的最后一列。例如，表达式b.cookies.t表示在特定时间t存储在浏览器b中的 Cookie 集。同样，documents字段将一组文档与给定时间的每个浏览器相关联。（有关我们如何建模动态行为的更多详细信息，请参阅附录：在 Alloy 中重用模块。）
文档是从对 HTTP 请求的响应中创建的。如果例如用户关闭选项卡或浏览器，它们也可以被销毁，但我们将其排除在模型之外。文档具有 URL（文档来源的 URL）、一些内容（DOM）和一个域名。
sig Document {
src: Url,
content: Resource -> Time,
domain: Domain -> Time
}后两个字段中包含Time列告诉我们它们可以随时间变化，而第一个字段（src，表示文档的源 URL）中省略它表示源 URL 是固定的。
为了模拟 HTTP 请求对浏览器的影响，我们引入了新的签名，因为并非所有 HTTP 请求都将源自浏览器级别；其余的将来自脚本。
sig BrowserHttpRequest extends HttpRequest {
doc: Document
}{
-- the request comes from a browser
from in Browser
-- the cookies being sent exist in the browser at the time of the request
sentCookies in from.cookies.start
-- every cookie sent must be scoped to the url of the request
all c: sentCookies | url.host in c.domains
-- a new document is created to display the content of the response
documents.end = documents.start + from -> doc
-- the new document has the response as its contents
content.end = content.start ++ doc -> response
-- the new document has the host of the url as its domain
domain.end = domain.start ++ doc -> url.host
-- the document's source field is the url of the request
doc.src = url
-- new cookies are stored by the browser
cookies.end = cookies.start + from -> sentCookies
}这种请求有一个新字段doc，表示在浏览器中根据请求返回的资源创建的文档。与HttpRequest一样，行为被描述为一组约束。其中一些说明了调用何时可以发生：例如，调用必须来自浏览器。一些约束调用的参数：例如，Cookie 必须正确地限定范围。还有一些约束效果，使用将调用后的关系值与其之前的值相关联的常用习惯用法。
例如，要理解约束documents.end = documents.start + from -> doc，请记住documents是在浏览器、文档和时间上具有 3 列的关系。字段start和end来自Call的声明（我们还没有看到，但在末尾的列表中包含），并表示调用开始和结束的时间。表达式documents.end给出调用结束时浏览器到文档的映射。因此，此约束表示调用后，映射是相同的，除了表中将from映射到doc的新条目。
一些约束使用++关系覆盖运算符：e1 ++ e2包含e2的所有元组，此外，还包含e1的任何元组，其第一个元素不是e2中的元组的第一个元素。例如，约束content.end = content.start ++ doc -> response表示调用后，content映射将更新为将doc映射到response（覆盖doc的任何先前映射）。如果我们使用联合运算符+，则在后状态下，同一文档可能会（错误地）映射到多个资源。
接下来，我们将基于 HTTP 和浏览器模型引入客户端脚本，它们表示在浏览器文档（context）中执行的代码片段（通常是 JavaScript）。
sig Script extends Client { context: Document }脚本是一个动态实体，可以执行两种不同的操作：（1）它可以发出 HTTP 请求（即 Ajax 请求），以及（2）它可以执行浏览器操作来操作文档的内容和属性。客户端脚本的灵活性是 Web 2.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 Analyzer 会生成一个与模型中系统描述一致的场景（如果存在）。默认情况下，分析器会任意选择任何一个可能的系统场景（直至指定的边界），并在场景中为签名实例（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, --- arguments and return data of this call
}{
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 {
-- Set of data that this component initially owns
accesses: Data -> Time
}{
all d: Data, t: Time - first |
-- This endpoint can only access a piece of data "d" at time "t" only when
d -> t in accesses implies
-- (1) It already had access in the previous time step, or
d -> t.prev in accesses or
-- there is some call "c" that ended at "t" such that
some c: Call & end.t |
-- (2) the endpoint receives "c" that carries "d" as one of its arguments or
c.to = this and d in c.args or
-- (3) the endpoint sends "c" that returns "d"
c.from = this and d in c.returns
}我们还需要限制模块可以作为调用参数或返回值提供的数据元素。否则，我们可能会遇到模块可以使用其无法访问的参数进行调用的奇怪场景。
sig DataflowCall in Call { ... } {
-- (1) Any arguments must be accessible to the sender
args in from.accesses.start
-- (2) Any data returned from this call must be accessible to the receiver
returns in to.accesses.start
}现在我们有了描述系统不同部分之间数据流的方法，我们（几乎）可以陈述我们关心的安全属性了。但请记住，机密性和完整性是上下文相关的概念；只有当我们可以谈论系统中的一些代理是可信的（或恶意的）时，这些属性才有意义。同样，并非所有信息都同等重要：我们需要区分我们认为是关键的或恶意的（或两者都不是）的数据元素
sig TrustedModule, MaliciousModule in DataflowModule {}
sig CriticalData, MaliciousData in Data {}然后，机密性属性可以陈述为对关键数据流入系统不可信部分的断言
// No malicious module should be able to access critical data
assert Confidentiality {
no m: Module - TrustedModule, t: Time |
some CriticalData & m.accesses.t
}完整性属性是机密性的对偶
// No malicious data should ever flow into a trusted module
assert Integrity {
no m: TrustedModule, t: Time |
some MaliciousData & m.accesses.t
}威胁模型描述了攻击者可能执行的一组操作，以试图破坏系统的安全属性。构建威胁模型是任何安全系统设计中的一个重要步骤；它使我们能够识别我们对系统及其环境做出的（可能无效的）假设，并确定需要缓解的不同类型风险的优先级。
在我们的模型中，我们考虑一个可以充当服务器、脚本或客户端的攻击者。作为服务器，攻击者可能会设置恶意网页以诱使毫无戒心的用户访问，这些用户反过来可能会在 HTTP 请求的一部分中无意中将敏感信息发送给攻击者。攻击者可能会创建一个恶意脚本，该脚本调用 DOM 操作以从其他页面读取数据并将这些数据中继到攻击者的服务器。最后，作为客户端，攻击者可能会模仿普通用户并向服务器发送恶意请求，试图访问用户的数据。我们不考虑窃听不同网络端点之间连接的攻击者；尽管这在实践中是一种威胁，但 SOP 并非旨在防止它，因此它超出了我们模型的范围。
现在我们已经定义了安全属性和攻击者的行为，让我们展示如何使用 Alloy 分析器自动检查这些属性即使在攻击者存在的情况下也成立。当提示使用check命令时，分析器会探索系统中所有可能的数据流跟踪，并生成一个反例（如果存在），以演示断言是如何被违反的
check Confidentiality for 5例如，当检查我们示例应用程序的模型是否满足机密性属性时，分析器会生成图 17.4和图 17.5中所示的场景，该场景显示了EvilScript如何访问关键数据（MyInboxInfo）。
图 17.4 - 时间 0 时的机密性反例
图 17.5 - 时间 1 时的机密性反例
此反例涉及两个步骤。在第一步（图 17.4）中，在EvilDomain的AdBanner中执行的EvilScript读取InboxPage的内容，该内容源自EmailDomain。在下一步（图 17.5）中，EvilScript通过发出XmlHtttpRequest调用将相同的内容（MyInboxInfo）发送到EvilServer。这里问题的核心在于，在一个域下执行的脚本能够读取来自另一个域的文档的内容；正如我们将在下一节中看到的，这正是 SOP 设计用于防止的场景之一。
单个断言可能有多个反例。考虑图 17.6，它显示了系统可能违反机密性属性的不同方式。
图 17.6 - 另一个机密性违规
在这种情况下，EvilScript不是读取收件箱页面的内容，而是直接向EmailServer发出GetInboxInfo请求。请注意，该请求包含一个 cookie（MyCookie），该 cookie 的范围与目标服务器相同。这可能很危险，因为如果 cookie 用于表示用户的身份（例如，会话 cookie），则EvilScript可以有效地假装是用户并欺骗服务器以响应用户的私人数据（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下是不可能的，因为Script不允许在来自不同源的文档上调用ReadDom。
策略的第二部分指出，脚本不能向服务器发送 HTTP 请求，除非其上下文与目标 URL 的源相同——有效地防止了第二个脚本场景等情况。
fact xmlHttpReqSop {
all x: XmlHttpRequest | origin[x.url] = origin[x.from.context.src]
}正如我们所看到的，SOP 的设计是为了防止可能由恶意脚本的操作引起的两种类型的漏洞；如果没有它，Web 将比今天危险得多。
然而，事实证明，SOP 可能过于严格。例如，有时您确实希望允许不同源的两个文档之间进行通信。根据上述源的定义，来自foo.example.com的脚本将无法读取bar.example.com的内容，或向www.example.com发送 HTTP 请求，因为这些都被视为不同的主机。
为了在必要时允许某种形式的跨源通信，浏览器实现了各种放宽 SOP 的机制。其中一些比另一些更经过深思熟虑，并且一些存在缺陷，如果使用不当，可能会破坏 SOP 的安全优势。在以下各节中，我们将描述这些机制中最常见的一些，并讨论其潜在的安全缺陷。
SOP 是功能与安全之间紧张关系的一个典型例子；我们希望确保我们的网站强大且功能齐全，但保护它的机制有时会妨碍我们。确实，当 SOP 最初引入时，开发人员在构建合法使用跨域通信（例如，Mashup）的网站时遇到了麻烦。
在本节中，我们将讨论 Web 开发人员设计和经常用来绕过 SOP 施加的限制的四种技术：（1）document.domain属性放松；（2）JSONP；（3）PostMessage；和（4）CORS。这些都是有价值的工具，但如果使用不当，可能会使 Web 应用程序容易受到 SOP 最初旨在阻止的攻击类型的影响。
这四种技术都出乎意料地复杂，如果详细描述，每种技术都值得用一章来讲解。因此，这里我们只简要介绍它们的工作原理、引入的潜在安全问题以及如何防止这些问题。特别是，我们将要求 Alloy Analyzer 检查每种技术是否可能被攻击者滥用，从而破坏我们之前定义的两个安全属性。
check Confidentiality for 5
check Integrity for 5基于分析器生成的逆例的见解，我们将讨论安全使用这些技术而不陷入安全陷阱的指南。
作为我们列表中的第一种技术，我们将研究使用document.domain属性作为绕过 SOP 的方法。此技术背后的想法是，通过将document.domain属性设置为相同的值，允许来自不同来源的两个文档访问彼此的 DOM。例如，来自email.example.com的脚本可以通过将两个文档中的脚本的document.domain属性都设置为example.com来读取或写入来自calendar.example.com的文档的 DOM（假设这两个源 URL 具有相同的协议和端口）。
我们将设置document.domain属性的行为建模为一种称为SetDomain的浏览器操作。
// Modify the document.domain property
sig SetDomain extends BrowserOp { newDomain: Domain }{
doc = from.context
domain.end = domain.start ++ doc -> newDomain
-- no change to the content of the document
content.end = content.start
}newDomain字段表示应将属性设置为的值。不过，有一个需要注意的地方：脚本只能将其主机名的右侧、完全限定的片段设置为域属性。（例如，email.example.com可以将其设置为example.com，但不能设置为google.com。）我们使用一个事实来捕获有关子域的此规则。
// Scripts can only set the domain property to only one that is a right-hand,
// fully-qualified fragment of its hostname
fact setDomainRule {
all d: Document | d.src.host in (d.domain.Time).subsumes
}如果没有此规则，任何网站都可以将document.domain属性设置为任何值，这意味着，例如，恶意网站可以将域属性设置为您的银行域，在 iframe 中加载您的银行帐户，并（假设银行页面已设置其域属性）读取您的银行页面的 DOM。
让我们回到我们最初的 SOP 定义，并放宽其对 DOM 访问的限制，以考虑document.domain属性的影响。如果两个脚本将属性设置为相同的值，并且它们具有相同的协议和端口，则这两个脚本可以相互交互（即，读取和写入彼此的 DOM）。
fact domSop {
-- For every successful read/write DOM operation,
all o: ReadDom + WriteDom | let target = o.doc, caller = o.from.context |
-- (1) target and caller documents are from the same origin, or
origin[target] = origin[caller] or
-- (2) domain properties of both documents have been modified
(target + caller in (o.prevs <: SetDomain).doc and
-- ...and they have matching origin values.
currOrigin[target, o.start] = currOrigin[caller, o.start])
}这里，currOrigin[d, t]是一个函数，它返回文档d在时间t时的来源，其主机名为document.domain属性。
值得指出的是，这两个文档的document.domain属性必须在加载到浏览器后进行显式设置。假设文档 A 从example.com加载，而文档 B 从calendar.example.com加载，并且其域属性被修改为example.com。即使这两个文档现在具有相同的域属性，它们也无法相互交互，除非文档 A 也显式地将其属性设置为example.com。起初，这似乎是一种相当奇怪的行为。但是，如果没有它，可能会发生各种不好的事情。例如，一个网站可能会受到来自其子域的跨站点脚本攻击：文档 B 中的恶意脚本可能会将其域属性修改为example.com并操纵文档 A 的 DOM，即使后者从未打算与文档 B 交互。
分析：现在我们已经放宽了 SOP 以允许在特定情况下进行跨源通信，SOP 的安全保证是否仍然有效？让我们要求 Alloy Analyzer 告诉我们document.domain属性是否可能被攻击者滥用以访问或篡改用户的敏感数据。
事实上，鉴于 SOP 的新放宽定义，分析器为机密性属性生成了一个逆例场景。
check Confidentiality for 5此场景包括五个步骤；前三个步骤展示了document.domain的典型用法，其中来自不同来源的两个文档CalendarPage和InboxPage通过将其域属性设置为公共值（ExampleDomain）进行通信。最后两个步骤引入了另一个文档BlogPage，该文档已受到包含恶意脚本的攻击，该脚本试图访问其他两个文档的内容。
在场景开始时（图 17.7和图 17.8），InboxPage和CalendarPage具有两个不同值的域属性（分别为EmailDomain和ExampleDomain），因此浏览器将阻止它们访问彼此的 DOM。文档内运行的脚本（InboxScript和CalendarScript）分别执行SetDomain操作以将其域属性修改为ExampleDomain（这是允许的，因为ExampleDomain是原始域的超域）。
图 17.7 - 时间 0 时的跨源逆例
图 17.8 - 时间 1 时的跨源逆例
完成此操作后，它们现在可以通过执行ReadDom或WriteDom操作来访问彼此的 DOM，如图 17.9所示。
图 17.9 - 时间 2 时的跨源逆例
请注意，当您将email.example.com和calendar.example.com的域设置为example.com时，您不仅允许这两个页面相互通信，还允许任何其他页面将example.com作为超域（例如，blog.example.com）。攻击者也意识到了这一点，并构建了一个特殊的脚本（EvilScript），该脚本在攻击者的博客页面（BlogPage）中运行。在下一步（图 17.10）中，脚本执行SetDomain操作以将BlogPage的域属性修改为ExampleDomain。
图 17.10 - 时间 3 时的跨源逆例
现在BlogPage与其他两个文档具有相同的域属性，它可以成功执行ReadDOM操作来访问它们的内容（图 17.11）。
图 17.11 - 时间 4 时的跨源逆例
此攻击指出了用于跨源通信的域属性方法的一个关键弱点：使用此方法的应用程序的安全性仅与其共享相同基本域的所有页面中最薄弱的环节一样强大。我们很快将讨论另一种称为 PostMessage 的方法，该方法可用于更一般的跨源通信类别，同时也能提供更高的安全性。
在引入 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 代码的字符串中；此字符串有时称为填充（因此得名“带填充的 JSON”）。此填充可以是任何任意 JavaScript 代码，但通常，它是回调函数（已在当前文档中定义）的名称，该函数将在响应数据上执行。
<script src="http://www.example.com/mydata?jsonp=processData"></script>www.example.com上的服务器将其识别为 JSONP 请求，并将请求的数据包装在jsonp参数中。
processData(mydata)这是一个有效的 JavaScript 语句（即，将函数“processData”应用于值“mydata”），并由浏览器在当前文档中执行。
在我们的模型中，JSONP 被建模为一种 HTTP 请求，该请求在padding字段中包含回调函数的标识符。服务器在收到 JSONP 请求后，会返回一个响应，其中包含包装在回调函数（cb）中的请求资源（payload）。
sig CallbackID {} // identifier of a callback function
// Request sent as a result of <script> tag
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
-- result of JSONP request is passed on as an argument to the callback
payload = resp.@payload
}（EventHandler是一种特殊的调用类型，必须在另一个调用（由causedBy表示）之后发生；我们将使用事件处理程序来模拟脚本响应浏览器事件执行的操作。）
请注意，执行的回调函数与响应中包含的回调函数（cb = resp.@cb）相同，但不一定与原始 JSONP 请求中的padding相同。换句话说，为了使 JSONP 通信正常工作，服务器负责正确构造包含原始填充作为回调函数的响应（即，确保JsonRequest.padding = JsonpResponse.cb）。原则上，服务器可以选择包含任何回调函数（或任何 JavaScript 代码），包括与请求中的padding无关的函数。这突出了 JSONP 的潜在风险：接受 JSONP 请求的服务器必须值得信赖且安全，因为它能够在客户端文档中执行任何 JavaScript 代码片段。
分析：使用 Alloy Analyzer 检查Confidentiality属性会返回一个逆例，该逆例显示了 JSONP 的一个潜在安全风险。在此场景中，日历应用程序（CalendarServer）使用 JSONP 端点（GetSchedule）将其资源提供给第三方网站。为了限制对资源的访问，CalendarServer仅在请求包含正确识别该用户的 Cookie 时才发送包含用户日程安排的响应。
请注意，一旦服务器将 HTTP 端点作为 JSONP 服务提供，任何人都可以向其发出 JSONP 请求，包括恶意网站。在此场景中，来自EvilServer的广告横幅页面包含一个脚本标签，该标签会导致GetSchedule请求，并使用名为Leak的回调函数作为padding。通常，AdBanner的开发者无法直接访问受害者用户的CalendarServer会话 Cookie（MyCookie）。但是，由于 JSONP 请求被发送到CalendarServer，浏览器会自动将MyCookie作为请求的一部分包含在内；CalendarServer在收到包含MyCookie的 JSONP 请求后，将受害者的资源（MySchedule）包装在填充Leak内（图 17.12）。
图 17.12 - 时间 0 时的 JSONP 逆例
在下一步中，浏览器将 JSONP 响应解释为对Leak(MySchedule)的调用（图 17.13）。攻击的其余部分很简单；Leak可以简单地编程为将输入参数转发到EvilServer，从而允许攻击者访问受害者的敏感信息。
图 17.13 - 时间 1 时的 JSONP 逆例
此攻击是跨站点请求伪造（CSRF）的一个示例，它显示了 JSOPN 的一个固有弱点；网络上的任何网站都可以通过包含<script>标签并访问填充内的有效负载来发出 JSONP 请求。可以通过两种方式降低风险：（1）确保 JSONP 请求永远不会返回敏感数据，或者（2）使用 Cookie 之外的其他机制（例如，秘密令牌）来授权请求。
PostMessage 是 HTML5 中的一项新功能，它允许来自两个文档（可能来自不同来源）的脚本相互通信。它为设置domain属性的方法提供了一种更有条理的替代方案，但也带来了自身的安全风险。
PostMessage是一个浏览器 API 函数，它接受两个参数：（1）要发送的数据（message）和（2）接收消息的文档的来源（targetOrigin）。
sig PostMessage extends BrowserOp {
message: Resource,
targetOrigin: Origin
}为了接收来自另一个文档的消息，接收文档注册一个事件处理程序，该处理程序由浏览器作为PostMessage的结果调用。
sig ReceiveMessage extends EventHandler {
data: Resource,
srcOrigin: Origin
}{
causedBy in PostMessage
-- "ReceiveMessage" event is sent to the script with the correct context
origin[to.context.src] = causedBy.targetOrigin
-- messages match
data = causedBy.@message
-- the origin of the sender script is provided as "srcOrigin" param
srcOrigin = origin[causedBy.@from.context.src]
}浏览器向ReceiveMessage传递两个参数：一个与正在发送的消息对应的资源（data）和发送文档的来源（srcOrigin）。签名事实包含四个约束，以确保每个ReceiveMessage与其对应的PostMessage在格式上是正确的。
分析：再次，让我们询问 Alloy 分析器PostMessage是否是一种安全的跨源通信方式。这次，分析器返回了Integrity属性的反例，这意味着攻击者能够利用PostMessage中的弱点将恶意数据引入受信任的应用程序。
请注意，默认情况下，PostMessage 机制不会限制谁可以发送 PostMessage；换句话说，任何文档都可以向另一个文档发送消息，只要后者注册了ReceiveMessage处理程序。例如，在以下从 Alloy 生成的实例中，EvilScript在AdBanner内运行，向目标来源为EmailDomain的文档发送了一个恶意的PostMessage（图 17.14）。
图 17.14 - PostMessage 反例（时间点 0）
然后，浏览器将此消息转发到具有相应来源的文档（在本例中为InboxPage）。除非InboxScript专门检查srcOrigin的值以过滤掉来自不需要来源的消息，否则InboxPage将接受恶意数据，这可能导致进一步的安全攻击。（例如，它可能会嵌入一段 JavaScript 代码来执行 XSS 攻击。）这在图 17.14中显示。
图 17.15 - PostMessage 反例（时间点 1）
如本例所示，PostMessage默认情况下是不安全的，接收文档有责任额外检查srcOrigin参数以确保消息来自可信的文档。不幸的是，在实践中，许多网站省略了此检查，使恶意文档能够将不良内容作为PostMessage的一部分注入1。
然而，省略来源检查可能不仅仅是程序员无知的结果。对传入的 PostMessage 实施适当的检查可能很棘手；在某些应用程序中，很难预先确定预期接收消息的可信来源列表。（在某些应用程序中，此列表甚至可能会动态更改。）这再次突出了安全性和功能性之间的矛盾：PostMessage 可用于安全的跨源通信，但前提是已知可信来源的白名单。
跨源资源共享 (CORS) 是一种机制，旨在允许服务器与来自不同来源的站点共享其资源。特别是，CORS 可以被来自一个来源的脚本用于向具有不同来源的服务器发出请求，有效地绕过 SOP 对跨源 Ajax 请求的限制。
简而言之，典型的 CORS 过程涉及两个步骤：(1) 想要访问来自外部服务器的资源的脚本在其请求中包含一个“Origin”标头，该标头指定脚本的来源，以及 (2) 服务器在其响应中包含一个“Access-Control-Allow-Origin”标头，指示一组允许访问服务器资源的来源。通常，如果没有 CORS，浏览器会首先阻止脚本发出跨源请求，符合 SOP。但是，在启用 CORS 的情况下，浏览器允许脚本发送请求并访问其响应，但仅当“Origin”是“Access-Control-Allow-Origin”中指定的来源之一。
（CORS 还包含预检请求的概念，此处未讨论，以支持除 GET 和 POST 之外的复杂类型的跨源请求。）
在 Alloy 中，我们将 CORS 请求建模为一种特殊的XmlHttpRequest，它有两个额外的字段origin和allowedOrigins。
sig CorsRequest in XmlHttpRequest {
-- "origin" header in request from client
origin: Origin,
-- "access-control-allow-origin" header in response from server
allowedOrigins: set Origin
}{
from in Script
}然后，我们使用 Alloy 事实corsRule来描述构成有效 CORS 请求的内容。
fact corsRule {
all r: CorsRequest |
-- the origin header of a CORS request matches the script context
r.origin = origin[r.from.context.src] and
-- the specified origin is one of the allowed origins
r.origin in r.allowedOrigins
}分析：CORS 是否可以被滥用来允许攻击者危害受信任站点的安全性？当被提示时，Alloy 分析器返回了Confidentiality属性的一个简单反例。
在这里，日历应用程序的开发人员决定通过使用 CORS 机制与其他应用程序共享其某些资源。不幸的是，CalendarServer被配置为在 CORS 响应中返回Origin（表示所有来源值的集合）作为access-control-allow-origin标头的值。结果，来自任何来源的脚本，包括EvilDomain，都被允许向CalendarServer发出跨站点请求并读取其响应（图 17.16）。
图 17.16 - CORS 反例
此示例突出显示了开发人员在使用 CORS 时常犯的一个错误：使用通配符值“*”作为“access-control-allow-origin”标头的值，允许任何站点访问服务器上的资源。如果资源被认为是公开的并且任何人都可以访问，则此访问模式是合适的。但是，事实证明，许多站点即使对于私有资源也使用“*”作为默认值，无意中允许恶意脚本通过 CORS 请求访问它们2。
为什么开发人员会使用通配符？事实证明，指定允许的来源可能很棘手，因为在设计时可能不清楚在运行时应授予哪些来源访问权限（类似于上面讨论的 PostMessage 问题）。例如，服务可能会允许第三方应用程序动态订阅其资源。
在本章中，我们着手构建一个文档，通过使用名为 Alloy 的语言构建该策略的模型，从而对 SOP 及其相关机制有清晰的了解。我们的 SOP 模型不是传统意义上的实现，不能像其他章节中显示的工件一样部署使用。相反，我们想展示我们“敏捷建模”方法的关键要素：(1) 从系统的简化抽象模型开始，并根据需要逐步添加细节，(2) 指定系统预期满足的属性，以及 (3) 应用严格的分析来探索系统设计中潜在的缺陷。当然，本章是在 SOP 首次引入很久之后才编写的，但我们相信，如果在系统设计的早期阶段进行这种建模，它可能会带来更大的好处。
除了 SOP 之外，Alloy 还被用于建模和推理各种不同领域的系统——从网络协议、语义网、字节码安全到电子投票和医疗系统。对于许多这些系统，Alloy 的分析导致发现了设计缺陷和错误，这些缺陷和错误在某些情况下困扰了开发人员数年。我们邀请读者访问Alloy 页面并尝试构建他们最喜欢的系统的模型！
如本章前面所述，Alloy 对正在建模的系统的行为不做任何假设。缺乏内置范式允许用户使用少量基本语言构造来编码各种建模习惯用法。例如，我们可以将系统指定为状态机、具有复杂不变量的数据模型、具有全局时钟的分布式事件模型，或任何最适合当前问题的习惯用法。常用习惯用法可以封装为通用模块，并在多个系统中重用。
在我们的 SOP 模型中，我们将系统建模为一组通过进行一个或多个调用相互通信的端点。由于调用是一个相当通用的概念，因此我们将它的描述封装在单独的 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 请求时，我们通过将Endpoint作为其类型参数导入模块call。结果，参数类型T被实例化为Endpoint，我们获得了一组与发送者和接收者端点对相关联的Call对象。一个模块可以多次导入；例如，我们可以声明一个名为UnixProcess的签名，并实例化模块call以获得一组不同的Call对象，这些对象从一个 Unix 进程发送到另一个 Unix 进程。