Автоматическая верификация
Метод автоматической верификации основан на представлении кода в определенном формате, называемом PCC (Proof-Carrying Code) [Nec97]. PCC-модуль содержит формальное доказательство соответствия кода данной политике безопасности. Истинность доказательства гарантирует безопасность кода, и программный модуль может выполняться без проверок во время выполнения. Политика безопасности ядра описывается с помощью аксиом и правил вывода в доказательствах, а также формулируется в виде предикатов логики первого порядка для каждой инструкции, в которых указывается, при каких обстоятельствах выполнение каждой инструкции будет оставаться безопасным. Приложение использует предикаты политики безопасности для вычисления предиката безопасности. Затем доказывается безопасность этого предиката по правилам логики первого порядка с использованием аксиом и правил вывода политики безопасности. Доказательство присоединяется к расширению. Ядро, в свою очередь, также вычисляет предикат безопасности и проверяет истинность ассоциированного доказательства для этого предиката. Проверка достоверности может быть сделана через простую и эффективную проверку типов (type checking).
Несмотря на привлекательность этого подхода, применимость его пока остается проблемой. Большие трудности возникают при попытках автоматизировать генерацию доказательств и использовать доказательства для языков высокого уровня.
