Код подтверждения - Proof-carrying code

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

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

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

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

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

Смотрите также

• Типизированный язык ассемблера
• Вывод программы
• Формальная проверка

Рекомендации

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

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