Runtime Code Manipulation (RCM) refers broadly to any programming construct that purposely loads, generates, or mutates code at runtime. A large number of today's systems software and virtual machines use various forms of the RCM constructs---many of which are often targets for security attacks. Unfortunately, existing logic-based formal methods---including both program verification and model checking---all assume that program code is immutable. This project aims to fix this major limitation so that existing verification technologies can also be used to certify important software that use RCM functionalities (e.g., OS boot loader, virtual machine, JIT compiler, dynamic linker and loader). The PI will adapt and extend ideas from recent work on certified programming and proof-carrying code, develop new methodologies for verifying runtime code generation, linking, and mutation, and show how to scale our approach to real-world system applications. Successful research on certifying general RCM constructs will remove a critical (yet bug-prone) piece of software from the trusted computing base in many of today's mission-critical systems. The machine-checkable specifications and proofs will make it easier to understand and maintain existing RCM implementations and to adapt them to satisfy particular needs of sophisticated application software. The PI will also develop new instructional material for certified RCM constructs and provide tutorial training to the general public.
