Composability, Provability, Reusability (CPR) for Survivability
Final rept. Oct 1996-Dec 1999
KESTREL INST PALO ALTO CA
Pagination or Media Count:
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 Kestrals 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 Suns 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.
- Computer Programming and Software