Building Certified Libraries for PCC: Dynamic Storage Allocation

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 06, 2003
Accession Number
ADA436475

Entities

People

  • Dachuan Yu
  • Nadeem A. Hamid
  • Zhong Shao

Organizations

  • Yale University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Assembly
  • Assembly Languages
  • Computer Programming
  • Computer Science
  • Computers
  • Construction
  • Guarantees
  • Instruction Set Architecture
  • Instructions
  • Language
  • Lists (Data Structures)
  • Reasoning
  • Sequences
  • Specifications
  • Splitting
  • Template Patterns

Fields of Study

  • Computer science
  • Engineering

Readers

  • Aviation Safety Risk Assessment.
  • Computational Linguistics
  • Parallel and Distributed Computing.