Код подтверждения подлинности
Код с доказательством ( PCC ) — это программный механизм, который позволяет хост-системе проверять свойства приложения с помощью формального доказательства , которое сопровождает исполняемый код приложения. Хост-система может быстро проверить действительность доказательства и сравнить выводы доказательства со своей собственной политикой безопасности, чтобы определить, безопасно ли выполнять приложение. Это может быть особенно полезно для обеспечения безопасности памяти (т. е. предотвращения таких проблем, как переполнение буфера ).
Код с доказательством был первоначально описан в 1996 году Джорджем Некулой и Питером Ли .
Пример фильтра пакетов
В оригинальной публикации о коде с доказательством в 1996 году [1] в качестве примера использовались пакетные фильтры : приложение пользовательского режима передает функцию, написанную в машинном коде, ядру, которое определяет, заинтересовано ли приложение в обработке определенного сетевого пакета. Поскольку пакетный фильтр работает в режиме ядра , он может нарушить целостность системы, если содержит вредоносный код, который записывает в структуры данных ядра. Традиционные подходы к этой проблеме включают интерпретацию доменно-специфического языка для фильтрации пакетов, вставку проверок при каждом доступе к памяти ( изоляция сбоев программного обеспечения ) и написание фильтра на языке высокого уровня, который компилируется ядром перед его запуском. Эти подходы имеют недостатки производительности для кода, который запускается так часто, как пакетный фильтр, за исключением подхода компиляции в ядре, который компилирует код только при его загрузке, а не каждый раз при его выполнении.
С помощью кода доказательства ядро публикует политику безопасности, определяющую свойства, которым должен подчиняться любой пакетный фильтр: например, пакетный фильтр не будет получать доступ к памяти за пределами пакета и его области временной памяти. Для демонстрации того, что машинный код удовлетворяет этой политике, используется доказатель теорем . Шаги этого доказательства записываются и прикрепляются к машинному коду, который передается загрузчику программы ядра. Затем загрузчик программы может быстро проверить доказательство, что позволяет ему впоследствии запустить машинный код без дополнительных проверок. Если злоумышленник изменяет либо машинный код, либо доказательство, полученный код доказательства либо недействителен, либо безвреден (все еще удовлетворяет политике безопасности).
Смотрите также
Ссылки
- ^ Necula, GC и Lee, P. 1996. Безопасные расширения ядра без проверки во время выполнения. Обзор операционных систем SIGOPS 30, SI (октябрь 1996 г.), 229–243.
- Джордж К. Некула и Питер Ли. Proof-Carrying Code. Технический отчет CMU-CS-96-165, ноябрь 1996 г. (62 страницы)
- Джордж К. Некула и Питер Ли. Безопасные, ненадежные агенты, использующие код подтверждения. Мобильные агенты и безопасность, Джованни Винья (ред.), Конспект лекций по информатике, том 1419, Springer-Verlag, Берлин, ISBN 3-540-64792-9 , 1998.
- Джордж К. Некула. Компиляция с доказательствами . Кандидатская диссертация, Факультет компьютерных наук, Университет Карнеги-Меллона, сентябрь 1998 г.
