Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Введение
Код, несущий доказательства (PCC), — это программный механизм, позволяющий хост-системе проверять свойства приложения посредством формального доказательства, сопровождающего исполняемый код этого приложения. Хост-система может быстро проверить корректность доказательства и сравнить его выводы со своей политикой безопасности, чтобы определить, безопасно ли запускать приложение. Это особенно полезно для обеспечения безопасности памяти, то есть предотвращения таких проблем, как переполнение буфера. Код, несущий доказательства, был впервые описан в 1996 году Джорджем Некулой и Питером Ли.
Proof carrying code (PCC) is a software mechanism that allows a host system to verify properties about an application via a formal proof that accompanies the application's executable code. The host system can quickly verify the validity of the proof, and it can compare the conclusions of the proof to its own security policy to determine whether the application is safe to execute. This can be particularly useful in ensuring memory safety (i. e. preventing issues like buffer overflows). Proof carrying code was originally described in 1996 by George Necula and Peter Lee.
Пример фильтра пакетов
В первоначальной публикации о коде с доказательством в 1996 году в качестве примера использовались пакетные фильтры: приложение, работающее в пользовательском режиме, передает ядру функцию, написанную на машинном коде, которая определяет, заинтересовано ли приложение в обработке конкретного сетевого пакета. Поскольку пакетный фильтр выполняется в режиме ядра, он может скомпрометировать целостность системы, если содержит вредоносный код, записывающий данные в структуры ядра. Традиционные подходы к решению этой проблемы включают интерпретацию доменно-специфичного языка для фильтрации пакетов, вставку проверок при каждом обращении к памяти (аппаратная изоляция ошибок) и написание фильтра на языке высокого уровня, который ядро компилирует перед запуском. Эти подходы имеют недостатки в производительности для кода, выполняемого так часто, как пакетный фильтр, за исключением подхода компиляции в ядре, который компилирует код только при загрузке, а не при каждом его выполнении. При использовании кода с доказательством ядро публикует политику безопасности, определяющую свойства, которым должен соответствовать любой пакетный фильтр: например, фильтр не должен обращаться к памяти за пределами пакета и его временной области памяти. Для доказательства того, что машинный код соответствует этой политике, используется решатель теорем. Шаги этого доказательства записываются и присоединяются к машинному коду, который передается загрузчику программ ядра. Загрузчик программ может быстро проверить доказательство, что позволяет ему впоследствии запускать машинный код без дополнительных проверок. Если злоумышленник изменит либо машинный код, либо доказательство, полученный код с доказательством будет либо недействителен, либо безвреден (все равно будет соответствовать политике безопасности).
The original publication on proof carrying code in 1996 used packet filters as an example: a user mode application hands a function written in machine code to the kernel that determines whether or not an application is interested in processing a particular network packet. Because the packet filter runs in kernel mode, it could compromise the integrity of the system if it contains malicious code that writes to kernel data structures. Traditional approaches to this problem include interpreting a domain specific language for packet filtering, inserting checks on each memory access (software fault isolation), and writing the filter in a high level language which is compiled by the kernel before it is run. These approaches have performance disadvantages for code as frequently run as a packet filter, except for the in kernel compilation approach, which only compiles the code when it is loaded, not every time it is executed. With proof carrying code, the kernel publishes a security policy specifying properties that any packet filter must obey: for example, the packet filter will not access memory outside of the packet and its scratch memory area. A theorem prover is used to show that the machine code satisfies this policy. The steps of this proof are recorded and attached to the machine code which is given to the kernel program loader. The program loader can then rapidly validate the proof, allowing it to thereafter run the machine code without any additional checks. If a malicious party modifies either the machine code or the proof, the resulting proof carrying code is either invalid or harmless (still satisfies the security policy).