Accession Number:

ADA478745

Title:

Modular Machine Code Verification

Descriptive Note:

Doctoral thesis

Corporate Author:

YALE UNIV NEW HAVEN CT DEPT OF COMPUTER SCIENCE

Personal Author(s):

Report Date:

2007-05-01

Pagination or Media Count:

183.0

Abstract:

Formally establishing safety properties of software presents a grand challenge to the computer science community. Producing proof-carrying code, i.e., machine code with machine-checkable specifications and proofs, is particularly difficult for system softwares written in low-level languages. One central problem is the lack of verification theories that can handle the expressive power of low-level code in a modular fashion. In particular, traditional type- and logic-based verification approaches have restrictions on either expressive power or modularity. This dissertation presents XCAP, a logic-based proof-carrying code framework for modular machine code verification. In XCAP, program specifications are written as general logic predicates, in which syntactic constructs are used to modularly specify some crucial higher-order programming concepts for system code, including embedded code pointers, impredicative polymorphisms, recursive invariants, and general references, all in a logical setting. Thus, XCAP achieves the expressive power of logic-based approaches and the modularity of type-based approaches. Its meta theory has been completely mechanized and proved. XCAP can be used to directly certify system kernel code. This dissertation contains a mini certified thread library written in x86 assembly. Every single instruction in the library, including those for context switching and thread scheduling, has a formal XCAP specification and a proof. XCAP is also connected to existing certifying compiler a typepreserving translation from a typed assembly language to XCAP is included.

Subject Categories:

  • Computer Programming and Software
  • Structural Engineering and Building Technology

Distribution Statement:

APPROVED FOR PUBLIC RELEASE