Specification and Synthesized Implementation of Java Bytecode Verifier and Loader

7/6/98


Click here to start


Table of Contents

Specification and Synthesized Implementation of Java Bytecode Verifier and Loader

Starting point: two “semi-formal” specifications

Background and Motivation

Why Formalize the Java Bytecode Verifier and Loader?

Information Flow

Java Virtual Machine

Java Concepts

Class Files

JVM Loading

Local and Global Consistency

Structure of the JVM

Bytecode Local Consistency Checks

A Dataflow Approach to Bytecode Verification

Data Flow Analysis

Intra-Procedural Data Flow Analysis

Instantiation of the DF Architecture

Lattice Construction: Formalization of JVM Primitive Types

Reference Types

JVM Type Categories

Subtype Assertions

Signature Assertions

Lattice Structure

Global Consistency

Consistent Assertion Sets

Typing Contexts

Lattice Theory

Lattice Constructions

Lattice for the JVM

Lg

LUB for Objects

No LUB in the Presence of Interfaces

Le

Transfer Functions

Transfer Functions

Example

Proving Transfer Functions Distributive

Object Initialization

Object Initialization

Control Flow Graph

Control Flow Graph

What did the designers of JVM Learn From COBOL?

Propagating the Types of Unexamined Variables

Constraint Solving

Applications

System Components

Data Flow Architecture in Specware

Formalization in Specware

Formalization

Refinement

Testing and Verification

Related Work

Related Work

Author: Allen Goldberg

Email: goldberg@kestrel.edu

Home Page: http://www.kestrel.edu