The FLINT Project

Research

People

Publications

Software

Support

Links

Internal

Modular Verification of Assembly Code with Stack-Based Control Abstractions

Last modified: Wed Nov 22 20:51:15 2006 GMT.

Authors

Xinyu Feng
Zhong Shao
Alexander Vaynberg
Sen Xiang
Zhaozhong Ni

Abstract

Runtime stacks are critical components of any modern software---they are used to implement powerful control structures such as function call/return, stack cutting and unwinding, coroutines, and thread context switch. Stack operations, however, are very hard to reason about: there are no known formal specifications for certifying C-style setjmp/longjmp, stack cutting and unwinding, or weak continuations (in C--). In many proof-carrying code (PCC) systems, return code pointers and exception handlers are treated as general first-class functions (as in continuation-passing style) even though both should have more limited scopes.

In this paper we show that stack-based control abstractions follow a much simpler pattern than general first-class code pointers. We present a simple but flexible Hoare-style framework for modular verification of assembly code with all kinds of stack-based control abstractions, including function call/return, tail call, setjmp/longjmp, weak continuation, stack cutting, stack unwinding, multi-return function call, coroutines, and thread context switch. Instead of presenting a specific logic for each control structure, we develop all reasoning systems as instances of a generic framework. This allows program modules and their proofs developed in different PCC systems to be linked together. Our system is fully mechanized. We give the complete soundness proof and a full verification of several examples in the Coq proof assistant.

Published

  • In Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06), Ottawa, Canada, pages 401-414, June 2006. ©2006 ACM.


  • Technical Report YALEU/DCS/TR-1336 (Extended Version) (24 pages)


  • Coq Implementaion [63k]
    • Encoding of the target machine (TM);
    • Encoding of the CAP framework and its soundness proof;
    • Proof of SCAP rules as lemmas;
    • Certified malloc/free library using SCAP.

  • Copyright © 1996-2017 The FLINT Group <flint at cs dot yale dot edu>
    Yale University Department of Computer Science
    Validate this page
    colophon