Building Certified Libraries for PCC: Dynamic Storage Allocation

Last modified: Wed May 7 14:42:29 2003 GMT.

Authors

Dachuan Yu
Nadeem Abdul Hamid
Zhong Shao

Abstract

Proof-Carrying Code (PCC) allows a code producer to provide to a host a program along with its formal safety proof. The proof attests a certain safety policy enforced by the code, and can be mechanically checked by the host. While this language-based approach to code certification is very general in principle, existing PCC systems have only focused on programs whose safety proofs can be automatically generated. As a result, many low-level system libraries (e.g., memory management) have not yet been handled. In this paper, we explore a complementary approach in which general properties and program correctness are semi-automatically certified. In particular, we introduce a low-level language CAP for building certified programs and present a certified library for dynamic storage allocation.

Published

In Proc. 2003 European Symposium on Programming (ESOP'03), Warsaw, Poland, April 2003. Lecture Notes in Computer Science Vol. 2618. © Springer-Verlag.

Technical Report YALEU/DCS/TR-1247, Dept. of Computer Science, Yale University, New Haven, CT, January 2003.

Gzipped Postscript [131k]
PDF [341k]
Implementation in Coq (v7.3.1) (tar.gz) [48k]

colophon