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