CT-ISG: Certified Runtime Code Manipulation

0716540 CT-ISG：认证运行时代码管理PI：中绍耶鲁大学运行时代码操作(RCM)泛指在运行时故意加载、生成或更改代码的任何编程构造。今天的大量系统软件和虚拟机使用各种形式的RCM结构-其中许多经常是安全攻击的目标。不幸的是，现有的基于逻辑的形式化方法-包括程序验证和模型检查--都假定程序代码是不变的。该项目旨在解决这一主要限制，以便现有的验证技术也可以用于认证使用RCM功能的重要软件(例如，操作系统引导加载程序、虚拟机、JIT编译器、动态链接器和加载程序)。PI将采用和扩展最近在认证编程和携带验证代码方面的工作的想法，开发用于验证运行时代码生成、链接和突变的新方法，并展示如何将方法扩展到真实世界的系统应用程序。对验证通用RCM结构的成功研究将从当今许多关键任务系统的可信计算基础中移除关键(但容易出现错误)的软件。机器可检查的规范和证明将使理解和维护现有的RCM实现变得更容易，并使其适应复杂应用软件的特定需求。该协会还将为经过认证的RCM结构开发新的教学材料，并为普通公众提供辅导培训。

0716540 CT-ISG: Certified Runtime Code ManipulationPI: Zhong Shao Yale UniversityRuntime Code Manipulation (RCM) refers broadly to any programmingconstruct that purposely loads, generates, or mutates code atruntime. A large number of today's systems software and virtualmachines use various forms of the RCM constructs---many of which areoften targets for security attacks. Unfortunately, existinglogic-based formal methods---including both program verification andmodel checking---all assume that program code is immutable. Thisproject aims to fix this major limitation so that existingverification technologies can also be used to certify importantsoftware that use RCM functionalities (e.g., OS boot loader, virtualmachine, JIT compiler, dynamic linker and loader). The PI will adaptand extend ideas from recent work on certified programming andproof-carrying code, develop new methodologies for verifying runtimecode generation, linking, and mutation, and show how to scale ourapproach to real-world system applications. Successful research oncertifying general RCM constructs will remove a critical (yetbug-prone) piece of software from the trusted computing base in manyof today's mission-critical systems. The machine-checkablespecifications and proofs will make it easier to understand andmaintain existing RCM implementations and to adapt them to satisfyparticular needs of sophisticated application software. The PI willalso develop new instructional material for certified RCM constructsand provide tutorial training to the general public.