一种构造代码安全性证明的新方法
携带证明的代码(Proof-Carrying Code，PCC)最早由Necula提出，其定义是可执行代码携带上关于自身安全性的形式证明。代码消费方不需要信任PCC代码的生产方，即可执行代码与安全性证明不再属于整个系统安全性的信任计算基础(Trusted Computing Base，TCB)。随后Appel与Felty提出了基础性携带证明的代码(FoundationalProof-Carrying Code，FPCC)的概念。 FPCC的基本思想是将PCC代码与复杂的推理系统都形式化在一个底层的基础逻辑(Foundational Logic)中，于是推理系统的可靠性就可以用基础逻辑保证，复杂的推理系统可以被排除出TCB，其TCB仅包括安全策略、机器模型、基础逻辑以及基础逻辑的证明检查器。 随后的各种FPCC实现采用了不同的推理系统来构造代码的安全性证明。例如采用类型系统(如LTFAL，TALT)或者采用逻辑系统(如SCAP)，还有一些FPCC系统同时采用了类型与逻辑的混合系统作为推理系统(如OCAP,Open Verifier)。
类型理论 软件安全 携带证明代码 程序验证 类型化汇编语言
郭宇 陈意云 林春晓
中国科学技术大学计算机科学技术系,安徽合肥,230027 中科大苏州研究院软件安全实验室,江苏苏州,215123
国内会议
苏州
中文
542-544
2007-10-18（万方平台首次上网日期，不代表论文的发表时间）