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.