Moat

Приложения с критическими требованиями к безопасности постоянно сталкиваются с угрозами эксплуатации уязвимостей в нижних уровнях вычислительной платформы, таких как операционная система, гипервизоры виртуальных машин или даже атаки со стороны злоумышленных администраторов. Для защиты секретов приложений от таких атак растёт интерес к аппаратным реализациям примитивов доверенных вычислений, например к инструкциям Intel Software Guard Extensions (SGX). Эти примитивы обеспечивают аппаратную защиту областей памяти, содержащих код и данные, и служат корнем доверия для измерений, удалённой аттестации и криптографического запечатывания. Однако уязвимости в самом приложении, такие как некорректное использование инструкций SGX или ошибки безопасности памяти, могут быть использованы для раскрытия секретов. В этой работе мы представляем новый подход к формальному моделированию этих примитивов и формальной верификации свойств так называемых программ-энклавов, использующих их. Конкретно, мы создаём формальные модели релевантных аспектов SGX, разрабатываем несколько моделей противника и предлагаем корректную методологию верификации (на основе автоматического доказательства теорем и анализа информационных потоков) для доказательства того, что программа-энклав, выполняемая на SGX, не содержит уязвимости, приводящей к раскрытию секретов противнику. Мы представляем Moat — инструмент, который формально верифицирует свойства конфиденциальности приложений, выполняющихся на SGX. Мы оцениваем Moat на нескольких приложениях, включая схему одноразовых паролей, систему приватных (off-the-record) сообщений, нотариальную службу и безопасную обработку запросов.