Код подтверждения

Код подтверждения ( PCC ) — это программный механизм, который позволяет хост-системе проверять свойства приложения посредством формального доказательства , которое сопровождает исполняемый код приложения. Хост-система может быстро проверить достоверность доказательства и сравнить выводы доказательства со своей собственной политикой безопасности , чтобы определить, безопасно ли выполнение приложения. Это может быть особенно полезно для обеспечения безопасности памяти (т.е. предотвращения таких проблем, как переполнение буфера ).

Код, несущий доказательства, был первоначально описан в 1996 году Джорджем Некулой и Питером Ли .

Пример фильтра пакетов

Оригинальная публикация о коде доказательства в 1996 г. ^[1] в качестве примера использовались фильтры пакетов : приложение пользовательского режима передает ядру функцию, написанную в машинном коде, которая определяет, заинтересовано ли приложение в обработке определенного сетевого пакета. Поскольку фильтр пакетов работает в режиме ядра , он может поставить под угрозу целостность системы, если содержит вредоносный код, записывающий в структуры данных ядра. Традиционные подходы к этой проблеме включают интерпретацию предметно-ориентированного языка для фильтрации пакетов, вставку проверок при каждом доступе к памяти ( программная изоляция ошибок ) и написание фильтра на языке высокого уровня, который компилируется ядром перед его запуском. Эти подходы имеют недостатки в производительности для кода, который так часто выполняется, как фильтр пакетов, за исключением подхода компиляции в ядре, который компилирует код только при его загрузке, а не при каждом его выполнении.

С помощью проверочного кода ядро публикует политику безопасности, определяющую свойства, которым должен подчиняться любой пакетный фильтр: например, пакетный фильтр не будет получать доступ к памяти за пределами пакета и его области рабочей памяти. Средство доказательства теорем используется, чтобы показать, что машинный код удовлетворяет этой политике. Шаги этого доказательства записываются и прикрепляются к машинному коду, который передается загрузчику программ ядра. Затем загрузчик программы может быстро проверить доказательство, что позволяет после этого запустить машинный код без каких-либо дополнительных проверок. Если злоумышленник изменяет машинный код или доказательство, полученный код доказательства либо недействителен, либо безвреден (по-прежнему удовлетворяет политике безопасности).

См. также

Ссылки

^ Некула, Г.К. и Ли, П. 1996. Безопасные расширения ядра без проверки во время выполнения. Обзор операционных систем SIGOPS 30, SI (октябрь 1996 г.), 229–243.

Джордж К. Некула и Питер Ли. Кодекс подтверждения . Технический отчет CMU-CS-96-165, ноябрь 1996 г. (62 страницы).
Джордж К. Некула и Питер Ли. Безопасные, ненадежные агенты, использующие подтверждающий код . Мобильные агенты и безопасность, Джованни Винья (ред.), Конспекты лекций по информатике, Vol. 1419, Шпрингер-Ферлаг, Берлин, ISBN 3-540-64792-9 , 1998.
Джордж К. Некула. Компиляция с доказательствами . Докторская диссертация, Школа компьютерных наук, Университет Карнеги-Меллона, сентябрь 1998 г.

[1] Некула, Г.К. и Ли, П. 1996. Безопасные расширения ядра без проверки во время выполнения. Обзор операционных систем SIGOPS 30, SI (октябрь 1996 г.), 229–243.

[1]