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 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 talk 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  evelop 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.

-------------------------------

Zhong Shao is a Professor and Director of Undergraduate Studies in the Department of Computer Science at Yale University.  His research interests include proof-carrying code, language-based security, programming languages and compilers, and operating systems.  He is a key developer of the Standard ML of New Jersey (SML/NJ) system and the architect of the FLINT certifying compiler infrastructure (now used by SML/NJ). He currently leads the Yale FLINT group to develop a certifed computing platform that can offer true guarantees of software reliability and security. Zhong graduated from University of Science and Technology of China in 1988 and received his Ph.D. in Computer Science from Princeton University in 1994.