[Kestrel circling]

Home : Project Archive : CPR : Objective
 

Home

About Kestrel

Research Staff

Current Projects

Project Archive

Publications

Technology Transfer

Career Opportunities

Contact Kestrel

Objective

The 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 Kestrel'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.

 

 

 

 

 

 

 

 

 

- Back to Top -


- Home - About Kestrel - Research Staff - Current Projects - Project Archive -
- Publications - Technology Transfer - Career Opportunities - Contact Kestrel -