Why Formalize the Java Bytecode Verifier and Loader?

• Verifier and loader are fundamental to JVM security

• Sun’s implementation is complex, 60 pages of C code

• High-level spec supports extensions to bytecode verification:

  • Extended type system
    • information flow
  • Analysis
    • null pointer de-reference
    • array bounds checking
    • safe narrowing casts

Previous slide

Next slide

Back to first slide

View graphic version