Safe kernel extensions without run-time checking
Safe kernel extensions without run-time checking
复制标题
DOI：
10.1145/238721.238781
复制
发表时间：
1996-10
期刊：
影响因子：
--
通讯作者：
G. Necula;Peter Lee
中科院分区：
文献类型：
--
作者：
G. Necula;Peter Lee
摘要：本文描述了一种操作系统内核能够确定无疑地判断执行由不可信来源提供的二进制文件是安全的机制。内核首先定义一个安全策略并将其公开。然后，应用程序可以利用该策略以一种称为携带证明代码（简称为PCC）的特殊形式提供二进制文件。除了原生代码外，每个PCC二进制文件还包含一个该代码遵循安全策略的形式化证明。内核无需使用密码学，也无需咨询任何外部可信实体就能轻松验证该证明。如果验证成功，就能保证代码遵守安全策略，而无需依赖运行时检查。PCC的主要实际困难在于生成安全证明。为了获得一些这方面的初步经验，我们用手工优化的DEC Alpha汇编语言编写了几个网络数据包过滤器，然后使用一个特殊的原型汇编器为它们生成PCC二进制文件。除了验证所包含证明的一次性1到3毫秒成本外，PCC二进制文件的执行没有运行时开销。最终结果是，我们的数据包过滤器在形式上被保证是安全的，并且比使用伯克利数据包过滤器、软件故障隔离或诸如Modula - 3等安全语言创建的数据包过滤器更快。
Abstract : This paper describes a mechanism by which an operating system kernel can determine with certainty that it is safe to execute a binary supplied by an untrusted source. The kernel first defines a safety policy and makes it public. Then, using this policy, an application can provide binaries in a special form called proof-carrying code, or simply PCC. Each PCC binary contains, in addition to the native code, a formal proof that the code obeys the safety policy. The kernel can easily validate the proof without using cryptography and without consulting any external trusted entities. If the validation succeeds, the code is guaranteed to respect the safety policy without relying on run-time checks. The main practical difficulty of PCC is in generating the safety proofs. In order to gain some preliminary experience with this, we have written several network packet filters in hand-tuned DEC Alpha assembly language, and then generated PCC binaries for them using a special prototype assembler. The PCC binaries can be executed with no run-time over-head, beyond a one-time cost of 1 to 3 milliseconds for validating the enclosed proofs. The net result is that our packet filters are formally guaranteed to be safe and are faster than packet filters created using Berkeley Packet Filters, Software Fault Isolation, or safe languages such as Modula-3.