Accession Number:

ADA639289

Title:

Building Certified Libraries for PCC: Dynamic Storage Allocation

Descriptive Note:

Corporate Author:

YALE UNIV NEW HAVEN CT DEPT OF COMPUTER SCIENCE

Report Date:

2003-01-13

Pagination or Media Count:

23.0

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.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE