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