Наши партнеры

UnixForum

Библиотека сайта rus-linux.net

Кросс-доменные ограничения

Оригинал:The Same-Origin Policy
Авторы: Eunsuk Kang, Santiago Perez De Rosso, and Daniel Jackson,
Дата публикации: July 12, 2016
Перевод: Н.Ромоданов
Дата перевода: январь 2017 г.

Это вторая часть статьи "Кросс-доменные ограничения".
Перейти к началу статьи.

Модель веба

Протокол HTTP

Первым шагом в построении модели Alloy является объявление нескольких наборов объектов. Давайте начнем с ресурсов: 

sig Resource {}

Ключевое слово sig используется здесь в качестве объявления сигнатуры (signature) языка Alloy. Здесь определяется набор объектов ресурсов; рассматривайте их просто как объекты класса, у которого нет переменных экземпляров, наподобие блобов (больших объектов), у которые имеют идентичность, но не имеют содержания. Когда будет запущен анализ, этот набор будет определен точно также, как в объектно-ориентированном языке определяется множество объектов при выполнении программа.

Ресурсы именуются с помощью 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, а во втором столбце содержатся протоколы. И безобидный на вид оператор точки, является, на самом деле, операцией реляционного объединения, поэтому вы могли бы также написать protocol.p для всех адресов URL с протоколом р, но об этом позже.

Обратите внимание, что пути, в отличие от адресов URL, рассматриваются, как будто у них нет структуры — это упрощение. Ключевое слово lone (который можно прочитать как "less than or equal to one" -"меньше одного или равно точно одному") указывает, что у каждого 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, нам также нужно понятие куки (cookies), так что давайте их объявим:

sig Cookie {
  domains: set Domain
}

Каждый куки имеет область действия с множеством доменов; это отражает тот факт, что куки могут применяться к выражению *.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 и тело посылаются клиентом, а receivedCookies и response отправляются обратно сервером.

При написании сигнатуры HttpRequest мы обнаружили, что в ней содержатся общие свойства вызовов, а именно, что они от конкретных элементов и к конкретным элементам. Так что мы, на самом деле, написал небольшой модуль на языке Alloy, объявляющий сигнатуру вызова Call, и чтобы его здесь использовать, нам необходимо его импортировать:

open call[Endpoint]

Это полиморфный модуль, поэтому он инстанцирован с использованием Endpoint, множества, определяющего кого он вызывает и откуда он вызывается. (Модуль полностью приведен в Приложении: Повторное использование модулей в языке Alloy).

После объявления полей в HttpRequest представляет собой набор ограничений. Каждое из этих ограничений применяется ко всем членам множества запросов HTTP. В ограничениях говорится, что (1) каждый запрос должен исходит от клиента, и (2) каждый запрос отправляется на один из серверов, указанных адресе URL хоста, отображение которого установлено в DNS.

Одной из отличительных особенностей языка Alloy состоит в том, что модель, независимо от того, насколько она проста или подробна, может быть выполнена в любой момент времени с тем, чтобы создать экземпляры примеров системы. Давайте воспользуемся командой run для того, чтобы попросить анализатор Alloy Analyzer выполнить модель HTTP, которая у нас уже построена к данному моменту:

run {} for 3    -- генерирует экземпляр системы, имеющей до 3 объектов для сигнатуры каждого типа

Как только анализатор обнаруживает возможный экземпляр системы, он автоматически создает схему, например, такую, как показана на рис.17.1.

Рис.17.1. Возможный вариант (экземпляр) системы

В этом варианте (экземпляре) системе показано, что клиент (представленный узлом Client) отправляет запрос HttpRequest на Server, который, в ответ, возвращает объект ресурса и инструктирует клиента сохранить куки 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.

Рис.17.2. Контрпример в момент 0

Рис.17.3. Контрпример в момент 1

В этом контрпримере еще раз показано, что запрос HTTP делается клиентом, но с двумя разными серверами. (В визуализаторе языка Alloy объекты одного и того же типа отличаются добавлением числовых суффиксом к их именам; если есть только один объект данного типа, то суффикс не добавляется. Каждое имя, которое отображается на диаграмме, является именем объекта. Поэтому, возможно, что на первый взгляд смущает, имена Domain, Path, Resource, Url относятся к отдельным объектам, а не к типам).

Обратите внимание, хотя DNS отображает домен Domain как на Server0, так и на Server1 (на самом деле, это обычная практика в случае балансировки нагрузки), только для сервера Server1 путь Path отображается к объекту ресурсов, в результате чего запрос HttpRequest1 приведет к пустому ответу: это еще ошибка в нашей модели. Чтобы это исправить, мы добавим конструкцию fact языка Alloy, в которой записано, что любые два сервера, для которых в DNS есть отображение на один и тот же хост, представляют собой один и тот же набор ресурсов:

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

Когда после добавления этого факта мы повторно запустим команду chec, анализатор больше не выдаст для этого свойства никаких контрпримеров. Это не значит, что такое свойство абсолютно истинно, т. к. контрпример может появиться в случае, если мы расширим количество используемых объектов. Однако, маловероятно, что данное свойство ложно, поскольку анализатор проверил все возможные случаи с использованием 3 объектов каждого типа.

Однако, мы можем, если захотим, для увеличения уверенности повторно запустить анализ с большим количество рассматриваемых объектов. Например, запуск указанной выше команды check с количеством рассматриваемых объектов, равным 10, все еще не выдаст нам никаких контрпримеров, так что можно предположить, что данное свойство, скорее всего, корректно. Однако, имейте в виду, что при увеличении количества используемых объектов анализатору потребуется проверить большее количество экземпляров моделей, и поэтому ему, скорее всего, потребуется для завершения больше времени.

Браузер

Давайте теперь добавим браузеры в нашу модель:

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

Это наш первый пример сигнатуры динамическими полями. В языке Alloy нет внутренних понятий времени или поведения, что означает, что для них можно пользоваться различными идиомами. В этой модели мы пользуемся обычной идиомой, в которой вы вводите понятие времени Time и присоединяете его в качестве последней колонки для каждого изменяющегося во времени поля. Например, выражение b.cookies.t представляет собой набор куки, которые хранятся в браузере b в конкретный момент времени t. Аналогично, поле документов documents связывает набор документов с каждым браузером в конкретный момент времени. (Для получения более подробной информации о том, как мы моделируем динамическое поведение, смотрите Приложении: Повторное использование модулей в языке Alloy).

Документы создаются из ответа на запрос HTTP. Они также могут быть уничтожены в случае, если, например, пользователь закрывает вкладку или браузер, но мы не учитываем это в данной модели. Документ имеет адрес URL (тот, откуда был взят документ), некоторый контент (DOM) и домен:

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

Добавление столбца Time для последних двух полей говорит нам о том, что они могут изменяться с течением времени, а ее отсутствие в первом поле (src, представляющего собой адрес URL исходного документа) указывает на то, что источник адреса URL зафиксирован.

Для того, чтобы промоделировать эффект запроса HTTP на браузере, мы вводим новую сигнатуру поскольку не все запросы HTTP будут происходить на уровне браузера; остальное будут поступать из скриптов.

sig BrowserHttpRequest extends HttpRequest {
  doc: Document
}{
  -- запрос поступает из браузера
  from in Browser
  -- куки, которые посылаются, в момент запроса находятся в браузере
  sentCookies in from.cookies.start
  -- действие каждого посылаемого куки ограничено url запроса
  all c: sentCookies | url.host in c.domains

  -- создается новый документ для того, чтобы отобразить содержимое запроса
  documents.end = documents.start + from -> doc
  -- документ, у которого в качестве контента указан ответ
  content.end = content.start ++ doc -> response
  -- у нового документа указывается хост и url в качестве его домена
  domain.end = domain.start ++ doc -> url.host
  -- поле источника, откуда получен документ, является url-ом запроса
  doc.src = url

  -- новые куки заполнены браузером
  cookies.end = cookies.start + from -> sentCookies
}

Этот вид запроса имеет одно новое поле, doc, представляющее собой документ, созданный в браузере из ресурса, возвращаемого с помощью запроса. Как и в случае запроса HttpRequest, поведение описывается как совокупность ограничений. В некоторых из них говорится, когда может произойти вызов: например, что вызов должен прийти из браузера. Некоторые из них накладывают ограничения на аргументы вызова: например, что куки должны иметь соответствующую область видимости. А некоторые ограничения обладают сдерживающим эффектом, используя общую идиому, которая связывает значение отношения после вызова со значением до вызова.

Например, чтобы понять ограничение documents.end = documents.start + from -> doc, запомните, что документы есть отношение с тремя колонками — между браузерами, документами и временами. Поля start и end берутся из объявления вызова Call (которого мы не видели, но включен в конце листинг) и представляют значения времени в начале и в конце вызова. Выражение documents.end дает отображение из браузеров в документы после завершения вызова. Поэтому это ограничение говорит, что после вызова, отображение точно такое же за исключением лишь новой записи в таблице, отображающей из from в doc.

Некоторые ограничения используют оператор переопределения отношений ++: e1 ++ e2 содержит все кортежи из e2, и, кроме того, все кортежи из e1, первый элемент которого не является первым элементом кортежа из e2. Например, ограничение content.end = content.start ++ doc -> response говорит, что после вызова отображение content будет обновлено так, чтобы doc было отображено в response (переопределяя любые предыдущие отображения doc). Если бы мы вместо этого использовали бы оператор объединения +, то тот же самый документ в состоянии after (после) бы мог (неправильно) отображаться на несколько ресурсов.

Скрипт

Далее мы будем использовать модели HTTP и браузера для того, чтобы ввести скрипты клиентской стороны client-side scripts, которые представляют собой фрагменты кода (обычно на языке JavaScript), выполняемые внутри документа браузера (context).

sig Script extends Client { context: Document }

Скрипт представляет собой динамический объект, который может выполнять два различных вида действия: 1) он может делать запросы HTTP (т.е., запросы Ajax) и 2) он может выполнять операции в браузере с тем, чтобы преобразовывать содержание и свойства документа. Гибкость скриптов, работающих на стороне клиента, является одним из основных катализаторов быстрого развития Web 2.0, но также является причиной того, почему в первую очередь были определены кросс-доменные ограничения. Без кросс-доменных ограничений скрипты могли бы иметь возможность отправлять серверам произвольные запросы, либо произвольным образом изменять документы, находящиеся внутри браузера - было бы плохо, если бы один или несколько скриптов оказались вредоносными.

Скрипт может обмениваться данными с сервером при помощи отправки запроса 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  
}

Какие виды действий скрипт может выполнять с документами? Во-первых, мы вводим общее понятие операций браузера (browser operations) для того, чтобы представить набор функций 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 ссылается на документ, к которому можно получить доступ или который можно изменять с помощью этого вызовом. Второе ограничение в сигнатуре facts говорит, что как doc, так и документ, в котором выполняется скрипт (from.context) должны быть документами, которые в настоящее время существуют в браузере. Наконец, операция BrowserOp может изменить состояние документа, но не набора документов или куки, которые хранятся в браузере. (На самом деле, куки могут быть ассоциированы с документом и могут изменяться с помощью API браузера, но на данный момент мы опустим эту деталь).

Скрипт может читать в различные части документа (обычно называемые элементами DOM) и может в них записывать. В обычном браузере существует большое количество функций API для доступа к DOM (например, 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.

Кроме того, скрипт может изменять различные свойства документа, такие как его ширина, высота, домен и название. Для нашего обсуждения кросс-доменных ограничений нам интересны только свойство domain (домен), которое мы введем в следующем разделе.

Перейти к следующей части статьи.

Перейти к началу статьи.