本文使用一種用于建模與分析軟件設(shè)計(jì)的語(yǔ)言 Alloy來(lái)構(gòu)建同源策略 SOP 模型。Alloy作為建模語(yǔ)言，并不能編寫(xiě)程序執(zhí)行，但它可以編寫(xiě)模型，并通過(guò)自動(dòng)生成并運(yùn)行測(cè)試用例來(lái)對(duì)模型進(jìn)行檢查。感覺(jué) Alloy 的中文資料不是很多，感興趣的小伙伴可以看下官網(wǎng)。

原文作者

Eunsuk Kang、Santiago Perez De Rosso 和 Daniel Jackson。Eunsuk Kang 是麻省理工學(xué)院的博士研究生和軟件設(shè)計(jì)小組成員。他在麻省理工學(xué)院（2010年）獲得計(jì)算機(jī)科學(xué)碩士學(xué)位，并獲得滑鐵盧大學(xué)軟件工程學(xué)士學(xué)位（2007年）。他的研究項(xiàng)目集中于開(kāi)發(fā)軟件建模和驗(yàn)證的工具和技術(shù)，并將其應(yīng)用于安全和安全關(guān)鍵系統(tǒng)。

Santiago Perez De Rosso 是麻省理工學(xué)院軟件設(shè)計(jì)組的博士生。他在麻省理工學(xué)院獲得計(jì)算機(jī)科學(xué)碩士學(xué)位（2015年），并在ITBA獲得本科學(xué)位（2011年）。他曾在谷歌工作，開(kāi)發(fā)框架和工具，讓工程師更有效率（2012年）。他現(xiàn)在大部分時(shí)間都在考慮設(shè)計(jì)和版本控制。

Daniel Jackson 是麻省理工學(xué)院電子工程和計(jì)算機(jī)科學(xué)系的教授，他領(lǐng)導(dǎo)著計(jì)算機(jī)科學(xué)和人工智能實(shí)驗(yàn)室的軟件設(shè)計(jì)小組。他獲得牛津大學(xué)物理碩士學(xué)位（1984年），麻省理工學(xué)院計(jì)算機(jī)科學(xué)碩士（1988年）和博士學(xué)位（1992年）。他是卡內(nèi)基梅隆大學(xué) Logic 公司的軟件工程師（1984—1986年），卡內(nèi)基梅隆大學(xué)計(jì)算機(jī)科學(xué)助理教授（1992—1997年），自1997年畢業(yè)于麻省理工學(xué)院。他對(duì)軟件工程有著廣泛的興趣，尤其是在開(kāi)發(fā)方法、設(shè)計(jì)和規(guī)范、形式方法和安全關(guān)鍵系統(tǒng)方面。

引言

同源策略（SOP）是現(xiàn)代瀏覽器安全機(jī)制的重要組成部分。它控制在瀏覽器中運(yùn)行的腳本何時(shí)可以相互通信（粗略地說(shuō)就是它們何時(shí)來(lái)自同一個(gè)網(wǎng)站）。SOP 最初是在 Netscape Navigator 中引入的，現(xiàn)在它在 Web 應(yīng)用程序的安全性方面起著關(guān)鍵的作用；如果沒(méi)有它，惡意黑客在 Facebook 上瀏覽你的私人照片、閱讀你的電子郵件或清空你的銀行賬戶就會(huì)容易得多。

但 SOP 還遠(yuǎn)遠(yuǎn)不夠完美。有時(shí)，限制性太強(qiáng)；在某些情況下（如 mashup），來(lái)自不同來(lái)源的腳本應(yīng)該能夠共享資源，但卻做不到。有時(shí)，它又沒(méi)有足夠的限制，留下了可以利用常見(jiàn)攻擊（如跨站點(diǎn)請(qǐng)求偽造）的極端案例。此外，SOP 的設(shè)計(jì)經(jīng)過(guò)多年的發(fā)展，讓許多開(kāi)發(fā)人員無(wú)法完全理解。

本文的目的是抓住這一重要但經(jīng)常被誤解的特征的本質(zhì)。特別是，我們將嘗試回答以下問(wèn)題：

• 為什么需要SOP？它可以防止哪些類型的安全違規(guī)行為？

• SOP如何影響 Web 應(yīng)用程序的行為？

• 繞過(guò)SOP的機(jī)制有什么不同？

• 這些機(jī)制有多安全？它們會(huì)帶來(lái)哪些潛在的安全問(wèn)題？

考慮到 Web 服務(wù)器、瀏覽器、HTTP、HTML 文檔、客戶端腳本等所涉及部分的復(fù)雜性，全面覆蓋 SOP 是一項(xiàng)艱巨的任務(wù)。我們可能會(huì)被這些部分的粗糙細(xì)節(jié)所困擾（甚至在達(dá)到 SOP 之前就寫(xiě)完我們的 500 行代碼）。但是，我們?cè)趺茨茉诓魂愂鲫P(guān)鍵細(xì)節(jié)的情況下做到精確講解呢？

使用 Aolly 建模

本文與這本書(shū)中的其它章節(jié)有些不同。我們將構(gòu)建一個(gè)可執(zhí)行模型，作為 SOP 的簡(jiǎn)單而精確的描述，而不是構(gòu)建一個(gè)可以工作的實(shí)現(xiàn)。與實(shí)現(xiàn)一樣，可執(zhí)行模型來(lái)探索系統(tǒng)的動(dòng)態(tài)行為，但與實(shí)現(xiàn)不同的是，模型忽略了可能妨礙理解基本概念的低級(jí)細(xì)節(jié)。

我們采用的方法可能被稱為“敏捷建?！?，因?yàn)樗c敏捷編程類似。我們逐步地工作，一點(diǎn)一點(diǎn)地組裝模型。我們的演變模型在每一點(diǎn)上都是可以執(zhí)行的。我們?cè)谘葑冞^(guò)程中制定并運(yùn)行測(cè)試，這樣到最后我們不僅擁有模型本身，而且還擁有它所滿足的屬性集合。

為了構(gòu)建這個(gè)模型，我們使用 Alloy，一種用于建模和分析軟件設(shè)計(jì)的語(yǔ)言。 Alloy 模型不能在傳統(tǒng)意義上的程序執(zhí)行中執(zhí)行。相反，可以（1）模擬模型以生成表示系統(tǒng)的有效場(chǎng)景或配置的實(shí)例，（2）檢查模型是否滿足所需屬性。

除了上述相似之處，敏捷建模與敏捷編程在一個(gè)關(guān)鍵方面不同：盡管我們會(huì)運(yùn)行測(cè)試，但實(shí)際上我們不會(huì)編寫(xiě)任何測(cè)試代碼。Alloy 的分析器自動(dòng)生成測(cè)試用例，需要提供的只是要檢查的屬性。不用說(shuō)，這省去了很多麻煩（和文字）。分析器實(shí)際執(zhí)行所有可能的測(cè)試用例，直到達(dá)到一定的大?。ǚQ為范圍）；這通常意味著生成所有可能對(duì)象的所有啟動(dòng)狀態(tài)，然后選擇操作和參數(shù)應(yīng)用到一些步驟中。由于執(zhí)行了如此多的測(cè)試（通常是數(shù)十億），并且由于涵蓋了一個(gè)狀態(tài)可以采取的所有可能配置（盡管在范圍內(nèi)），這種分析往往可以比傳統(tǒng)測(cè)試更有效地暴露BUG （有時(shí)被稱為“有界驗(yàn)證”）。

簡(jiǎn)化

因?yàn)?SOP 是在瀏覽器、服務(wù)器、HTTP等環(huán)境中運(yùn)行的，所以一個(gè)完整的描述將十分復(fù)雜。因此，我們的模型（和所有模型一樣）抽象掉了不相關(guān)的方面，比如網(wǎng)絡(luò)數(shù)據(jù)包的結(jié)構(gòu)和路由。同時(shí)它也簡(jiǎn)化了一些相關(guān)的方面，這意味著該模型不能完全考慮到所有可能的安全漏洞。

例如，我們將 HTTP 請(qǐng)求視為遠(yuǎn)程過(guò)程調(diào)用，而忽略了對(duì)請(qǐng)求的響應(yīng)可能出現(xiàn)順序錯(cuò)誤這一事實(shí)。我們還假設(shè) DNS（域名服務(wù)）是靜態(tài)的，因此我們不考慮在交互過(guò)程中 DNS 綁定改變的攻擊。雖然從原則上講，我們可以擴(kuò)展我們的模型以涵蓋所有這些方面，但在安全分析的本質(zhì)上，任何模型（即使它代表整個(gè)代碼庫(kù)）都不能保證是完整的。

路線圖

以下是我們向前演化 SOP 模型的順序。我們將首先構(gòu)建三個(gè)關(guān)鍵組件的模型，這三個(gè)組件是我們討論SOP所需要的：HTTP、瀏覽器和客戶端腳本。我們將在這些基本模型的基礎(chǔ)上構(gòu)建，以定義 Web 應(yīng)用程序的安全性意義，然后引入 SOP 作為一種嘗試實(shí)現(xiàn)所需安全屬性的機(jī)制。

然后我們將看到 SOP 有時(shí)會(huì)限制性太強(qiáng)，妨礙web應(yīng)用程序的正常運(yùn)行。因此，我們將介紹四種不同的技術(shù)，它們通常用于繞過(guò)政策施加的限制。

你可以按自己喜歡的順序?yàn)g覽這些部分。如果你不熟悉 Alloy，我們建議你從前三部分（HTTP、瀏覽器和腳本）開(kāi)始，因?yàn)樗鼈兘榻B了建模語(yǔ)言的一些基本概念。在你閱讀本文的同時(shí)，我們也鼓勵(lì)你使用 Alloy 分析器中的模型；運(yùn)行它們，探索生成的場(chǎng)景，嘗試進(jìn)行修改并查看其效果。它可以免費(fèi)下載。

Web模型

HTTP

構(gòu)建 Aolly 模型的第一步是聲明一些對(duì)象集。讓我們從資源開(kāi)始：

sig Resource {}

關(guān)鍵字 sig 將其標(biāo)識(shí)為 Aolly 簽名聲明。這引入了一組資源對(duì)象；把它們想象成沒(méi)有實(shí)例變量的類的對(duì)象，有標(biāo)識(shí)但沒(méi)有內(nèi)容的blob。當(dāng)分析運(yùn)行時(shí)，這個(gè)集合將被確定，就像面向?qū)ο笳Z(yǔ)言中的類在程序執(zhí)行時(shí)用來(lái)表示一組對(duì)象一樣。

資源由URL（統(tǒng)一資源定位符）命名：

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

在這里，我們有五個(gè)簽名聲明，介紹了一組 URL 和四個(gè)附加集，分別用于它們所包含的每種基本類型的對(duì)象。在 URL 聲明中，我們有四個(gè)字段。字段類似于類中的實(shí)例變量；例如，如果 u 是一個(gè)URL，那么 u.protocol 將表示該 URL 的協(xié)議（就像Java中的點(diǎn)）。但事實(shí)上，我們將在后面看到，這些字段是關(guān)系。你可以將每個(gè)表看作是一個(gè)兩列數(shù)據(jù)庫(kù)表。因此，protocol 是一個(gè)表，第一列包含 URL，第二列包含協(xié)議。看起來(lái)無(wú)害的點(diǎn)運(yùn)算符實(shí)際上是一種相當(dāng)普遍的關(guān)系連接，因此你也可以為所有具有協(xié)議 p 的 URL 編寫(xiě) protocol.p，稍后會(huì)有更多這方面的內(nèi)容。

請(qǐng)注意，與 URL 不同，路徑被視為沒(méi)有結(jié)構(gòu)，這是一種簡(jiǎn)化。關(guān)鍵字 lone（可以讀作“小于等于1”）表示每個(gè) URL 最多有一個(gè)端口。路徑是 URL 中主機(jī)名后面的字符串，它（對(duì)于簡(jiǎn)單的靜態(tài)服務(wù)器）對(duì)應(yīng)于資源的文件路徑；我們假設(shè)它總是存在的，但可能是一條空路徑。

讓我們介紹一下客戶端和服務(wù)器，它們都包含從路徑到資源的映射：

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

extends 關(guān)鍵字引入了一個(gè)子集，因此所有客戶端的集合 Client 就是所有端點(diǎn)的集合 Endpoint 的子集。擴(kuò)展是不相交的，因此沒(méi)有端點(diǎn)同時(shí)是客戶端和服務(wù)器。abstract 關(guān)鍵字表示簽名的所有擴(kuò)展都會(huì)繼承它，因此它出現(xiàn)在 Endpoint 聲明中，例如，表示每個(gè)端點(diǎn)必須屬于其中一個(gè)子集（此時(shí)為 Client 和 Server）。對(duì)于服務(wù)器 s，表達(dá)式 s.resources 將表示從路徑到資源的映射（聲明中的箭頭）?；叵胍幌拢總€(gè)字段實(shí)際上都是一個(gè)關(guān)系，第一列包含所有者簽名，因此此字段表示 Server、Path 和 Resource 上的三列關(guān)系。

為了將 URL 映射到服務(wù)器，我們引入了域名服務(wù)器集合 Dns，每個(gè)服務(wù)器都具有從域到服務(wù)器的映射：

one sig Dns {
  map: Domain -> Server
}

簽名聲明中的關(guān)鍵字 one 意味著（為簡(jiǎn)單起見(jiàn)）我們將假設(shè)只有一個(gè)域名服務(wù)器，并且將有一個(gè)由表達(dá)式 DNS.map 給出的DNS映射。同樣，和服務(wù)資源一樣，這可能是動(dòng)態(tài)的（事實(shí)上，在交互過(guò)程中存在依賴于更改 DNS 綁定的已知安全攻擊），但我們進(jìn)行了簡(jiǎn)化。

為了對(duì) HTTP 請(qǐng)求建模，我們還需要 Cookie 的概念，讓我們聲明：

sig Cookie {
  domains: set Domain
}

每個(gè) Cookie 的范圍是一組域；這代表了這樣一個(gè)事實(shí)： Cookie 可以應(yīng)用于 *.mit.edu，它將包括后綴為 mit.edu 的所有域。

最后，我們可以將這些放在一起構(gòu)建 HTTP 請(qǐng)求的模型：

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]
}

我們?cè)趩蝹€(gè)對(duì)象中建模 HTTP 請(qǐng)求和響應(yīng)；url、sentCookies 和 body 由客戶端發(fā)送，而 receivedCookies 和 response 則由服務(wù)器發(fā)回。

在編寫(xiě) HttpRequest 簽名時(shí)，我們發(fā)現(xiàn)它包含調(diào)用的通用特性，即它們來(lái)自和指向特定事物。所以我們實(shí)際上編寫(xiě)了一個(gè)聲明 Call 簽名的小 Alloy 模塊，要在這里使用它，我們需要導(dǎo)入它：

open call[Endpoint]

它是一個(gè)多態(tài)模塊，所以它是用端點(diǎn)實(shí)例化的，調(diào)用的對(duì)象集是 from 和 to。

HttpRequest 中的字段聲明后面是一組約束。這些約束中的每一個(gè)都適用于HTTP請(qǐng)求集的所有成員。約束條件表示（1）每個(gè)請(qǐng)求來(lái)自客戶端，（2）每個(gè)請(qǐng)求都被發(fā)送到 DNS 映射下 URL 主機(jī)指定的一個(gè)服務(wù)器。

Alloy 的一個(gè)顯著特點(diǎn)是，無(wú)論模型多么簡(jiǎn)單或詳細(xì)，都可以隨時(shí)執(zhí)行以生成示例系統(tǒng)實(shí)例。讓我們使用 run 命令要求 Alloy 分析器執(zhí)行到目前為止的 HTTP 模型：

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

一旦分析器找到系統(tǒng)的一個(gè)可能實(shí)例，它就會(huì)自動(dòng)生成一個(gè)實(shí)例圖，如下圖。

fig-http-1.png

此實(shí)例顯示了一個(gè)客戶端（由節(jié)點(diǎn) Client 表示）向 Server 發(fā)送 HttpRequest，服務(wù)器作為響應(yīng)返回一個(gè)資源對(duì)象，并指示客戶端在 Domain 中存儲(chǔ) Cookie。

盡管這是一個(gè)很小的例子，細(xì)節(jié)似乎很少，但它表明我們的模型存在缺陷。請(qǐng)注意，從請(qǐng)求（Resource1）返回的資源在服務(wù)器中不存在。我們忽略了一個(gè)關(guān)于服務(wù)器的明顯事實(shí)；也就是說(shuō)，對(duì)請(qǐng)求的每個(gè)響應(yīng)都是服務(wù)器存儲(chǔ)的資源。我們可以回到 HttpRequest 的定義并添加一個(gè)約束：

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

現(xiàn)在重新運(yùn)行會(huì)生成沒(méi)有該缺陷的實(shí)例。

我們可以要求分析器檢查模型是否滿足屬性，而不是生成示例實(shí)例。例如，我們可能需要的一個(gè)特性是，當(dāng)客戶端多次發(fā)送相同的請(qǐng)求時(shí)，它總是會(huì)收到相同的響應(yīng)：

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

給定此check命令，分析器探索系統(tǒng)的所有可能行為（直到指定的界限），當(dāng)發(fā)現(xiàn)違反屬性的行為時(shí)，將該實(shí)例顯示為反例，如下所示。

fig-http-2a.png

fig-http-2b.png

這個(gè)反例再次顯示了一個(gè)由客戶端發(fā)出的 HTTP 請(qǐng)求，但是使用兩個(gè)不同的服務(wù)器(在Alloy visualizer中，相同類型的對(duì)象通過(guò)在名稱后附加數(shù)字后綴來(lái)區(qū)分；如果給定類型只有一個(gè)對(duì)象，則不添加后綴?？煺贞P(guān)系圖中出現(xiàn)的每個(gè)名稱都是對(duì)象的名稱。因此，乍一看，Domain、Path、Resource、Url 都是指單個(gè)對(duì)象，而不是類型，這可能會(huì)令人困惑。）

請(qǐng)注意，雖然 DNS 將 Domain 映射到 Server0 和 Server1（實(shí)際上，這是負(fù)載平衡的常見(jiàn)做法），但只有 Server1 將 Path 映射到資源對(duì)象，導(dǎo)致 HttpRequest1 產(chǎn)生空響應(yīng)：我們模型中的另一個(gè)錯(cuò)誤。為了解決這個(gè)問(wèn)題，我們添加了一個(gè) Alloy fact記錄 DNS 映射到單個(gè)主機(jī)的任何兩個(gè)服務(wù)器都提供相同的資源集：

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

添加此 fact 后重新運(yùn)行 check 命令時(shí)，分析器不再報(bào)告該屬性的任何反例。這并不意味著這個(gè)屬性已經(jīng)被證明是正確的，因?yàn)樵诟蟮姆秶鷥?nèi)可能會(huì)有一個(gè)反例。但是屬性不太可能為否，因?yàn)榉治銎饕呀?jīng)測(cè)試了所有可能的實(shí)例，每個(gè)實(shí)例都涉及每種類型的3個(gè)對(duì)象。

但是，如果需要，我們可以在更大范圍內(nèi)重新運(yùn)行分析，以增加信心。例如，在范圍為10的情況下運(yùn)行上述檢查仍然不會(huì)產(chǎn)生任何反例，這表明該屬性可能是有效的。但是，請(qǐng)記住，給定更大的范圍，分析器需要測(cè)試更多的實(shí)例，因此可能需要更長(zhǎng)的時(shí)間才能完成。

瀏覽器

現(xiàn)在，讓我們?cè)谀Ｐ椭幸霝g覽器：

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

這是我們第一個(gè)帶有動(dòng)態(tài)字段的簽名示例。Alloy 沒(méi)有內(nèi)置的時(shí)間或行為概念，這意味著可以使用各種習(xí)慣用法。在這個(gè)模型中，我們使用了一個(gè)常見(jiàn)的習(xí)慣用法，在這個(gè)習(xí)慣用法中，你引入了 Time 的概念，并將其作為每個(gè)時(shí)變字段的最后一列。例如，表達(dá)式 b.cookies.t 表示在特定時(shí)間 t 存儲(chǔ)在瀏覽器 b 中的 cookies 集。同樣，documents 字段在給定時(shí)間將一組文檔與每個(gè)瀏覽器關(guān)聯(lián)。

文檔是根據(jù)對(duì) HTTP 請(qǐng)求的響應(yīng)創(chuàng)建的。例如，如果用戶關(guān)閉選項(xiàng)卡或?yàn)g覽器，但我們將其從模型中刪除，它們也會(huì)被銷毀。文檔有一個(gè)URL（文檔的來(lái)源）、一些內(nèi)容（DOM）和一個(gè)域：

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

包含后兩個(gè)字段的 Time 列告訴我們，它們可以隨時(shí)間而變化，而省略第一個(gè)字段（src，表示文檔的源URL）表明源 URL 是固定的。

為了模擬 HTTP 請(qǐng)求對(duì)瀏覽器的影響，我們引入了一個(gè)新的簽名，因?yàn)椴⒎撬?HTTP 請(qǐng)求都源自瀏覽器級(jí)別；其余的將來(lái)自腳本。

/* 從瀏覽器發(fā)送到服務(wù)器的HTTP請(qǐng)求 */
sig BrowserHttpRequest extends HttpRequest { doc: lone Document }{
    -- 請(qǐng)求來(lái)自瀏覽器
    from in Browser
    -- 請(qǐng)求時(shí)瀏覽器中存在正在發(fā)送的cookie
    sentCookies in from.cookies.start
    -- 發(fā)送的每個(gè)cookie都必須限定為請(qǐng)求的url
    matchingScope[sentCookies, url]

    -- 如果沒(méi)有響應(yīng)，則不會(huì)打開(kāi)新文檔
    some doc iff some response
    -- 將創(chuàng)建一個(gè)新文檔以顯示響應(yīng)的內(nèi)容
    documents.end = documents.start + from -> doc
    -- 新文檔將響應(yīng)作為其內(nèi)容
    content.end = content.start ++ doc -> response
    -- 新文檔將url的主機(jī)作為其域
    domain.end = domain.start ++ doc -> url.host
    -- 文檔的源是請(qǐng)求的url
    some doc implies doc.src = url

    -- 瀏覽器會(huì)存儲(chǔ)新的cookie
    cookies.end = cookies.start + from -> sentCookies
}

此類請(qǐng)求有一個(gè)新字段 doc，表示從請(qǐng)求返回的資源在瀏覽器中創(chuàng)建的文檔。與 HttpRequest 一樣，該行為被描述為一組約束。其中一些表示調(diào)用何時(shí)發(fā)生：例如，調(diào)用必須來(lái)自瀏覽器。有些約束調(diào)用的參數(shù)：例如，Cookie 必須被適當(dāng)?shù)叵薅ǚ秶?。還有一些限制效果，使用一種常見(jiàn)的習(xí)慣用法，將調(diào)用后關(guān)系的值與調(diào)用前關(guān)系的值聯(lián)系起來(lái)。

例如，要理解約束 documents.end = documents.start + from -> doc，請(qǐng)記住，在瀏覽器、文檔和時(shí)間上，documents 是三列關(guān)系。字段 start 和 end 來(lái)自 Call 聲明（我們還沒(méi)有看到，但包含在末尾的列表中），表示調(diào)用開(kāi)始和結(jié)束的時(shí)間。表達(dá)式 documents.end 在調(diào)用結(jié)束時(shí)提供從瀏覽器到文檔的映射。因此，該約束表示，在調(diào)用之后，映射是相同的，只是表中的一個(gè)新條目映射 from 到 doc。

某些約束使用 ++ 關(guān)系覆蓋運(yùn)算符：e1 ++ e2 包含 e2 的所有元組，此外，其第一個(gè)元素不是 e2中元組的第一個(gè)元素的任何 e1 元組。例如，content.end = content.start ++ doc -> response 表示在調(diào)用之后， content 映射將更新為將 doc 映射到 response（覆蓋 doc 之前的任何映射）。如果改為使用聯(lián)合運(yùn)算符+，則同一文檔可能（錯(cuò)誤地）映射到處于后續(xù)狀態(tài)的多個(gè)資源。

腳本

接下來(lái)，我們將在 HTTP 和瀏覽器模型的基礎(chǔ)上引入客戶端腳本，這些腳本表示在瀏覽器文檔（context）中執(zhí)行的代碼片段（通常是JavaScript）。

sig Script extends Client { context: Document }

腳本是一個(gè)動(dòng)態(tài)實(shí)體，它可以執(zhí)行兩種不同的操作：（1）它可以發(fā)出 HTTP 請(qǐng)求（即Ajax請(qǐng)求）和（2）它可以執(zhí)行瀏覽器操作來(lái)操作文檔的內(nèi)容和屬性?？蛻舳四_本的靈活性是 Web2.0 快速發(fā)展的主要催化劑之一，也是 SOP 最初創(chuàng)建的原因。如果沒(méi)有 SOP，腳本將能夠向服務(wù)器發(fā)送任意請(qǐng)求，或者自由修改瀏覽器中的文檔，如果一個(gè)或多個(gè)腳本被證明是惡意的，這將是一個(gè)壞消息。

腳本可以通過(guò)發(fā)送 XmlHttpRequest 與服務(wù)器通信：

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

腳本可以使用 XmlHttpRequest 向服務(wù)器發(fā)送/接收資源，但與 BrowserHttpRequest 不同，它不會(huì)立即創(chuàng)建新頁(yè)面或?qū)g覽器及其文檔進(jìn)行其他更改。為了說(shuō)明調(diào)用不會(huì)修改系統(tǒng)的這些方面，我們定義了謂詞 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  
}

腳本可以對(duì)文檔執(zhí)行什么類型的操作？首先，我們引入瀏覽器操作的一般概念，以表示一組可由腳本調(diào)用的瀏覽器 API 函數(shù)：

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 是指此調(diào)用將訪問(wèn)或操作的文檔。簽名事實(shí)中的第二個(gè)約束條件是，doc 和執(zhí)行腳本的文檔（from.context）必須是當(dāng)前存在于瀏覽器中的文檔。最后，BrowserOp 可以修改文檔的狀態(tài)，但不能修改存儲(chǔ)在瀏覽器中的文檔集或 Cookie(實(shí)際上，Cookie可以與文檔關(guān)聯(lián)并使用瀏覽器API進(jìn)行修改，但我們現(xiàn)在省略了這個(gè)細(xì)節(jié)。）

腳本可以讀取和寫(xiě)入文檔的各個(gè)部分（通常稱為 DOM 元素）。在一個(gè)典型的瀏覽器中，有大量用于訪問(wèn) DOM 的 API 函數(shù)（例如 document.getElementById），但是枚舉所有這些函數(shù)對(duì)于我們的目的并不重要。相反，我們將它們簡(jiǎn)單地分為兩類：ReadDom 和 WriteDom，以及作為整個(gè)文檔的整體替換的模型修改：

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 返回目標(biāo)文檔的內(nèi)容，但不修改它；另一方面，WriteDom 將目標(biāo)文檔的新內(nèi)容設(shè)置為 newDom。

此外，腳本可以修改文檔的各種屬性，如寬度、高度、域和標(biāo)題。對(duì)于SOP的討論，我們只對(duì)域?qū)傩愿信d趣，我們將在后面的部分中介紹。

示例應(yīng)用程序

如前所述，給定 run 或 check 命令，Alloy 分析器將生成與模型中系統(tǒng)描述一致的場(chǎng)景（如果存在）。默認(rèn)情況下，分析器任意選擇任何一種可能的系統(tǒng)場(chǎng)景（直到指定的界限），并為場(chǎng)景中的簽名實(shí)例（Server0、Browser1等）分配數(shù)字標(biāo)識(shí)符。

有時(shí)，我們可能希望分析特定 Web 應(yīng)用程序的行為，而不是探索隨機(jī)配置服務(wù)器和客戶端的場(chǎng)景。例如，假設(shè)我們希望構(gòu)建一個(gè)在瀏覽器中運(yùn)行的電子郵件應(yīng)用程序（如Gmail）。除了提供基本的電子郵件功能外，我們的應(yīng)用程序還可能顯示來(lái)自第三方廣告服務(wù)的橫幅，該廣告服務(wù)由潛在的惡意參與者控制。

在 Alloy 中，關(guān)鍵字 one sig 引入了僅包含一個(gè)對(duì)象的單態(tài)簽名；我們?cè)谏厦婵吹搅艘粋€(gè)使用 Dns 的示例。此語(yǔ)法可用于指定具體的原子。例如，要說(shuō)有一個(gè)收件箱頁(yè)面和一個(gè)廣告橫幅（每個(gè)都是文檔），我們可以寫(xiě)：

one sig InboxPage, AdBanner extends Document {}

通過(guò)此聲明，Alloy 生成的每個(gè)場(chǎng)景都將至少包含這兩個(gè) Document 對(duì)象。

同樣，我們可以指定特定的服務(wù)器、域等，并使用約束（我們稱之為 Configuration）來(lái)指定它們之間的關(guān)系：

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
}

例如，事實(shí)中的最后一個(gè)約束指定如何將 DNS 配置為映射系統(tǒng)中兩個(gè)服務(wù)器的域名。如果沒(méi)有此約束，Alloy 分析器可能會(huì)生成將 EmailDomain映射到 EvilServer的場(chǎng)景，我們對(duì)此不感興趣（實(shí)際上，這種映射可能是由于一種稱為DNS欺騙的攻擊造成的，但我們將從我們的模型中排除它，因?yàn)樗粚儆赟OP旨在防止的攻擊類別。）

讓我們介紹另外兩個(gè)應(yīng)用程序：在線日歷和博客站點(diǎn)：

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

我們應(yīng)該更新上面關(guān)于DNS映射的約束，以合并這兩個(gè)服務(wù)器的域名：

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

此外，讓我們假設(shè)電子郵件、博客和日歷應(yīng)用程序都是由單個(gè)組織開(kāi)發(fā)的，因此共享相同的基本域名。從概念上講，我們可以認(rèn)為 EmailServer 和 CalendarServer 具有子域 email 和 calendar，將 example.com 共享為公共超域。在我們的模型中，這可以通過(guò)引入一個(gè)域名包含其它來(lái)表示：

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

注意，由于每個(gè)域名都包含它自己，所以 this 是 subsumes的成員。

關(guān)于這些應(yīng)用程序，我們?cè)谶@里省略了其他細(xì)節(jié)（完整模型見(jiàn) example.als）。但在本文的其余部分，我們將重新討論這些應(yīng)用程序，作為我們的運(yùn)行示例。

安全屬性

在討論 SOP 之前，有一個(gè)重要的問(wèn)題我們還沒(méi)有討論：當(dāng)我們說(shuō)我們的系統(tǒng)是安全的時(shí)，我們到底是什么意思？

毫不奇怪，這是一個(gè)很難回答的問(wèn)題。出于我們的目的，我們將轉(zhuǎn)向信息安全的保密性和完整性這兩個(gè)經(jīng)過(guò)充分研究的概念。這兩個(gè)概念都討論了如何允許信息通過(guò)系統(tǒng)的各個(gè)部分。粗略地說(shuō)，機(jī)密性意味著關(guān)鍵數(shù)據(jù)塊只能被認(rèn)為是可信的部分訪問(wèn)，而完整性意味著可信部分只依賴于未被惡意篡改的數(shù)據(jù)。

數(shù)據(jù)流屬性

為了更精確地指定這些安全屬性，我們首先需要定義一段數(shù)據(jù)從系統(tǒng)的一部分流向另一部分意味著什么。到目前為止，在我們的模型中，我們已經(jīng)將兩個(gè)端點(diǎn)之間的交互描述為通過(guò)調(diào)用執(zhí)行；例如，瀏覽器通過(guò)發(fā)出 HTTP 請(qǐng)求與服務(wù)器交互，腳本通過(guò)調(diào)用瀏覽器 API 操作與瀏覽器交互。直觀地說(shuō)，在每次調(diào)用期間，一段數(shù)據(jù)可能作為調(diào)用的參數(shù)或返回值從一個(gè)端點(diǎn)流向另一個(gè)端點(diǎn)。為了說(shuō)明這一點(diǎn)，我們?cè)谀Ｐ椭幸肓?DataflowCall 的概念，并將每個(gè)調(diào)用與一組 args 和 returns 數(shù)據(jù)字段相關(guān)聯(lián)：

sig Data in Resource + Cookie {}

sig DataflowCall in Call {
  args, returns: set Data,  -- 本次調(diào)用的參數(shù)和返回?cái)?shù)據(jù)
}{
 this in HttpRequest implies
    args = this.sentCookies + this.body and
    returns = this.receivedCookies + this.response
 ...
}

例如，在 HttpRequest 類型的每次調(diào)用期間，客戶端將SentCookies 和 body 傳輸?shù)椒?wù)器，并接收 receivedCookies 和 response 作為返回值。

更一般地說(shuō)，參數(shù)從調(diào)用的發(fā)送方流向接收方，返回值從接收方流向發(fā)送方。這意味著端點(diǎn)訪問(wèn)新數(shù)據(jù)段的唯一方法是將其作為端點(diǎn)接受的調(diào)用的參數(shù)或端點(diǎn)調(diào)用的調(diào)用的返回值接收。我們引入了 DataflowModule 的概念，并分配字段 accesses 以表示模塊在每個(gè)時(shí)間步可以訪問(wèn)的數(shù)據(jù)元素集：

sig DataflowModule in Endpoint {
    -- 此組件擁有的數(shù)據(jù)集
    accesses: Data -> Time
} {
    all d: Data, t: Time - first |
        -- 只有在以下情況下，此端點(diǎn)才能在時(shí)間“t”訪問(wèn)一段數(shù)據(jù)“d”
        d -> t in accesses implies
            -- （1）它在上一時(shí)間步中已具有訪問(wèn)權(quán)限，或
            d -> t.prev in accesses or
            -- 有一些調(diào)用“c”，以“t”結(jié)尾，這樣
            some c: Call & end.t |
                --（2）端點(diǎn)接收帶有“d”作為其參數(shù)之一的“c”，或
                c.to = this and d in c.args or
                --（3）端點(diǎn)發(fā)送返回d的“c”
                c. from = this and d in c.returns

    -- 關(guān)于特定端點(diǎn)的限制
    this in Server implies Path.(this.resources) in initData
}

我們還需要限制模塊可以作為參數(shù)或調(diào)用返回值提供的數(shù)據(jù)元素。否則，我們可能會(huì)遇到一些奇怪的情況，模塊可以使用無(wú)法訪問(wèn)的參數(shù)進(jìn)行調(diào)用。

sig DataflowCall in Call { ... } {
  -- 關(guān)于數(shù)據(jù)流調(diào)用的兩個(gè)一般約束
  --（1）發(fā)送方必須能夠訪問(wèn)任何參數(shù)
  args in from.accesses.start +
  --（除非是Ajax調(diào)用，在這種情況下，參數(shù)可能包括瀏覽器cookie）
      (this in XmlHttpRequest implies from.browser[start].accesses.start & Cookie else none)

  --（2）此調(diào)用返回的任何數(shù)據(jù)必須可供接收方訪問(wèn)
  returns in to.accesses.start
}

現(xiàn)在我們有了描述系統(tǒng)不同部分之間數(shù)據(jù)流的方法，我們（幾乎）已經(jīng)準(zhǔn)備好陳述我們關(guān)心的安全屬性。但請(qǐng)記住，保密性和完整性是與上下文相關(guān)的概念；只有當(dāng)我們可以將系統(tǒng)中的某些代理稱為受信任（或惡意）時(shí)，這些屬性才有意義。同樣，并非所有的信息都同等重要：我們需要區(qū)分我們認(rèn)為是關(guān)鍵或惡意的數(shù)據(jù)元素（或兩者都不）：

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

然后，機(jī)密性屬性可以表示為關(guān)鍵數(shù)據(jù)流入系統(tǒng)不可信部分的斷言：

// 任何惡意模塊都不能訪問(wèn)私有數(shù)據(jù)
assert Confidentiality {
  no m: Module - TrustedModule, t: Time |
    some CriticalData & m.accesses.t 
}

完整性屬性具有雙重保密性：

// 任何惡意數(shù)據(jù)都不應(yīng)進(jìn)入受信任的模塊
assert Integrity {
  no m: TrustedModule, t: Time | 
    some MaliciousData & m.accesses.t
}

威脅模型

威脅模型描述了攻擊者在試圖破壞系統(tǒng)安全屬性時(shí)可能執(zhí)行的一系列操作。建立威脅模型對(duì)任何安全系統(tǒng)的設(shè)計(jì)都是一個(gè)重要步驟；它允許我們識(shí)別關(guān)于系統(tǒng)及其環(huán)境的（可能是無(wú)效的）假設(shè)，并優(yōu)先考慮需要緩解的不同類型的風(fēng)險(xiǎn)。

在我們的模型中，我們考慮一個(gè)可以充當(dāng)服務(wù)器、腳本或客戶端的攻擊者。作為服務(wù)器，攻擊者可能會(huì)設(shè)置惡意網(wǎng)頁(yè)，以請(qǐng)求毫無(wú)戒心的用戶進(jìn)行訪問(wèn)，而這些用戶可能會(huì)在 HTTP 請(qǐng)求中無(wú)意中將敏感信息發(fā)送給攻擊者。攻擊者可能會(huì)創(chuàng)建一個(gè)惡意腳本，調(diào)用 DOM 操作從其他頁(yè)面讀取數(shù)據(jù)，并將這些數(shù)據(jù)中繼到攻擊者的服務(wù)器。最后，作為客戶端，攻擊者可能會(huì)模擬普通用戶并向服務(wù)器發(fā)送惡意請(qǐng)求，試圖訪問(wèn)該用戶的數(shù)據(jù)。我們不認(rèn)為攻擊者竊聽(tīng)不同網(wǎng)絡(luò)端點(diǎn)之間的連接；雖然它在實(shí)踐中是一種威脅，但 SOP 并不是為了防止它而設(shè)計(jì)的，因此它不在我們模型的范圍之內(nèi)。

檢查屬性

現(xiàn)在，我們已經(jīng)定義了安全屬性和攻擊者的行為，讓我們展示如何使用 Alloy 分析器自動(dòng)檢查這些屬性，即使在攻擊者在場(chǎng)的情況下，這些屬性仍然有效。當(dāng)使用 check 命令提示時(shí)，分析器將探索系統(tǒng)中所有可能的數(shù)據(jù)流跟蹤，并生成一個(gè)反例（如果存在）來(lái)演示如何違反斷言：

check Confidentiality for 5

例如，當(dāng)根據(jù)機(jī)密性屬性檢查示例應(yīng)用程序的模型時(shí)，分析器生成下面兩幅圖中的場(chǎng)景，其中顯示了腳本如何訪問(wèn)一段關(guān)鍵數(shù)據(jù)（MyInboxInfo）。

fig-attack-1a.png

fig-attack-1b.png

這個(gè)反例包括兩個(gè)步驟。在第一步中，EvilScript 在來(lái)自 EvilDomain 的 AdBanner 內(nèi)執(zhí)行，讀取 InboxPage 的內(nèi)容。在下一步中，EvilScript 通過(guò)調(diào)用 XmlHtttpRequest 向 EvilServer 發(fā)送相同的內(nèi)容（MyInboxInfo）。這里的核心問(wèn)題是，在一個(gè)域下執(zhí)行的腳本能夠從另一個(gè)域讀取文檔的內(nèi)容；正如我們將在下一節(jié)中看到的，這正是 SOP 旨在防止的場(chǎng)景之一。

一個(gè)斷言可能有多個(gè)反例?？紤]下圖，它顯示了系統(tǒng)可能違反保密屬性的另一種方式。

fig-attack-2.png

在這種場(chǎng)景下，腳本不讀取收件箱頁(yè)面的內(nèi)容，而是直接向 EmailServer 發(fā)出 GetInboxInfo 請(qǐng)求。請(qǐng)注意，請(qǐng)求包含一個(gè) cookie（MyCookie），其作用域與目標(biāo)服務(wù)器的作用域相同。這是潛在的危險(xiǎn)，因?yàn)槿绻?cookie 用于表示用戶的身份（例如，會(huì)話 cookie），則腳本可以有效地偽裝成用戶，并誘使服務(wù)器使用用戶的私有數(shù)據(jù)（MyInboxInfo）進(jìn)行響應(yīng)。這里，問(wèn)題再次與腳本可用于跨不同域訪問(wèn)信息的自由方式有關(guān)，即在一個(gè)域下執(zhí)行的腳本能夠向具有不同域的服務(wù)器發(fā)出 HTTP 請(qǐng)求。

這兩個(gè)反例告訴我們需要額外的措施來(lái)限制腳本的行為，特別是因?yàn)槠渲幸恍┠_本可能是惡意的。這正是 SOP 的用武之地。

同源策略

在我們陳述 SOP 之前，我們應(yīng)該做的第一件事是引入源的概念，它由協(xié)議、主機(jī)和可選端口組成：

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

為了方便起見(jiàn)，讓我們定義一個(gè)函數(shù)，在給定 URL 的情況下，該函數(shù)返回相應(yīng)的源：

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

SOP 本身有兩個(gè)部分，限制腳本（1）進(jìn)行 DOM API 調(diào)用和（2）發(fā)送 HTTP 請(qǐng)求的能力。策略的第一部分規(guī)定，腳本只能讀取和寫(xiě)入與腳本來(lái)源相同的文檔：

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

domSop 下不可能出現(xiàn)（上一節(jié)中的）第一個(gè)腳本場(chǎng)景這樣的實(shí)例，因?yàn)椴辉试S腳本對(duì)來(lái)自不同來(lái)源的文檔調(diào)用 ReadDom。

該策略的第二部分指出，腳本無(wú)法向服務(wù)器發(fā)送 HTTP 請(qǐng)求，除非其上下文與目標(biāo) URL 具有相同的來(lái)源，從而有效地阻止了第二個(gè)腳本場(chǎng)景等實(shí)例。

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

正如我們所見(jiàn)，SOP 旨在防止惡意腳本操作可能產(chǎn)生的兩類漏洞；沒(méi)有它，網(wǎng)絡(luò)將更加危險(xiǎn)。

然而，事實(shí)證明，SOP 可能過(guò)于嚴(yán)格。例如，有時(shí)你確實(shí)希望允許兩個(gè)不同來(lái)源的文檔之間進(jìn)行通信。根據(jù)上述來(lái)源的定義，來(lái)自 foo.example.com 的腳本將無(wú)法讀取 bar.example.com 的內(nèi)容，或向 www.example.com 發(fā)送 HTTP 請(qǐng)求，因?yàn)檫@些都被視為不同的主機(jī)。

為了在必要時(shí)允許某種形式的跨源通信，瀏覽器實(shí)現(xiàn)了各種放松 SOP 的機(jī)制。其中一些經(jīng)過(guò)深思熟慮，一些則存在陷阱，如果使用不當(dāng)，可能會(huì)破壞 SOP 的安全優(yōu)勢(shì)。在下面的部分中，我們將描述這些機(jī)制中最常見(jiàn)的，并討論它們潛在的安全隱患。

繞過(guò) SOP 的技術(shù)

SOP是功能性和安全性之間權(quán)衡的經(jīng)典示例；我們希望確保我們的網(wǎng)站是健壯的和功能強(qiáng)大的，但是保護(hù)它的機(jī)制有時(shí)會(huì)成為障礙。事實(shí)上，當(dāng) SOP 最初引入時(shí)，開(kāi)發(fā)人員在構(gòu)建合法使用跨域通信（例如mashup）的站點(diǎn)時(shí)遇到了麻煩。

在本節(jié)中，我們將討論 Web 開(kāi)發(fā)人員為繞過(guò) SOP 施加的限制而設(shè)計(jì)和經(jīng)常使用的四種技術(shù)：（1）document.domain 屬性松弛；(2） JSONP；(3） PostMessage；和（4）CORS。這些都是很有用的工具，但如果不小心使用，可能會(huì)使 Web 應(yīng)用程序容易受到 SOP 最初設(shè)計(jì)用來(lái)阻止的攻擊類型的攻擊。

這四種技術(shù)中的每一種都非常復(fù)雜，詳細(xì)描述需要專門的章節(jié)。所以這里我們只是簡(jiǎn)單介紹一下它們是如何工作的，它們帶來(lái)的潛在安全問(wèn)題，以及如何預(yù)防這些問(wèn)題。特別是，我們將要求 Alloy 分析器檢查每種技術(shù)是否會(huì)被攻擊者濫用以破壞我們之前定義的兩個(gè)安全屬性：

check Confidentiality for 5
check Integrity for 5

根據(jù)分析器生成的反例，我們將討論安全使用這些技術(shù)而不落入安全陷阱的指導(dǎo)原則。

域?qū)傩?/h3>

作為我們列表中的第一項(xiàng)技術(shù)，我們將使用 document.domain 屬性作為繞過(guò) SOP 的方法。這種技術(shù)背后的思想是，只需將 document.domain 屬性設(shè)置為相同的值，即可允許來(lái)自不同來(lái)源的兩個(gè)文檔訪問(wèn)彼此的 DOM。因此，例如，如果兩個(gè)文檔中的腳本都將 document.domain 屬性設(shè)置為 example.com（假設(shè)兩個(gè)源 URL 也具有相同的協(xié)議和端口），則 email.example.com 中的腳本可以讀取或?qū)懭?calendar.example.com 中文檔的 DOM。

我們將 document.domain 屬性的設(shè)置行為建模為一種稱為 SetDomain 的瀏覽器操作：

// 修改 document.domain 屬性
sig SetDomain extends BrowserOp { newDomain: Domain }{
  doc = from.context
  domain.end = domain.start ++ doc -> newDomain
  -- 文件內(nèi)容無(wú)任何更改
  content.end = content.start
}

newDomain 字段表示屬性應(yīng)設(shè)置為的值。不過(guò)有一個(gè)警告：腳本只能將域?qū)傩栽O(shè)置為其主機(jī)名的右側(cè)完全限定片段(例如，email.example.com 可以將其設(shè)置為 example.com，但不能設(shè)置為 google.com。）我們使用一個(gè)事實(shí)來(lái)捕獲關(guān)于子域的規(guī)則：

// 腳本只能將域?qū)傩栽O(shè)置為其主機(jī)名的右側(cè)完全限定片段
fact setDomainRule {
  all d: Document | d.src.host in (d.domain.Time).subsumes
}

如果沒(méi)有此規(guī)則，任何站點(diǎn)都可以將 document.domain 屬性設(shè)置為任何值，這意味著，例如，惡意站點(diǎn)可以將域?qū)傩栽O(shè)置為你的銀行域，在嵌套頁(yè)面中加載你的銀行帳戶，并且（假設(shè)銀行頁(yè)面已設(shè)置其域?qū)傩裕┳x取你銀行頁(yè)面的 DOM。

讓我們回到 SOP 的原始定義，并放寬其對(duì) DOM 訪問(wèn)的限制，以便考慮 document.domain 屬性的影響。如果兩個(gè)腳本將屬性設(shè)置為相同的值，并且它們具有相同的協(xié)議和端口，那么這兩個(gè)腳本可以相互交互（即，讀取和寫(xiě)入彼此的 DOM）。

fact domSop {
  -- 對(duì)于每個(gè)成功的讀/寫(xiě) DOM 操作，
    all o: ReadDom + WriteDom | let target = o.doc, caller = o.from.context |
        -- 調(diào)用文檔和目標(biāo)文檔來(lái)自同一來(lái)源，或
        origin[target] = origin[caller] or
        -- --兩個(gè)文檔的域?qū)傩远家研薷?        (target + caller in (o.prevs <: SetDomain).doc and
            -- ...它們已匹配源的值。
            currOrigin[target, o.start] = currOrigin[caller, o.start])
}

這里，currOrigin[d, t] 是一個(gè)函數(shù)，它返回文檔 d 的源，屬性document.domain 在時(shí)間 t 將其作為其主機(jī)名。

值得指出的是，兩個(gè)文檔的 document.domain 屬性必須在加載到瀏覽器后的某個(gè)時(shí)間進(jìn)行明確設(shè)置。假設(shè)文檔 A 是從 example.com 加載的，而 calendar.example.com 中的文檔 B 的域?qū)傩员恍薷臑?example.com。即使這兩個(gè)文檔現(xiàn)在具有相同的域?qū)傩?，它們也無(wú)法相互交互，除非文檔 A 也明確地將其屬性設(shè)置為 example.com。起初，這似乎是一種相當(dāng)奇怪的行為。然而，沒(méi)有這一點(diǎn)，各種各樣的壞事都可能發(fā)生。例如，站點(diǎn)可能會(huì)受到來(lái)自其子域的跨站點(diǎn)腳本攻擊：文檔 B 中的惡意腳本可能會(huì)將其域?qū)傩孕薷臑?code>example.com并操縱文檔 A 的 DOM，即使后者從未打算與文檔 B 交互。

分析：既然我們已經(jīng)放寬了 SOP，允許在某些情況下進(jìn)行跨源通信，SOP 的安全保障是否仍然有效？讓我們讓 Alloy 分析器告訴我們，攻擊者是否會(huì)濫用 document.domain 屬性來(lái)訪問(wèn)或篡改用戶的敏感數(shù)據(jù)。

事實(shí)上，考慮到 SOP 的新的、寬松的定義，分析器生成了機(jī)密性屬性的反例場(chǎng)景：

check Confidentiality for 5

該場(chǎng)景包括五個(gè)步驟；前三個(gè)步驟顯示 document.domain 的典型用法，其中來(lái)自不同源的兩個(gè)文檔 CalendarPage 和 InboxPage 通過(guò)將其域?qū)傩栽O(shè)置為公共值（ExampleDomain）進(jìn)行通信。最后兩個(gè)步驟引入了另一個(gè)文檔 BlogPage，該文檔已被惡意腳本破壞，該腳本試圖訪問(wèn)其他兩個(gè)文檔的內(nèi)容。

在場(chǎng)景開(kāi)始時(shí)，InboxPage 和 CalendarPage 具有兩個(gè)不同值的域?qū)傩裕ǚ謩e為 EmailDomain 和 ExampleDomain），因此瀏覽器將阻止它們?cè)L問(wèn)彼此的 DOM。文檔中運(yùn)行的腳本（InboxScript 和 CalendarScript）分別執(zhí)行 SetDomain 操作，以將其域?qū)傩孕薷臑?code>ExampleDomain（這是允許的，因?yàn)?ExampleDomain 是原始域的超級(jí)域）。

fig-setdomain-1a.png

fig-setdomain-1b.png

完成此操作后，它們現(xiàn)在可以通過(guò)執(zhí)行 ReadDom 或 WriteDom 操作來(lái)訪問(wèn)彼此的 DOM。

fig-setdomain-1c.png

請(qǐng)注意，當(dāng)你將 email.example.com 和 calendar.example.com 的域設(shè)置為 example.com 時(shí)，你不僅允許這兩個(gè)頁(yè)面相互通信，還允許 example.com 作為超級(jí)域的任何其他頁(yè)面（例如 blog.example.com）。攻擊者也意識(shí)到了這一點(diǎn)，并構(gòu)造了一個(gè)在攻擊者的博客頁(yè)面（BlogPage）內(nèi)運(yùn)行的特殊腳本（EvilScript）。在下一步中，腳本執(zhí)行 setdomain操作，將 BlogPage 的域?qū)傩孕薷臑?ExampleDomain。

fig-setdomain-2a.png

既然 BlogPage 與其他兩個(gè)文檔具有相同的域?qū)傩裕涂梢猿晒Φ貓?zhí)行 ReadDOM 操作來(lái)訪問(wèn)它們的內(nèi)容。

fig-setdomain-2b.png

此攻擊指出了用于跨源通信的域?qū)傩苑椒ǖ囊粋€(gè)關(guān)鍵弱點(diǎn)：使用此方法的應(yīng)用程序的安全性僅與共享同一基本域的所有頁(yè)面中最薄弱的鏈接一樣強(qiáng)。我們將很快討論另一種稱為 PostMessage 的方法，它可以用于更一般的跨源通信，同時(shí)也更安全。

帶填充的JSON（JSONP）

在引入 CORS（我們將很快討論）之前，JSONP 可能是繞過(guò) XMLHttpRequest 上的 SOP 限制的最流行的技術(shù)，至今仍被廣泛使用。JSONP 利用了這樣一個(gè)事實(shí)，即 HTML 中的腳本包含標(biāo)記（即<script>）不受 SOP* 的約束；也就是說(shuō)，你可以包含來(lái)自任何 URL 的腳本，并且瀏覽器可以在當(dāng)前文檔中隨時(shí)執(zhí)行該腳本：

（*如果沒(méi)有此豁免，就不可能從其他域加載 JavaScript 庫(kù)，如JQuery）

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

腳本標(biāo)記可以用來(lái)獲取代碼，但是我們?nèi)绾问褂盟鼜牟煌挠蚪邮杖我鈹?shù)據(jù)（例如 JSON 對(duì)象）？問(wèn)題是瀏覽器希望 src 的內(nèi)容是一段 JavaScript 代碼，因此簡(jiǎn)單地將其指向數(shù)據(jù)源（例如 JSON 或 HTML 文件）會(huì)導(dǎo)致語(yǔ)法錯(cuò)誤。

一種解決方法是將所需數(shù)據(jù)包裝在一個(gè)字符串中，瀏覽器將該字符串識(shí)別為有效的 JavaScript 代碼；此字符串有時(shí)稱為 padding（因此名為“帶填充的 JSON”）。此填充可以是任意 JavaScript 代碼，但按照慣例，它是要對(duì)響應(yīng)數(shù)據(jù)執(zhí)行的回調(diào)函數(shù)（已在當(dāng)前文檔中定義）的名稱：

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

www.example.com 上的服務(wù)器將其識(shí)別為 JSONP 請(qǐng)求，并將請(qǐng)求的數(shù)據(jù)包裝在 JSONP 參數(shù)中：

processData(mydata)

它是一個(gè)有效的 JavaScript 語(yǔ)句（即函數(shù)“processData”在值“mydata”上的應(yīng)用），由瀏覽器在當(dāng)前文檔中執(zhí)行。

在我們的模型中，JSONP 被建模為一種 HTTP 請(qǐng)求，在字段填充中包含回調(diào)函數(shù)的標(biāo)識(shí)符。在接收到 JSONP 請(qǐng)求后，服務(wù)器返回一個(gè)響應(yīng)，該響應(yīng)將請(qǐng)求的資源（payload）包裝在回調(diào)函數(shù)（cb）中。

sig CallbackID {}  // 回調(diào)函數(shù)的標(biāo)識(shí)符
// 由于 <script> 標(biāo)記而發(fā)送的請(qǐng)求
sig JsonpRequest in BrowserHttpRequest {
  padding: CallbackID
}{
  response in JsonpResponse
}
sig JsonpResponse in Resource {
  cb: CallbackID,
  payload: Resource
}

當(dāng)瀏覽器收到響應(yīng)時(shí)，它對(duì)有效負(fù)載執(zhí)行回調(diào)函數(shù)：

sig JsonpCallback extends EventHandler {
  cb: CallbackID,
  payload: Resource
}{
  causedBy in JsonpRequest
  let resp = causedBy.response | 
    cb = resp.@cb and
    -- JSONP請(qǐng)求的結(jié)果作為參數(shù)傳遞給回調(diào)
    payload = resp.@payload
}

（EventHandler 是一種特殊類型的調(diào)用，必須在另一個(gè)調(diào)用之后的某個(gè)時(shí)間發(fā)生，由 causedBy 表示；我們將使用事件處理程序?qū)δ_本為響應(yīng)瀏覽器事件而執(zhí)行的操作進(jìn)行建模。）

請(qǐng)注意，執(zhí)行的回調(diào)函數(shù)與響應(yīng)中包含的回調(diào)函數(shù)相同（cb = resp.@cb），但不一定與原始 JSONP 請(qǐng)求中的填充相同。換句話說(shuō)，為了讓 JSONP 通信正常工作，服務(wù)器負(fù)責(zé)正確地構(gòu)造一個(gè)響應(yīng)，其中包含原始填充作為回調(diào)函數(shù)（即，確保 JsonRequest.padding = JsonpResponse.cb）。原則上，服務(wù)器可以選擇包含任何回調(diào)函數(shù)（或任何一段 JavaScript），包括與請(qǐng)求中的填充無(wú)關(guān)的回調(diào)函數(shù)。這突出了 JSONP 的一個(gè)潛在風(fēng)險(xiǎn)：接受 JSONP 請(qǐng)求的服務(wù)器必須是可信和安全的，因?yàn)樗軌驁?zhí)行客戶端文檔中的任何 JavaScript 代碼。

分析：使用 Alloy 分析器檢查機(jī)密性屬性會(huì)返回一個(gè)反例，顯示 JSONP 的一個(gè)潛在安全風(fēng)險(xiǎn)。在此場(chǎng)景中，日歷應(yīng)用程序（CalendarServer）使用 JSONP 端點(diǎn)（GetSchedule）將其資源提供給第三方站點(diǎn)。為了限制對(duì)資源的訪問(wèn)，CalendarServer 僅在請(qǐng)求包含正確標(biāo)識(shí)該用戶的 cookie 時(shí)，才返回帶有用戶計(jì)劃的響應(yīng)。

注意，一旦服務(wù)器提供 HTTP 端點(diǎn)作為 JSONP 服務(wù)，任何人都可以向它發(fā)出 JSONP 請(qǐng)求，包括惡意站點(diǎn)。在這個(gè)場(chǎng)景中，EvilServer 的廣告橫幅頁(yè)面包含一個(gè) script 標(biāo)記，該標(biāo)記導(dǎo)致一個(gè) GetSchedule請(qǐng)求，并使用一個(gè)名為 Leak 的回調(diào)函數(shù)作為填充。通常，AdBanner 的開(kāi)發(fā)人員無(wú)法直接訪問(wèn) CalendarServer的受害用戶會(huì)話 cookie（MyCookie）。但是，由于 JSONP 請(qǐng)求被發(fā)送到 CalendarServer，瀏覽器會(huì)自動(dòng)將 MyCookie 作為請(qǐng)求的一部分；CalendarServer 接收到帶有 MyCookie 的 JSONP 請(qǐng)求后，將返回包裝在填充 Leak 中的受害者資源（MySchedule）。

fig-jsonp-1.png

在下一步中，瀏覽器將 JSONP 響應(yīng)解釋為對(duì) Leak（MySchedule） 調(diào)用。攻擊的剩余部分很簡(jiǎn)單；Leak 可以簡(jiǎn)單地編程為將輸入?yún)?shù)轉(zhuǎn)發(fā)到 EvilServer，從而允許攻擊者訪問(wèn)受害者的敏感信息。

fig-jsonp-2.png

此攻擊是跨站點(diǎn)請(qǐng)求偽造（CSRF）的一個(gè)示例，顯示了 JSONP 的固有弱點(diǎn)；Web 上的任何站點(diǎn)都可以通過(guò)包含 <script> 標(biāo)記并訪問(wèn)填充中的有效負(fù)載來(lái)發(fā)出 JSONP 請(qǐng)求。可以通過(guò)兩種方式降低風(fēng)險(xiǎn)：（1）確保 JSONP 請(qǐng)求從不返回敏感數(shù)據(jù)，或者（2）使用另一種機(jī)制代替 cookie（例如，秘密令牌）來(lái)授權(quán)請(qǐng)求。

PostMessage

PostMessage 是 HTML5 中的一項(xiàng)新功能，它允許來(lái)自兩個(gè)文檔（可能源不同）的腳本相互通信。它提供了一種比設(shè)置域?qū)傩愿鼑?yán)格的方法，但也帶來(lái)了自身的安全風(fēng)險(xiǎn)。

PostMessage 是一個(gè)瀏覽器 API 函數(shù)，它接受兩個(gè)參數(shù)：（1）要發(fā)送的數(shù)據(jù)（message）和（2）接收消息的文檔的源（targetOrigin）：

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

要從另一個(gè)文檔接收消息，接收文檔會(huì)注冊(cè)一個(gè)事件處理程序，瀏覽器會(huì)根據(jù) PostMessage 調(diào)用該事件處理程序：

sig ReceivedMessage extends EventHandler {
    data: Resource,
    srcOrigin: Origin
}{
    causedBy in PostMessage
    -- “ReceiveMessage”事件被發(fā)送到具有正確上下文的腳本
    origin[to.context.src] = causedBy.targetOrigin
    -- 消息匹配
    data = causedBy.@message
    --發(fā)送方腳本的源作為“srcOrigin”參數(shù)提供
    srcOrigin = origin[causedBy.@from.context.src]
}

瀏覽器向 ReceiveMessage 傳遞兩個(gè)參數(shù)：與正在發(fā)送的消息相對(duì)應(yīng)的資源（data）和發(fā)送方文檔的源（srcOrigin）。簽名事實(shí)包含四個(gè)約束，以確保每個(gè) ReceiveMessage 相對(duì)于其相應(yīng)的 PostMessage 格式正確。

分析：再次詢問(wèn) Alloy 分析器 PostMessage 是否是執(zhí)行跨源通信的安全方式。這一次，分析器返回 Integrity 屬性的反例，這意味著攻擊者能夠利用 PostMessage 中的弱點(diǎn)將惡意數(shù)據(jù)引入受信任的應(yīng)用程序。

請(qǐng)注意，默認(rèn)情況下，PostMessage 機(jī)制不限制允許發(fā)送 PostMessage 的用戶；換句話說(shuō)，任何文檔都可以向另一個(gè)文檔發(fā)送消息，只要后者已注冊(cè) ReceiveMessage 處理程序。例如，在以下由 Alloy 生成的實(shí)例中，在 AdBanner 中運(yùn)行的 EvilScript 向目標(biāo)源為 EmailDomain 的文檔發(fā)送惡意 PostMessage。

fig-postmessage-1.png

然后，瀏覽器將此消息轉(zhuǎn)發(fā)到具有相應(yīng)源（在本例中為 InboxPage）的文檔。除非 InboxScript 專門檢查 srcOrigin 的值以過(guò)濾掉不需要的源的消息，否則 InboxPage 將接受惡意數(shù)據(jù)，可能導(dǎo)致進(jìn)一步的安全攻擊(例如，它可能嵌入一段 JavaScript 來(lái)執(zhí)行 XSS 攻擊。）如下圖所示。

fig-postmessage-2.png

如本例所示，PostMessage 在默認(rèn)情況下是不安全的，接收文檔有責(zé)任額外檢查 srcOrigin 參數(shù)，以確保消息來(lái)自可靠的文檔。不幸的是，在實(shí)踐中，許多網(wǎng)站忽略了此檢查，從而使惡意文檔能夠作為 PostMessage^[1] 的一部分插入錯(cuò)誤內(nèi)容。

然而，省略源檢查可能不僅僅是程序員無(wú)知的結(jié)果。對(duì)傳入的 PostMessage 執(zhí)行適當(dāng)?shù)臋z查可能很棘手；在某些應(yīng)用程序中，很難預(yù)先確定預(yù)期從中接收消息的可信源列表(在某些應(yīng)用程序中，此列表甚至可能會(huì)動(dòng)態(tài)更改。）這再次凸顯了安全性和功能性之間的緊張關(guān)系：PostMessage 可用于安全的跨源通信，但只有在已知可信源白名單的情況下。

跨源資源共享（CORS）

跨源資源共享（CORS）是一種允許服務(wù)器與來(lái)自不同源的站點(diǎn)共享其資源的機(jī)制。特別是，來(lái)自一個(gè)源的腳本可以使用 CORS 向具有不同源的服務(wù)器發(fā)出請(qǐng)求，從而有效地繞過(guò) SOP 對(duì)跨源 Ajax 請(qǐng)求的限制。

簡(jiǎn)單地說(shuō)，典型的 CORS 過(guò)程包括兩個(gè)步驟：（1）希望從外部服務(wù)器訪問(wèn)資源的腳本在其請(qǐng)求中包括一個(gè)“源”頭，該頭指定腳本的源；（2）服務(wù)器包括一個(gè)“訪問(wèn)控制允許源”頭作為其響應(yīng)的一部分，指示允許訪問(wèn)服務(wù)器資源的一組源。通常，在沒(méi)有 CORS 的情況下，瀏覽器首先會(huì)阻止腳本根據(jù) SOP 發(fā)出跨源請(qǐng)求。但是，在啟用 CORS 的情況下，瀏覽器允許腳本發(fā)送請(qǐng)求并訪問(wèn)其響應(yīng)，但前提是“源”是“訪問(wèn)控制允許源”中指定的源之一。

（CORS 還包括 preflight 請(qǐng)求的概念（此處未討論），以支持 GET 和 POST 之外的復(fù)雜類型的跨源請(qǐng)求。）

在 Alloy 中，我們將 CORS 請(qǐng)求建模為一種特殊類型的 XmlHttpRequest，具有兩個(gè)額外字段 origin 和 allowedOrigins：

sig CorsRequest in XmlHttpRequest {
    -- 來(lái)自客戶端的請(qǐng)求中的“origin”報(bào)文頭
    origin: Origin
    -- 服務(wù)器響應(yīng)中的“"access-control-allow-origin”報(bào)文頭
    allowedOrigins: set Origin
}{
    from in Script
}

然后，我們使用 Alloy 事實(shí) corsRule 來(lái)描述什么構(gòu)成有效的 CORS 請(qǐng)求：

fact corsRule {
    all r: CorsRequest |
        -- CORS請(qǐng)求的原始報(bào)文頭與腳本上下文匹配
        r.origin = origin[r.from.context.src] and
        -- 指定的源是允許的源之一
        r.origin in r.allowOrigins
}

分析： CORS是否會(huì)被濫用，從而使攻擊者危害受信任站點(diǎn)的安全？當(dāng)出現(xiàn)提示時(shí)，Alloy 分析器返回 Confidentiality 屬性的簡(jiǎn)單反例。

在這里，日歷應(yīng)用程序的開(kāi)發(fā)人員決定使用 CORS 機(jī)制與其他應(yīng)用程序共享一些資源。不幸的是，CalendarServer 配置為在 CORS 響應(yīng)中返回 access-control-allow-origin 報(bào)文頭的 Origin（表示所有源的集合）。因此，允許來(lái)自任何源（包括 EvilDomain）的腳本向 CalendarServer 發(fā)出跨站點(diǎn)請(qǐng)求并讀取其響應(yīng)。

fig-cors.png

這個(gè)例子強(qiáng)調(diào)了開(kāi)發(fā)人員在 CORS 中犯的一個(gè)常見(jiàn)錯(cuò)誤：使用通配符值“*”作為“access-control-allow-origin”報(bào)文頭的值，允許任何站點(diǎn)訪問(wèn)服務(wù)器上的資源。如果資源被認(rèn)為是公共的并且任何人都可以訪問(wèn)，那么這種訪問(wèn)模式是合適的。然而，事實(shí)證明，許多站點(diǎn)甚至將“*”用作私有資源的默認(rèn)值，無(wú)意中允許惡意腳本通過(guò) CORS 請(qǐng)求訪問(wèn)它們^[2]。

為什么開(kāi)發(fā)人員會(huì)使用通配符？事實(shí)證明，指定允許的源可能很棘手，因?yàn)樵谠O(shè)計(jì)時(shí)可能不清楚哪些源應(yīng)該在運(yùn)行時(shí)被授予訪問(wèn)權(quán)限（類似于上面討論的 PostMessage 問(wèn)題）。例如，服務(wù)可以允許第三方應(yīng)用程序動(dòng)態(tài)訂閱其資源。

總結(jié)

在本文中，我們著手構(gòu)建一個(gè)文檔，通過(guò)用一種稱為 Alloy 的語(yǔ)言構(gòu)建一個(gè)策略模型，提供對(duì) SOP 及其相關(guān)機(jī)制的清晰理解。我們的 SOP 模型不是傳統(tǒng)意義上的實(shí)現(xiàn)，不能部署使用，這與其他章節(jié)中顯示的工件不同。相反，我們希望展示“敏捷建?！狈椒ū澈蟮年P(guān)鍵要素：（1）從系統(tǒng)的小型抽象模型開(kāi)始，并在必要時(shí)逐步添加細(xì)節(jié)，（2）指定系統(tǒng)預(yù)期滿足的屬性，（3）應(yīng)用嚴(yán)格的分析來(lái)探索系統(tǒng)設(shè)計(jì)中的潛在缺陷。當(dāng)然，本章是在 SOP 首次引入之后很久才編寫(xiě)的，但我們相信，如果在系統(tǒng)設(shè)計(jì)的早期階段進(jìn)行，這種建?？赡軙?huì)更加有益。

除了 SOP 之外，Alloy 還被用于對(duì)網(wǎng)絡(luò)協(xié)議、語(yǔ)義 Web、字節(jié)碼安全、電子投票和醫(yī)療系統(tǒng)等不同領(lǐng)域的各種系統(tǒng)進(jìn)行建模和推理。對(duì)于這些系統(tǒng)，Alloy 的分析發(fā)現(xiàn)了設(shè)計(jì)缺陷和 BUG，在某些情況下，開(kāi)發(fā)人員多年來(lái)一直沒(méi)有發(fā)現(xiàn)這些缺陷和 BUG。我們邀請(qǐng)我們的讀者訪問(wèn) Alloy 頁(yè)面，嘗試構(gòu)建他們喜愛(ài)的系統(tǒng)模型！

附錄：在 Alloy 中重復(fù)使用模塊

如本文前面所述，Alloy 不對(duì)所建模系統(tǒng)的行為進(jìn)行假設(shè)。由于缺乏內(nèi)置的范例，用戶可以使用基本語(yǔ)言結(jié)構(gòu)的一小部分核心對(duì)廣泛的建模習(xí)慣用法進(jìn)行編碼。例如，我們可以將系統(tǒng)指定為狀態(tài)機(jī)、具有復(fù)雜不變量的數(shù)據(jù)模型、具有全局時(shí)鐘的分布式事件模型，或者任何最適合當(dāng)前問(wèn)題的習(xí)慣用法。常用習(xí)慣用法可以作為通用模塊捕獲，并在多個(gè)系統(tǒng)中重用。

在我們的 SOP 模型中，我們將系統(tǒng)建模為一組端點(diǎn)，這些端點(diǎn)通過(guò)一個(gè)或多個(gè) call 相互通信。由于 call 是一個(gè)相當(dāng)通用的概念，我們將其描述封裝在一個(gè)單獨(dú)的 Alloy 模塊中，從依賴它的其他模塊中導(dǎo)入——類似于編程語(yǔ)言中的標(biāo)準(zhǔn)庫(kù)：

module call[T] 

在這個(gè)模塊聲明中，T 表示一個(gè)類型參數(shù)，該參數(shù)可以實(shí)例化為導(dǎo)入模塊時(shí)提供的具體類型。我們將很快看到如何使用此類型參數(shù)。

通?？梢苑奖愕貙⑾到y(tǒng)執(zhí)行描述為在全局時(shí)間范圍內(nèi)發(fā)生，這樣我們就可以將調(diào)用描述為發(fā)生在彼此之前或之后（或同時(shí)發(fā)生）。為了表示時(shí)間的概念，我們引入了一個(gè)新的簽名，稱為 Time：

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

在 Alloy 中，util/ordering 是一個(gè)內(nèi)置模塊，它對(duì)類型參數(shù)施加總順序，因此通過(guò)導(dǎo)入 ordering[Time]，我們可以獲得一組 Time 對(duì)象，其行為類似于其他全順序集（例如，自然數(shù)）。

請(qǐng)注意，Time 沒(méi)有什么特別之處；我們可以將其命名為任何其他方式（例如，Step 或 State），它根本不會(huì)改變模型的行為。我們?cè)谶@里所做的就是在關(guān)系中使用一個(gè)額外的列，作為表示系統(tǒng)執(zhí)行中不同點(diǎn)的字段內(nèi)容的一種方式；例如，Browser 簽名中的 cookies 。從這個(gè)意義上講，Time對(duì)象只是用作索引的助手對(duì)象。

每個(gè)調(diào)用發(fā)生在兩個(gè)時(shí)間點(diǎn)之間，即 start 和 end，并與發(fā)送方（由 from 表示）和接收方（to 表示）關(guān)聯(lián)：

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

回想一下，在我們對(duì) HTTP 請(qǐng)求的討論中，我們通過(guò)將端點(diǎn)作為其類型參數(shù)傳遞來(lái)導(dǎo)入模塊調(diào)用。結(jié)果，參數(shù)類型 T 被實(shí)例化為 Endpoint，我們獲得了一組與一對(duì)發(fā)送方和接收方端點(diǎn)關(guān)聯(lián)的 Call 對(duì)象。一個(gè)模塊可以多次導(dǎo)入；例如，我們可以聲明一個(gè)名為 UnixProcess 的簽名，并實(shí)例化模塊 call 以獲得從一個(gè) Unix 進(jìn)程發(fā)送到另一個(gè) Unix 進(jìn)程的一組不同的 Call 對(duì)象。

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。 ?