[Kestrel circling]

Home : Current Projects : High-Assurance Java Platform
 

Home

About Kestrel

Research Staff

Current Projects

Project Archive

Publications

Technology Transfer

Career Opportunities

Contact Kestrel

High-Assurance Java Platform

Contributors

Current

Past

  • Scott Burson
  • Eric Bush
  • Allen Goldberg
  • Zhenyu Qian

Background

The Java platform consists of the Java programming language, the Java Virtual Machine (JVM), the Java APIs, the Java compiler, and other tools. Java is increasingly used in smart cards, cell phones, PCs, and other computing devices.

Motivation

Java is designed to provide a secure platform where applications can be safely deployed. In order to achieve this goal, the various components (VM, compiler, etc.) must be designed and implemented correctly.

Objectives

Our ultimate goal is to synthesize a high-assurance implementation of the Java platform using Kestrel's Specware system. This is achieved by (1) developing a mathematical specification of the Java platform and (2) refining it to executable code that is provably correct with respect to the specification. In the process of developing the mathematical specification, desired properties can be formally established to hold, or flaws can be uncovered and fixed. This approach achieves high-assurance by addressing correctness of both design and implementation.

Our initial focus has been on bytecode verification and class loading, the components of the JVM that enforce type safety. Type safety is the basis of Java security.

Our current focus is on Java Card, a version of the Java platform that is tailored to smart cards. Our goal is to synthesize a high-assurance implementation of the Java Card Runtime Environment (JCRE), which includes the Java Card VM and the Java Card APIs.

Results

We have developed a complete formalization of bytecode verification and proved type safety properties of it. Our formalization includes several improvements to Sun's specification and implementation of the bytecode verifier. A paper containing this formalization will appear shortly. See [1,2,3] for preliminary, partial formalizations; note that our final formalization differs from them in some respects.

We have written this formalization in Specware and we have refined it to a running implementation, which has been successfully tested on several thousands of Java classes. See [4] for a description of a preliminary version of our bytecode verifier; note that the current version differs from it in some respects.

We have devised a novel technique to verify bytecode with subroutines. Subroutines constitute the most complex aspect of bytecode verification. Existing bytecode verifiers reject certain programs with subroutines generated by mundane compilers. Our technique is very simple yet powerful, and it accepts all code produced by compilers. See [11,12].

We have also studied in detail Sun's treatment of subroutines, and found formal evidence that it guarantees type safety. A paper on this will appear shortly.

We have studied the subtleties of checking access to protected members in the JVM. See [13,14].

We have found some subtle bugs in the bytecode verifier of Java 2 SDK (versions 1.2, 1.3, and 1.4) that lead to type safety violations. See [7,8,14].

We have analyzed in detail Sun's specification of bytecode verification and exposed all its inadequacies and ambiguities. We have also proposed concrete improvements to eliminate all these problems. See [9,10].

We have formalized the class loading mechanisms of the JVM, including multiple class loaders, interaction with bytecode verification, and invocation of user code that realizes customized loading policies. We have proved type safety results of this formalization. See [5,6].

We have developed a formal specification, in Specware, of the complete Java Card VM, of a large subset of the Java Card APIs, of non-standard extensions of the Java Card cryptographic APIs (e.g. MQV key agreement), of most of the JCRE top-level control (i.e. command processing, applet installation, etc.), of a large subset of GlobalPlatform features, and of a non-standard extension of the GlobalPlatform secure channel protocol suite. The Java Card and GlobalPlatform standards allow optional support for certain features; our formal specification supports a selection of features that results in a self-contained JCRE that can run a very large class of applets, but we plan to extend our formal specification to cover all the possible Java Card and GlobalPlatform features eventually. Papers on our formal specification of the JCRE will appear shortly.

We have refined our JCRE formal specification, using Specware, to an executable JCRE simulator. We have also developed an on-card prototype implementation, in C, of the JCRE from our formal specification; we plan to generate a second version of this on-card implementation via refinement of the JCRE formal specification, using Specware. Papers on this simulator and on-card implementation will appear shortly.

We are investigating the extension of the JCRE with runtime monitors to enforce information flow policies. We have used Specware to formalize and refine to code a monitor to enforce a separation policy, expressed as a form of non-interference, among security domains in an idealized subset of the JCRE; we have formally proved that the monitor enforces the policy. These results can be extended to the full JCRE. We are currently studying the enforcement, in a multi-threaded extension of the JCRE, of a separation policy that takes timing (covert) channels into account. Papers on these JCRE information flow policy monitors will appear shortly.

We have developed a preliminary formal specification, in Specware, of the memory model of the Real Time Specification for Java. Papers on this work will appear shortly.

A Related Project

While the project described in this page aims at high assurance for the Java platform, and in particular of the JCRE, the project described in this other page aims at high assurance for the Java Card applets that run on top of the JCRE. Together, the two projects aim at high assurance for the whole smart card software.

Publications

  1. A Specification of Java Loading and Bytecode Verification
    Allen Goldberg
    5th ACM Conference on Computer and Communications Security (CCS'98), pages 49-58
    October 1998
    [PS] [PDF] [BibTeX]
    {A specification of some salient aspects of bytecode verification and class loading, in a data flow analysis framework. This work is the basis of the preliminary version of our bytecode verifier in Specware described in [4].}

  2. A Formal Specification of Java Virtual Machine Instructions for Objects, Methods and Subroutines
    Zhenyu Qian
    Formal Syntax and Semantics of Java, volume 1523 of Lecture Notes in Computer Science, pages 271-312
    1999
    [PS] [PDF] [BibTeX]
    {A specification of several bytecode instructions, comprehensive of operational semantics and bytecode verification. Concepts from this work have been used in the development of our bytecode verifier in Specware.}

  3. Standard Fixpoint Iteration for Java Bytecode Verification
    Zhenyu Qian
    ACM Transactions on Programming Languages and Systems (TOPLAS), 22(4):638-672
    July 2000
    [PS] [PDF] [BibTeX]
    {A solution to the non-monotonicity problem that arises in typical data flow formulations of bytecode verification, based on [2].}

  4. Towards a Provably-Correct Implementation of the JVM Bytecode Verifier
    Alessandro Coglio, Allen Goldberg, and Zhenyu Qian
    OOPSLA'98 Workshop on the Formal Underpinnings of Java
    October 1998
    [PS] [PDF] [BibTeX]
    {A description of a preliminary version of our bytecode verifier in Specware, based on [1]. The architecture of our current, complete bytecode verifier is slightly different, closer to Sun's. This paper also appears in DARPA Information Survivability Conference and Exposition (DISCEX'00), volume 2, pages 403-410, IEEE Computer Society Press, January 2000, as well as in 1st NSA Conference on High Confidence Software and Systems, March 2001.}

  5. A Formal Specification of Java Class Loading
    Zhenyu Qian, Allen Goldberg, and Alessandro Coglio
    Technical Report, Kestrel Institute
    April 2000, revised July 2000
    [PS] [PDF] [BibTeX]
    {A complete formalization and type safety proof for an abstraction of the JVM with all the essential features of class loading, plus an improvement over Sun's design. An overview of the formalization and proof is contained in [6].}

  6. A Formal Specification of Java Class Loading
    Zhenyu Qian, Allen Goldberg, and Alessandro Coglio
    15th ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'00), volume 35, number 10 of ACM SIGPLAN Notices, pages 325-336
    October 2000
    [PS] [PDF] [BibTeX]
    {An overview of the formalization and proof in [5], augmented with additional informal descriptions and examples.}

  7. Type Safety in the JVM: Some Problems in JDK 1.2.2 and Proposed Solutions
    Alessandro Coglio and Allen Goldberg
    2nd ECOOP Workshop on Formal Techniques for Java Programs
    June 2000
    [PS] [PDF] [BibTeX]
    {An overview of the bugs we found in Sun's bytecode verifier, with a detailed desciption of one of them, along with solutions. A description of all the bugs we found and of solutions to them is contained in [8].}

  8. Type Safety in the JVM: Some Problems in Java 2 SDK 1.2 and Proposed Solutions
    Alessandro Coglio and Allen Goldberg
    Concurrency and Computation: Practice and Experience, 13(13):1153-1171
    November 2001
    [PDF] [BibTeX]
    {A complete description of all the bugs we found in Sun's bytecode verifier, along with solutions. An overview, with details about only one of the bugs, is contained in [7]. This paper supersedes the Kestrel Technical Report Type Safety in the JVM: Some Problems in JDK 1.2.2 and Proposed Solutions of April 2000. Source code, compilation instructions, and class files to demonstrate the bugs are available here.}

  9. Improving the Official Specification of Java Bytecode Verification
    Alessandro Coglio
    3rd ECOOP Workshop on Formal Techniques for Java Programs
    June 2001
    [PS] [PDF] [BibTeX]
    {Preliminary version of [10].}

  10. Improving the Official Specification of Java Bytecode Verification
    Alessandro Coglio
    Concurrency and Computation: Practice and Experience, 15(2):155-179
    February 2003
    [PDF] [BibTeX]
    {A comprehensive analysis of Sun's specification of bytecode verification and a comprehensive plan for improvement. A preliminary version is [9].}

  11. Simple Verification Technique for Complex Java Bytecode Subroutines
    Alessandro Coglio
    4th ECOOP Workshop on Formal Techniques for Java-like Programs
    June 2002
    [PS] [PDF] [BibTeX]
    {An overview of our novel technique to verify subroutines and its comparison with related work. The full formalization of the technique, including proofs, is contained in [12].}

  12. Simple Verification Technique for Complex Java Bytecode Subroutines
    Alessandro Coglio
    Concurrency and Computation: Practice and Experience, 16(7):647-670
    June 2004
    [PDF] [BibTeX]
    {A formalization of our novel technique to verify subroutines, including proofs of its properties and comparison with related work. An overview of this material can be found in [11]. This paper supersedes the Kestrel Technical Report Simple Verification Technique for Complex Java Bytecode Subroutines of December 2001, revised May 2002.}

  13. Checking Access to Protected Members in the Java Virtual Machine
    Alessandro Coglio
    6th ECOOP Workshop on Formal Techniques for Java-like Programs
    June 2004
    [PS] [PDF] [BibTeX]
    {A detailed analysis of the requirements on protected member access in the Java Virtual Machine and how to check them. Examples of incorrect checking in Sun's Java 2 SDK version 1.4 are in [14].}

  14. Checking Access to Protected Members in the Java Virtual Machine
    Alessandro Coglio
    Journal of Object Technology
    October 2005
    [PDF] [BibTeX]
    {Detailed analysis of the requirements on protected member access in the Java Virtual Machine and how to check them; examples of incorrect checking in Sun's Java 2 SDK version 1.4. A shorter version is [13]. This paper supersedes the Kestrel Institute Technical Report Checking Access to Protected Members in the Java Virtual Machine of February 2004.}

 

 

- Back to Top -


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