Эксперты представили новый фреймворк для анализа безопасности браузера

Специалисты Венского технического университета разработали фреймворк для анализа безопасности браузера под названием WebSpec. С его помощью они обнаружили множество логических ошибок в браузерах, представили новую атаку на базе cookie-файлов и выявили противоречия в политике безопасности контента (Content Security Policy).

Логические ошибки – это не всегда уязвимости, хотя могут и быть таковыми. Они представляют собой несоответствия между спецификациями web-платформы и тем, как эти спецификации на самом деле реализуются в браузерах.

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

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

WebSpec использует язык доказательства теорем Coq для тестирования взаимодействия браузеров и их заданного поведения. Это дает возможность тестировать безопасность браузера с помощью задачи выполнимости формул в теориях (SMT).

WebSpec позволил исследователям обнаружить новую атаку на префикс __Host- cookie-файлов, а также выявить противоречия между правилами наследования Content Security Policy и запланированными изменениями в стандарте HTML.

HTTP cookie-файлы с префиксом __Host- должны настраиваться только доменом хоста или скриптами, включенными в страницы этого домена. Однако с помощью WebSpec специалисты выявили атаку, позволяющую исказить связанный инвариантный тест.

«Запущенный на странице скрипт может модифицировать время запуска эффективного домена, использующегося для проверок SOP (правило ограничения домена – ред.), через document.domain API», – пояснили специалисты.

По словам экспертов, из-за несоответствия между политиками контроля доступа Document Object Model и файла cookie jar запущенный в iframe скрипт может получать доступ к свойству document.cookie на родительской странице, если обе страницы устанавливают для document.domain одно и то же значение.

Однако, как отмечают исследователи, хотя текущая web-платформа уязвима к этой атаке, в конечном итоге она перестанет быть таковой, поскольку свойство document.domain устарело, а значит, будущие обновления браузера когда-нибудь не будут его поддерживать.

С помощью WebSpec исследователи также обнаружили несоответствие в том, как объекты Blob наследуют свои политики безопасности контента.

В любом случае доступность WebSpec в качестве инструмента для формальной оценки поведения браузера должна немного облегчить жизнь тем, кто изо всех сил старается поддерживать разросшуюся кодовую базу браузера.

Задача выполнимости формул в теориях – задача разрешимости для логических формул с учетом лежащих в их основе теорий. Примерами таких теорий для SMT-формул являются: теории целых и вещественных чисел, теории списков, массивов, битовых векторов и т. п.

Document Object Model – независящий от платформы и языка программный интерфейс, позволяющий программам и скриптам получить доступ к содержимому HTML-, XHTML- и XML-документов, а также изменять содержимое, структуру и оформление таких документов.