Certified self-modifying code
| Autor: | Zhong Shao, Hongxu Cai, Alexander Vaynberg |
|---|---|
| Rok vydání: | 2007 |
| Předmět: |
Source code
Dead code Computer science Program animation media_common.quotation_subject Binary translation Static program analysis Program code computer.software_genre Dead code elimination Obfuscation Code generation Software system Redundant code Formal verification computer.programming_language media_common Assembly language Programming language Program transformation Code Access Security Program optimization Code bloat Formal methods Self-modifying code Object code Binary code KPI-driven code analysis Unreachable code Machine code computer |
| Zdroj: | PLDI |
| DOI: | 10.1145/1250734.1250743 |
| Popis: | Self-modifying code (SMC), in this paper, broadly refers to anyprogram that loads, generates, or mutates code at runtime. It is widely used in many of the world's critical software systems tosupport runtime code generation and optimization, dynamic loading and linking, OS boot loader, just-in-time compilation, binary translation,or dynamic code encryption and obfuscation. Unfortunately, SMC is alsoextremely difficult to reason about: existing formal verification techniques-including Hoare logic and type system-consistentlyassume that program code stored in memory is fixedand immutable; this severely limits their applicability and power.This paper presents a simple but novel Hoare-logic-like framework that supports modular verification of general von-Neumann machine code with runtime code manipulation. By dropping the assumption that code memory is fixed and immutable, we are forced to apply local reasoningand separation logic at the very beginning, and treat program code uniformly as regular data structure. We address the interaction between separation and code memory and show how to establish the frame rules for local reasoning even in the presence of SMC. Our frameworkis realistic, but designed to be highly generic, so that it can support assembly code under all modern CPUs (including both x86 andMIPS). Our system is expressive and fully mechanized. We prove itssoundness in the Coq proof assistant and demonstrate its power by certifying a series of realistic examples and applications-all of which can directly run on the SPIM simulator or any stock x86 hardware. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|