pcc技术浅究.pptVIP

PCC技术浅究 PCC技术产生背景 目前软件开发工作中，程序员经常需要从网上得到相应的代码和库，对他们稍加修改得到自己想要的结果。因此，会面临代码破坏计算机的文件系统和泄露机密文件的问题。 如果代码编写者给出代码安全性证明，那么验证一个代码的证明的正确性的代价远远小于证明一个代码安全的代价。 为了解决以上问题，G.C.Necula 和 P.Lee 等人，将形式语义学，类型系统程序验证，逻辑框架理论有机结合形成一种基于程序设计语言的安全解决方案。提出了pcc（proof-carrying code）理论。 PCC基本概念 场景：存在代码提供者和代码执行者两方，前者的代码在后者处执行 目的：保护代码执行方不受代码提供方伤害 方法：欲执行代码的一方预先制定安全策略，代码提供者据此赋予代码一个安全证明以说明其符合安全规则。再把该证明送至代码执行者带的证明确认器，证明被确认是对的，则说明代码符合安全要求，方可将此代码交付执行。 PCC系统框架 证明阶段：代码提供者根据安全策略对源程序生成安全证明 确认阶段：代码执行者将证明送往证明确认器，验证证明是否正确 执行阶段：若证明正确，则将代码送往cpu执行 PCC实现条件 PCC系统的实现必须具有四个部分： 刻画安全策略的形式的规格说明语言 将程序关联到规格说明的逻辑系统 表达证明的语言（证明的格式） 确认证明的算法 PCC设计实例 ML语言软件开发中PCC应用实例： 用ML语言开发应用软件，调用非ML语言实现的函数的时候，通过PCC系统来确保系统的安全。 使用ML语言编程定义一个类型T，以及作用在T上的一个函数sum。Sum的功能是求T表所包含的所有整数的和。 通过使用汇编语实现SUM函数 ML定义程序 汇编程序（SUM） 系统框图 系统四个部分 （1）规格说明语言：扩展的一阶谓词演算逻辑。（包含与安全有关的公式和推导规则） （2）将程序关联到规格的逻辑系统：将一段代码转换成一个公式，完成由程序世界到逻辑世界的转换。采用Floyd验证条件生成器（VCG），将安全需求与程序同时输入，输出验证条件（VC） （3）证明的格式：采用爱丁堡逻辑框架（LF）对证明编码 （4）证明的确认：对证明的表达式做LF的类型检查 系统框图 系统步骤 代码提供者： （1）制定安全规则（代码执行者） （2）生成验证条件（VC）：将源程序与安全规则通过VCG，得到（VC） （3）生成证明：将VC通过定理证明器生成VC的推导D，对D进行编码得到[D] （4）得到PCC代码（P，[D]） 生成VC的形式 生成证明的形式 系统框图 系统步骤 代码执行者： （1）分离程序代码和安全证明 （2）从程序代码计算出（VC） （3）验证安全证明是否正确，及是否是（VC）的证明 （4）如果通过验证则开始执行代码 PCC优点及问题 问题及难点 安全规则的完备性很难达到 证明的生成：程序较大时，证明的结构将比较复杂和庞大 规约逻辑，公理化 优点 主机端工作简单，只需快速的确认 防篡改，代码变动后需要重新证明 先检查后执行，不会产生运行时的开销 检查一次通过可执行多次，有利于工程化设计