介绍
同源政策（SOP）是每个现代浏览器安全机制的重要组成部分。它控制在浏览器中运行的脚本可以彼此通信（大致来自同一网站）。首先在Netscape Navigator中引入，SOP现在在Web应用程序的安全性中起着至关重要的作用;没有它，恶意骇客在Facebook上仔细阅读你的私人照片，阅读你的电子邮件或清空你的银行帐户将更容易。
但是SOP远非完美。有时，它太限制了;有些情况（如mashup），其中来自不同来源的脚本应该能够共享资源但它不能。在其他时候它没有足够的限制，留下可以利用跨站点请求伪造等常见攻击的角色情况。此外，SOP的设计多年来已经有机地发展，并且使许多开发人员困惑不解。
本章的目标是捕捉这个重要而又经常被误解的特征的本质。特别是我们将尝试回答以下问题：
-
为什么需要SOP？它阻止的安全违规类型是什么？
-
Web应用程序的行为如何受到SOP的影响？
-
绕过SOP有什么不同的机制？
-
这些机制有多安全？他们介绍的潜在安全问题是什么？
考虑到所涉及的部分的复杂性 - Web服务器，浏览器，HTTP，HTML文档，客户端脚本等，整体覆盖SOP是一项艰巨的任务。我们可能会被所有这些部件的粗细细节陷入僵局（并且在达到SOP之前消耗了我们的500行代码）。但是，如果没有代表关键的细节，我们怎么能做到精准呢？
Modeling with Alloy
本章与本书中的其他内容有所不同。我们将构建一个可执行模型，而不是构建一个工作的实现，作为一个简单而精确的SOP描述。可以执行该模型来探索系统的动态行为，但与实现不同，该模型忽略了可能妨碍基本概念的低级细节。
我们采取的方法是“agile modeling”，因为它与agile programming相似。我们逐步组装模型直至可执行，并制定和运行测试时，所以最终我们不仅拥有模型本身，还包含了它所满足的属性集合。
为了构建这个模型，我们使用Alloy，一种用于建模和分析软件设计的语言。Alloy modelling不能以传统的程序执行方式执行。相反，模型可以（1）模拟以产生表示系统的有效场景或配置的实例，以及（2）检查以查看模型是否满足期望的属性。
尽管有上述的相似之处，agile modeling不同于agile programming：虽然我们将会运行测试，但实际上并不会写任何内容。 Alloy的分析仪自动生成测试用例，需要提供的所有测试用例要检查的属性。这节省了很多麻烦（和文字）。分析器实际上执行所有可能的测试用例，直到一定的范围;这通常意味着产生具有一定数量的对象的所有起始状态，然后选择操作和参数来应用到一些步骤。由于执行了许多测试（通常是数十亿次），并且由于所有可能的状态可能会被配置覆盖，所以这种分析倾向于比常规测试更有效地显示错误（有时被称为”bounded verification”）。
简化
由于SOP在浏览器，服务器，HTTP等环境中运行，所以完整的描述将是压倒性的。因此，我们的模型（如所有模型）抽象出不相关的方面，例如网络数据包的结构和路由。但也简化了一些相关的内容，这意味着该模型无法充分说明所有可能的安全漏洞。
例如，我们将HTTP请求视为远程过程调用，忽略了对请求的响应可能会出错的事实。我们还假设DNS（域名服务）是静态的，所以我们不考虑在交互过程中DNS绑定变化的攻击。原则上，这样做可以扩展我们的模型来涵盖所有这些的内容，在安全分析的本质上，没有模型（即使它代表整个代码库）也可以被保证是完整的。
Roadmap
以下是我们使用的SOP模型的顺序。首先构建我们需要的三个关键组件的模型，以便我们讨论SOP：HTTP，浏览器和客户端脚本。我们将建立在这些基本模型之上，以定义Web应用程序的安全性意义，然后将SOP作为尝试实现所需安全属性的机制。
然后，我们将看到SOP有时太限制，阻碍了Web应用程序的正常运行。因此，我们介绍四种不同的技术，通常用于绕过策略强加的限制。
随意浏览你想要的任何顺序的部分。如果你是Alloy的新人，我们建议从前三部分（HTTP，浏览器和脚本）开始，因为它们介绍了agile language的一些基本概念。在阅读本章的过程中，我们鼓励你使用Alloy Analyzer;运行它们，探索生成的场景，并尝试修改并查看其效果。它可以免费下载。
Model of the Web
HTTP
构建Alloy model的第一步是声明对象。 我们从资源开始：
sig Resource {}
关键字sig将声明标识为Alloy signature。这引入了一组资源对象; 就像没有实例变量的类的对象一样，作为具有身份但没有内容的blob。当分析运行时，确定该集合，正如面向对象语言中的类在程序执行时表示对象时一样。
资源由URL（uniform resource locators）命名：
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编写protocol.p。
请注意，与URL不同的路径被视为没有结构 ——简化。关键字lone（可以读取“小于等于1”）表示每个URL最多只有一个端口。路径是跟随URL中主机名的字符串，（对于简单的静态服务器）对应于资源的文件路径;我们假设它总是存在，但可以是为空。
介绍客户端和服务器，每个客户端和服务器都包含从路径到资源的映射：
abstract sig Endpoint {}
abstract sig Client extends Endpoint {}
abstract sig Server extends Endpoint {
resources: Path -> lone Resource
}
关键字extend引入了一个子集，所以所有客户端的’Client’集都是所有结点的’Endpoint’集合的子集。扩展是不相交的，所以任何端点都不是客户端和服务器。关键字abstract，一个签名的所有扩展都会耗尽它，所以它在Endpoint声明中的出现说明每个端点必须属于其中一个子集（此时是客户端和服务器）。对于服务器，表达式s.resources将表示从路径到资源（因此声明中的箭头）的映射。回想一下，每个字段实际上是一个包含签名作为第一列的关系，因此该字段表示Server, Path和Resource的三列关系。
要将URL映射到服务器，我们引入一组域名服务器，每个域具有从域到服务器的映射：
one sig Dns {
map: Domain -> Server
}
签名声明中的关键字’one‘意味着，我们将假定只有一个域名服务器，并且有一个由表达式Dns.map给出的单一的DNS映射。与服务资源一样，这可能是动态的（事实上，已知的安全攻击依赖于交互期间更改DNS绑定），但我们正在简化。
为了建模HTTP请求，我们还需要cookies的概念，所以让我们来声明一下：
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 module，在这里我们需要导入它：
open call[Endpoint]
它是一个多态模块，所以它被实例化为Endpoint，这些集合调用from和to。（该模块完整内容在 Appendix: Reusing Modules in Alloy）
遵循HttpRequest中的字段声明是约束的集合。这些约束中的每个都适用于HTTP请求集合中的所有成员。约束条件是：（1）每个请求都来自一个客户端，（2）每个请求被发送到由DNS主机根据DNS映射指定的服务器。
Alloy的一个突出特点是可以随时执行一个模型，无论多么简单或复杂，以生成示例系统实例。让我们使用run命令来询问Alloy Analyzer执行到目前为止的HTTP模型：
run {} for 3 -- generate an instance with up to 3 objects of every signature type
一旦分析器发现系统的可能实例，它就会自动生成一个实例图，如图17.1所示。
该实例显示一个客户端（由节点客户端表示）向Server发送一个HttpRequest，作为响应，客户端返回资源对象并指示客户端存储Cookie在Domain。
即使这是一个看似细节的小例子，它表明了我们的模型有一个缺陷。请注意，从请求返回的资源（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所示。
这个反例再次显示了客户端发出的HTTP请求，但是使用了两个不同的服务器。（在 Alloy visualizer中，相同类型的对象通过将数字后缀附加其名称来区分;如果只有一个给定类型的对象，则不添加任何后缀。快照图中出现的每个名称都是一个对象，所以或许可以令人困惑的，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字段在给定时间将一组文档与每个浏览器相关联。（有关我们如何模拟动态行为的更多详细信息，请参阅附录：Appendix: Reusing Modules in Alloy]。）
文档是从响应HTTP请求创建的。如果用户关闭选项卡或浏览器，我们将其退出模型，也可能会被破坏。一个文件有一个URL（源自该文档的URL），一些内容（DOM）和一个域：
sig Document {
src: Url,
content: Resource -> Time,
domain: Domain -> Time
}
在后两个字段中Timer列可以告诉我们，它们可以随着时间而变化，并且省略第一个（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声明，并且表示呼叫开始和结束时的时间。表达式document.end在调用结束时给出从浏览器到文档的映射。所以这个约束，在调用之后，映射不变，除了表格映射from到doc。
一些约束使用++关系覆盖运算符：e1 ++ e2包含e2的所有元组，此外，e1中的任何元组是e1的第一个元素不是e2中的元组的第一个元素。例如，约束content.end = content.start ++ doc -> response，在调用之后，context映射将被更新映射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 Analyzer可能会生成场景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具有子域名电子邮件和日历，将example.com分享共同的超级域名。在我们的模型中，可以通过引入包含其他人的域名来表示：
one sig ExampleDomain extends Domain {}{
subsumes = EmailDomain + EvilDomain + CalendarDomain + this
}
注意，subsumes的成员包含this，因为每个域名都包含自身。
还有关于我们在这里省略的这些应用程序的其他细节（请参阅完整版example.als）。但是，我们在本章的其余部分重新审视这些应用程序作为示例。
安全属性
在进入SOP之前，我们还没有讨论一个重要的问题：当我们说我们的系统是安全的时候是什么意思？
毫无疑问，这是一个棘手的问题。我们将转向信息安全 - 机密性和完整性两个深入研究的概念。这两个概念都是谈论如何允许信息通过系统的各个部分。大致来说，机密性意味着只有对被认为可信任的部分才能访问关键的数据，而完整性意味着信任的部分只能依赖于没有被恶意篡改的数据。
数据流属性
为了更精确地指定这些安全属性，我们首先需要定义从系统的一部分流向另一部分的数据的意义。模型中，我们已经描述了两个端点之间的通过通话进行的交互;例如，浏览器通过HTTP请求与服务器交互，脚本通过调用浏览器API操作与浏览器交互。直观地，在每个呼叫期间，一条数据可以作为呼叫的参数或返回值从一个端点流向另一端点。为了表示这一点，我们将DataflowCall的概念引入模型，并将每个调用与一组参数关联并返回数据字段：
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的概念，并分配字段访问来表示在每个时间步长模块可以访问的数据元素集合：
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
}
Threat Model
威胁模型描述了攻击者可能执行的以试图破坏系统的安全属性的一组操作。构建威胁模型是安全系统设计中重要的一步;它允许我们识别我们关于系统及其环境的假设，并优先考虑需要减轻的不同类型的风险。
在我们的模型中，我们考虑可以充当服务器，脚本或客户端的攻击者。作为服务器，攻击者可能会设置恶意网页，以征求不知情用户的访问权限，而这些访问者又可能会无意中向攻击者发送敏感信息作为HTTP请求的一部分。攻击者可能会创建一个恶意脚本，调用DOM操作从其他页面读取数据，并将这些数据中继到攻击者的服务器。最后，作为一个客户端，攻击者可以冒充普通用户，并向服务器发送恶意请求，以尝试访问用户的数据。我们不认为攻击者窃取不同网络端点之间的连接;虽然在实践中是一个威胁，但是SOP并不是为了防止它而设计，因此它不在我们模型的范围之内。
检查属性
现在我们已经定义了安全属性和攻击者的行为，让我们展示如何使用Alloy Analyzer来自动检查这些属性，即使存在攻击者。当使用检查命令提示时，分析器会探测系统中所有可能的数据流跟踪，并生成一个反例（如果存在），演示如何违反：
check Confidentiality for 5
例如，根据机密属性检查示例应用程序的模型时，分析器将生成图17.4和图17.5中的方案，它显示了EvilScript如何访问关键数据（MyInboxInfo）。
这个反例有两个步骤。第一步（图17.4）中，EvilScript从EvilDomain在AdBanner内部执行，读取来自EmailDomain的InboxPage内容。第二步（图17.5）中，EvilScript通过进行调用XmlHtttpRequest向EmilServer发送相同的内容（MyInboxInfo）。这里的核心问题是，在一个域下执行的脚本能够从另一个域读取文档的内容; 正如我们将在下一节中看到的，这正是SOP旨在防止的情景之一。
单个assertion可能有多个反例。图17.6，显示了系统可能违反机密性质的不同方式。
在这个场景下，EvilScript不是阅读收件箱页面的内容，而是直接向EmailServer发送GetInboxInfo请求。请注意，该请求包括一个cookie（MyCookie），该cookie是作用于与目标服务器相同的域。这是危险的，因为如果cookie表示用户的身份（例如，会话cookie），则vilScript可以有效地伪装成用户，并欺骗服务器响应用户的私有数据（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]
}
我们可以看到，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）邮寄;和（4）CORS。这些是有价值的工具，但是如果使用时不小心，可能会使Web应用程序容易让SOP受到各种攻击。
四项技术的每种都是很复杂的，如果充分详细描述，需要一章。所以在这里我们只是给出一个简短的印象，说明它们如何工作，潜在的安全问题，以及如何防止这些问题。特别是，我们要求 Alloy Analyzer检查每种技术是否被攻击者滥，破了坏我们之前定义的两个安全属性：
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的浏览器操作类型的行为：
// 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字段表示属性应该设置的值。cunz 一个警告：脚本只能将域属性设置为其主机名的右侧，完全限定的片段。（即，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起始位置的函数，document.domain是在时间t的主机名。
值得指出的是，这两个文档的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是原始域的超级域），所以它可以被允许。
完成此操作后，现在可以通过执行ReadDom或WriteDom操作来访问对方的DOM，如图17.9所示。
请注意，当你将email.example.com和calendar.example.com的域设置为example.com时，不仅允许这两个页面在彼此之间进行通信，还允许具有example.com的任何其他页面作为 超域（例如blog.example.com）。攻击者也意识到这一点，并构建了一个在攻击者博客页面（BlogPage）内运行的特殊脚本（EvilScript）。下一步（图17.10）中，脚本执行SetDomain操作，将BlogPage的domain属性修改为ExampleDomain。
现在BlogPage与其他两个文档具有相同的域属性，可以成功执行ReadDOM操作来访问其内容（图17.11。）
这种攻击指出了跨原始通信的域属性方法的一个关键弱点：使用此方法的应用程序的安全性与所有共享相同基础域的页面中最薄弱的链接一样强大。我们将尽快讨论另一种称为PostMessage的方法，它可以用于更一般的跨原始通信类，同时也更安全。
JSON with Padding (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代码;这个字符串称为填充（名为“JSON with padding”）。这个填充可以是任何任意的JavaScript代码，但是通常来说，它是在响应数据上执行的回调函数的名称：
<script src="http://www.example.com/mydata?jsonp=processData"></script>
www.example.com上的服务器将其识别为JSONP请求，并将请求的数据包装在jsonp参数中：
processData(mydata)
这是一个有效的JavaScript语句（即在“mydata”上应用函数“processData”），并由当前文档的浏览器执行。
在我们的模型中，JSONP被建模为一种HTTP请求，其包括字段padding中的回调函数的标识符。在收到JSONP请求后，服务器返回一个包含回调函数（cb）内部请求的资源（有效载荷）的响应。
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是一种特殊类型的调用，必须在另一个调用之后的某个时间进行，由causeBy表示;我们将使用事件处理程序来模拟脚本响应浏览器事件执行的操作。）
请注意，执行的回调函数与响应中包含的回调函数（cb = resp.@cb）相同，但不一定与原始JSONP请求中的padding相同。换句话说，为了使JSONP通信工作，服务器负责正确地构建包含原始填充作为回调函数的响应（如确保JsonRequest.padding = JsonpResponse.cb）。原则上，服务器可以选择包括任何回调函数（或任何JavaScript），包括与请求中padding无关的函数。这突出了JSONP的潜在风险：接受JSONP请求的服务器必须是可靠和安全的，因为它可以在客户端文档中执行任何JavaScript代码。
分析：检查Alloy Analyzer的Confidentiality属性返回一个反例，显示JSONP潜在安全风险。这种情况下，日历应用程序（CalendarServer）使用JSONP端点（GetSchedule）使其资源可用于第三方站点。要限制对资源的访问权限，如果请求包含正确标识该用户的cookie，则CalendarServer将仅向用户发回具有调度的响应。
请注意，一旦服务器将HTTP端点提供为JSONP服务，任何人都可以提供JSONP请求，包括恶意站点。在这种情况下，EvilServer的广告标题页面包含脚本标签，该脚本标签导致GetSchedule请求，并将回调函数称为padding的Leak。通常，AdBanner的开发人员无法直接访问CalendarServer的受害用户的会话cookie（MyCookie）。但是，由于JSONP请求被发送到CalendarServer，浏览器会自动将MyCookie作为请求的一部分;已收到与MyCookie的JSONP请求的CalendarServer将返回被包含在padding leak的受害者的资源（MySchedule）（图17.12）。
下一步中，浏览器将JSONP响应解释为对Leak(MySchedule)的调用（图17.13）。 其余的攻击很简单; Leak可以简单地将输入参数转发到EvilServer，允许攻击者访问受害者的敏感信息。
这种攻击是跨站点请求伪造（CSRF）的示例，显示了JSOPN的固有缺陷; 网站上的任何网站都可以通过添加<script>标签并访问padding的有效内容来简单地制作JSONP请求。风险可以通过两种方式得到缓解：（1）确保JSONP请求不会返回敏感数据，或者（2）使用另一种机制代替cookie（例如秘密令牌）来授权请求。
PostMessage
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 Analyzer PostMessage是否是一种执行跨原始通信的安全方式。这次，分析仪返回Integrity属性的反例，这意味着攻击者可以利用PostMessage中的弱点将恶意数据引入受信任的应用程序。
请注意，默认情况下，PostMessage机制不限制允许发送PostMessage的人员;换句话说，只要后者已经注册了一个ReceiveMessage处理程序，任何文档都可以发送消息到另一个文档。例如，在由Alloy生成的以下实例中，AdBanner中运行的EvilScript将恶意PostMessage发送到目标来源为EmailDomain的文档（图17.14）。
然后，浏览器将该消息转发到具有相应来源（在本例中为InboxPage）的文档。除非InboxScript专门检查srcOrigin的值以过滤不需要的邮件，InboxPage将接受恶意数据，可能导致进一步的安全攻击。（例如，它可能嵌入一个JavaScript来执行XSS攻击）。如图17.14所示。
如此示例所示，默认情况下PostMessage不安全，接收文档有责任另外检查srcOrigin参数，以确保该消息来自可信赖的文档。不幸的是，实践中许多站点都省略了这个检查，使恶意文件能够将不良内容注入PostMessage。
然而，省略原始检查不仅仅是程序员无知的结果。对传入的PostMessage执行适当的检查很棘手;在某些应用中，难以预先确定可接收消息的可信来源的列表。同样，这突出显示了安全性和功能性之间的紧张关系：PostMessage可用于安全的跨原始通信，但仅当已知可信来源的白名单时。
Cross-Origin Resource Sharing (CORS)
CORS是一种允许服务器与来自不同来源的站点共享其资源的机制。特别地，CORS可以由来自一个来源的脚本用于向具有不同来源的服务器发出请求，有效地绕过了跨原始Ajax请求的SOP限制。
简单来说，典型的CORS过程包括两个步骤：（1）从外部服务器访问资源的脚本在其请求中包括指定脚本的起源的“Origin”，以及（2）服务器包括“Access-Control-Allow-Origin”标头作为其响应的一部分，指示允许访问服务器资源的一组源。通常，没有CORS，浏览器将阻止脚本首先发出符合SOP的跨原始请求。然而，启用CORS后，浏览器允许脚本发送请求并访问其响应，但只有当“Origin”是“Access-Control-Allow-Origin”中指定的源时才允许。
（除了GETs和POST之外，CORS还包括一个前瞻性请求概念，这里不讨论这些概念来支持复杂类型的跨原始请求。）
在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 fact 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 Analyzer为Confidentiality属性返回一个简单的反例。
在这里，日历应用程序的开发人员决定通过使用CORS机制与其他应用程序共享一些资源。不幸的是，CalendarServer被配置为返回CORS响应中的access-control-allow-origin头的Origin（它代表所有原始值的集合）。因此，允许任何来源的脚本（包括EvilDomain）向CalendarServer发出跨站点请求并读取其响应（图17.16）。
此示例突出了开发人员使用CORS的一个常见错误：使用通配符值“”作为“access-control-allow-origin”标头的值，允许任何站点访问服务器上的资源。如果资源是公开的，并且任何人都可以访问，则该访问模式是适当的。然而，事实证明，即使是私人资源，许多站点也使用“”作为默认值，无意中允许恶意脚本通过CORS请求访问它们。
为什么开发人员会使用通配符？事实证明，指定允许的来源可能是棘手的，因为在设计时可能不清楚哪个起始应该在运行时被授予访问权限（类似于上面提到的PostMessage问题）。例如，服务可以允许第三方应用程序动态地订阅其资源。
结论
在本章中，我们着手构建一个文档，通过以一种Alloy语言构建模型，从而对SOP及其相关机制提供了清晰的了解。我们的SOP模型不是传统意义上的实现，不能像其他章节所示的工件一样部署使用。相反，我们想要展示我们的“agile modeling”方法背后的关键要素：（1）开始使用系统的小型抽象模型，并根据需要逐步添加细节，（2）指定系统预期的属性，（3）严格分析，探索系统设计中的潜在缺陷。当然，这一章是在SOP第一次引入之后写的很久，但是我们认为，如果在系统设计的早期阶段完成这种建模，这种类型的建模可能会更有益处。
除了SOP之外，Alloy已被用于对不同领域的各种系统进行建模和推理，从网络协议，语义网，字节码安全到电子投票和医疗系统。对于这些系统，Alloy的分析发现设计缺陷和错误，在某些情况下，开发人员很早就发现了。我们邀请读者访问Alloy Page页面，并尝试构建自己喜欢的系统的模型！
引用
-
Sooel Son and Vitaly Shmatikov. The Postman Always Rings Twice: Attacking and Defending postMessage in HTML5 Websites. Network and Distributed System Security Symposium (NDSS), 2013.↩
-
Sebastian Lekies, Martin Johns, and Walter Tighzert. The State of the Cross-Domain Nation. Web 2.0 Security and Privacy (W2SP), 2011.↩