Библиотека сайта rus-linux.net
Кросс-доменные ограничения
Оригинал:The Same-Origin Policy
Авторы: Eunsuk Kang, Santiago Perez De Rosso, and Daniel Jackson,
Дата публикации: July 12, 2016
Перевод: Н.Ромоданов
Дата перевода: январь 2017 г.
Это седьмая часть статьи "Кросс-доменные ограничения".
Перейти к
началу статьи.
Приложение: Повторное использование модулей в языке Alloy
Как уже упоминалось ранее в этой главе, язык Alloy не делает никаких предположений о поведении системы, которая моделируются. Отсутствие встроенной парадигмы позволяет пользователю кодировать широкий спектр идиом моделирования с использованием небольшого ядра базовых конструкций языка. Мы могли бы, например, определить систему в виде конечного автомата, в виде модели данных с комплексными инвариантами, в виде распределенной модели событий в рамках глобального времени или в виде любой другой идиомы, которая будет наиболее подходящей для рассматриваемой проблемы. Обычно используемые идиомы можно реализовать в виде базового модуля и повторно использовать его в различных системах.
В нашей модели кросс-доменных ограничений мы моделируем систему в виде набора конечных точек, которые взаимодействуют друг с другом при помощи одного или нескольких вызовов. Так как вызов является довольно обобщенным понятием, мы инкапсулируем его описание в виде отдельного модуля языка Alloy, который будет импортирован из других модулей, которые ими пользуются - по аналогии со стандартными библиотеками в языках программирования:
module call[T]
В этом модуле декларация T представляет собой параметр-типа, который может быть инстанцирован для конкретного типа, который указывается, когда модуль импортируется. Скоро мы мы увидим, как используется этот параметр типа.
Часто бывает удобно описывать выполнение системы как нечто, происходящее в рамках глобального времени, так что мы можем говорить о вызовах, которые происходят до или после друг друга (или одновременно). Для того, чтобы представить понятие времени, мы вводим новую сигнатуру, которая называется Time:
open util/ordering[Time] as ord
sig Time {}
В языке Alloy util/ordering является встроенным модулем, с помощью которого задается общий порядок для параметра типа, и поэтому за счет импорта ordering[Time] мы получим множество объектов Time, которые ведут себя как и другие вполне упорядоченные множества (например, натуральные числа).
Обратите внимание, что нет абсолютно ничего особенного, касающегося времени Time; мы могли бы назвал его любым другим способом (например, шаг Step или состояние State), и это вообще не изменило бы поведение модели. Все, что мы здесь делаем, это в различные моменты исполнении системы пользуемся дополнительным столбцом — отношением как способом представления содержимого поля; например, cookies в сигнатуре Browser. В этом смысле объекты Time являются всего лишь вспомогательными объектами, используемыми в качестве индекса специального вида.
Каждый вызов происходит между двумя моментами времени - его началом start и окончанием end, и ассоциируется с отправителем (представленным с помощью from) и получателем (to):
abstract sig Call { start, end: Time, from, to: T }
Напомним, что в нашем обсуждении запросов HTTP мы импортировали модуль call при помощи передачи конечной точки Endpoint в качестве параметра типа. В результате параметрический тип Т инстанциируется в Endpoint и мы получаем набор объектов Call, которые ассоциированы с парой конечных точек отправителя и получателя. Модуль может быть импортирован несколько раз; например, мы могли бы объявить сигнатуру, которая назвается UnixProcess, и экземпляр модуля call с тем, чтобы получить определенный набор объектов Call, которые отправляются от одного процесса Unix к другому.
- 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.
- 2. Sebastian Lekies, Martin Johns, and Walter Tighzert. The State of the Cross-Domain Nation. Web 2.0 Security and Privacy (W2SP), 2011.
Перейти к началу статьи.