Theory surrounding JVM 2

What is the foundational security architecture of Java?

-Mobile-code paradigm: write code locally, compile to platform-independent bytecode (.class files)

• Distribute across networks for execution on remote hosts

• Requires safety verification before execution without severe runtime overhead

What are the two trust boundary dilemmas for JVM?

-Untrusted sources: host downloads bytecode from potentially hostile networks

• Malicious compiler threat: cannot assume bytecode from compliant compiler (manual binary construction possible)
• Solution must guarantee safety before execution begins

What are the three core safety properties enforced by JVM verification?

-Type safety invariance: every instruction receives operands of exact expected type

• Operand stack neutrality: no underflow/overflow, stack height consistent across all control flow branches
• Access control & memory integrity: data visibility rules (private variables) and reference semantics enforced

What is operand stack neutrality?

-JVM is stack-based abstract machine

• Prevents stack underflow (popping from empty stack) and stack overflow
• Guarantees stack height and structural layout consistent across all possible control flow branches at any instruction location

What happens during the JVM static analysis pass at class-loading time?

-Static bytecode verifier runs before code execution

• Treats instructions as state transition system
• Runs data-flow analysis loop tracking abstract type states (not concrete values) across control-flow graph

What is the risk if the JVM verifier contains a software bug?

-Analysis pass runs on consumer's machine every program load

• Invalid or malicious file might slip through verification
• Compromises entire host system

What is the approach for formal executable modeling of JVM in ITP?

-Construct fully functioning executable interpreter of JVM inside proof assistant (Rocq/Coq)

• Define types for stack, local variables, class tables, instruction states in type theory
• JVM instruction formalized as function: exec_instr : Instruction → JVMState → JVMState

How are structural properties proved for JVM instructions in ITP?

-Write and prove absolute theorems about entire instruction sets

• Example for IADD (integer add): ∀ s: JVMState, well_formed s → well_formed (exec_instr IADD s)
• Proves valid starting state never causes underflow, type corruption, or stack crash

What is the B-Method?

-Correct-by-construction approach (Jean-Raymond Abrial)

• Write high-level mathematical specification using Abstract Machine Notation (AMN)
• Systematically translate to concrete models using strict mathematical refinement rules

What is the refinement pipeline in B-Method?

-High-level specification translated to increasingly concrete implementation models

• Each step mathematically proven to preserve invariants of abstract specification
• Final compiled code guaranteed free of runtime logic bugs by design

What industrial system used the B-Method?

-Paris Metro Line 14 (driverless train control systems)

• Automated safety controls verified correct-by-construction
• Moved burden of proof from runtime defensive analysis to initial software construction

What is the difference between JVM defensive verification and correct-by-construction?

-JVM: checks potentially flawed compiled code at runtime (defensive framework)

• Correct-by-construction: eliminates runtime validation overhead entirely
• B-Method verifies during construction, not after compilation