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

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

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

Приложения - примеры

Как мы уже видели ранее анализатор языка Alloy при выполнении команд run или check генерирует сценарий (если он существует), который согласуется с описанием системы в модели. По умолчанию анализатор произвольным образом выбирает любой один из возможных сценариев работы с системой (до указанного ограничения) и в сценарии присваивает числовые идентификаторы экземплярам сигнатур (Server0, Browser1 и т.д.).

Иногда вместо того, чтобы исследовать сценарии со случайной конфигурацией серверов и клиентов, мы можем захотеть проанализировать поведение конкретного веб-приложения. Например, представьте, что мы хотим создать приложение электронной почты, который работает внутри браузера (например, Gmail). В дополнение к основным функциям электронной почты, наше приложение может отображать баннер рекламной службы третьей стороны, которая контролируется потенциально опасным актором.

В языке Alloy с помощью ключевых слов one sig вводится сигнатура-синглетон singleton, которая содержит в себе ровно один объект; мы видели выше такой пример для Dns. Этот синтаксис можно использовать для указания на конкретные атомы. Например, чтобы сказать, что есть одна страница InboxPage (Входящие) и один рекламный баннер (AdBanner), каждый из которых представляет собой документ, мы можем написать следующее:

one sig InboxPage, AdBanner extends Document {}

Благодаря этой декларации, каждый сценарий, который генерируется с помощью языка Alloy, будет содержать, по меньшей мере, эти два объекта документа.

Кроме того, мы можем указать отдельные серверы, домены и так далее, с ограничением (которые мы назвали конфигурацией 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
}

Например, последнее ограничение в fact, указывает, каким образом будет сконфигурирован DNS с тем, чтобы отображать имена доменов для двух серверов в нашей системе. Без этого ограничения, анализатор языка Alloy может генерировать сценарии, в которых домен EmailDomain отображается на сервер EvilServer, что тдля нас не интересно. На практике, такое отображение может оказаться возможным из-за атаки, которая называется DNS-спуфинг, но мы исключаем его из нашей модели, так как оно лежит за пределами класса атак, для предотвращения которых предназначены кросс-доменные ограничения.

Давайте введем два дополнительных приложения: онлайновый календарь и сайт-блог:

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. В нашей модели это можно добавить, если добавить доменное имя, которое является подсуммой subsumes других доменов:

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

Обратите внимание, что в подсумму subsumes в качестве члена входит this, поскольку каждое доменное имя в качестве подсуммы содержит самого себя.

Есть и другие частности, касающиеся этих приложений, которые мы здесь опускаем (полную модель смотрите в example.als). И мы будем возвращаться к этим приложениях, т. к. на протяжении оставшейся части данной главы эти приложения будут использоваться в качестве нашего рабочего примера.

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

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

---

---

---