Building Certified Libraries for PCC: Dynamic Storage Allocation (Extended Version)
Last modified: Tue Mar 30 18:46:43 2004 GMT.
Authors
Dachuan YuNadeem 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 to 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 Science of Computer Programming (Special Issue ESOP 2003), Volume 50, Issues 1-3, Pages 101-127, March 2004. Published online via ScienceDirect. © 2004 Elsevier.
- PDF [719k]
- BibTex entry
- Implementation in Coq (v7.3.1) (tar.gz) [48k]
