Certified Assembly Programming with Embedded Code Pointers
Last modified: Tue Dec 20 15:11:17 2005 GMT.
Authors
Zhaozhong NiZhong Shao
Abstract
Embedded code pointers (ECPs) are stored handles of functions and continuations commonly seen in low-level binaries as well as functional or higher-order programs. ECPs are known to be very hard to support well in Hoare-logic style verification systems. As a result, existing proof-carrying code (PCC) systems have to either sacrifice the expressiveness or the modularity of program specifications, or resort to construction of complex semantic models. In Reynolds's LICS'02 paper, supporting ECPs is listed as one of the main open problems for separation logic.In this paper we present a simple and general technique for solving the ECP problem for Hoare-logic-based PCC systems. By adding a small amount of syntax to the assertion language, we show how to combine semantic consequence relation with syntactic proof techniques. The result is a new powerful framework that can perform modular reasoning on ECPs while still retaining the expressiveness of Hoare logic. We show how to use our techniques to support polymorphism, closures, and other language extensions and how to solve the ECP problem for separation logic. Our system is fully mechanized. We give its complete soundness proof and a full verification of Reynolds's CPS-style ``list-append'' example in the Coq proof assistant.
Published
In Proc. 33rd ACM Symposium on Principles of Programming Languages (POPL'06), Charleston, SC, pages 320-333, January 2006. ©2006 ACM.- Gzipped Postscript [331k]
- PDF [328k]
- Coq implementaion [35k]
