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