CT-ISG: Certified Runtime Code Manipulation

点击翻译按钮获取中文摘要

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.