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

Код подтверждения ( 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]