A Simple Model for Certifying Assembly Programs with First-Class Function Pointers

Last modified: Mon Oct 31 19:47:03 2011 GMT.

Authors

Abstract

First-class function pointers are common in low-level assembly languages. Higher-level features such as closures, virtual functions, and call-backs are all compiled down to assembly code with function pointers. Function pointers are, however, hard to reason about. Previous program logics for certifying assembly programs either do not support first-class function pointers, or follow Continuation-Passing-Style reasoning which does not provide the same partial correctness guarantee as in high-level languages. In this paper, we present a simple semantic model for certifying the partial correctness property of assembly programs with first-class function pointers. Our model does not require any complex domain-theoretical construction, instead, it is based on a novel step-indexed, direct-style operational semantics for our assembly language. From the model, we derive a new program logic named ISCAP (or Indexed SCAP). We use an example to demonstrate the power and simplicity of ISCAP. The semantic model, the ISCAP logic, and the soundness proofs have been implemented in the Coq proof assistant.

Published

In Proc. 5th International Conference on Theoretical Aspects of Software Engineering, Xi'an, China, August 2011, pages 125-132. © 2011 IEEE. [PDF]

Soundness proof in Coq [iscap-soundness.tar]

colophon