Composability, Provability, Reusability (CPR) for Survivability

Abstract

The goal of this effort Composability, Provability, Reusability (CPR) for Survivability is to address the problem of composition of survivable systems. The particular objective of this project is to construct a formal specification of the Java Virtual Machine (JVM) bytecode loader and verifier, and from that specification formally derive a provably-correct implementation. The specification and program development is being carried out using Kestral's Specware System. The security of Java applications depend on type safety and related properties enforced by bytecode verification. Serious Java security flaws have been traced to errors in Sun's Java bytecode verifier and loader. A formal specification will serve as a reference document for the construction of new JVM implementations for just-in-time compilers, web browsers, smart cards, etc. The desired safety and security properties of the verifier will be proved as putative properties of the formal specification. The formally-derived implementation can be used as a test oracle to test implementations, or may be incorporated directly into a JVM implementation.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Apr 01, 2002
Accession Number
ADA402606

Entities

People

  • Allen Goldberg

Organizations

  • Kestrel Institute

Tags

DTIC Thesaurus Topics

  • Air Force Research Laboratories
  • Compilers
  • Computer Program Documentation
  • Computer Programming
  • Computer Programs
  • Computers
  • Information Operations
  • Language
  • Object Code
  • Programming Languages
  • Security
  • Specifications
  • Standards
  • Survivability
  • Verification
  • Virtual Machines
  • Web Browsers

Fields of Study

  • Computer science
  • Engineering

Readers

  • Computer Engineering
  • Database Systems and Applications
  • Software Engineering.