Algorithm-Independent Framework for Verifying Integer Constraints

Abstract

Proof-carrying code (PCC), as pioneered by Necula and Lee, allows a code producer to provide a compiled program to a host, along with a formal proof of safety. The PCCbased systems often rely on solving integer constraints to prove the soundness of the index types and to control resource consumption. Unfortunately, existing approaches often require the inclusion of an oracle-like constraints solver into the trusted computing base (TCB) or at least lock the safety policy with one particular solver. This paper presents a feasibility study for dissociating the constraints solver from the TCB and the safety policy from the actual solver algorithm. To demonstrate this, we produce a simple framework, we show how to adapt the popular solvers such as the Omega test and the Simplex method into this framework and we study some of its properties.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jul 20, 2000
Accession Number
ADA436487

Entities

People

  • David Teller
  • Zhong Shao

Organizations

  • Yale University

Tags

Communities of Interest

  • Energy and Power Technologies
  • Ground and Sea Platforms
  • Human Systems

DTIC Thesaurus Topics

  • Algorithms
  • Coefficients
  • Compilers
  • Computer Programming
  • Computer Programs
  • Computers
  • Elimination
  • Equations
  • Feasibility Studies
  • Grammars
  • Inequalities
  • Language
  • Optimization
  • Polynomials
  • Programming Languages
  • Security
  • Simplex Method

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Cybersecurity.
  • Operations Research