Bytecode verifier — JVMS coverage, gaps, and residual attacker capability

Scope: classloading/src/{verifier,bytecode_verifier,verify_insn,verify_frame,vtype}.rs.

This document is the honest inventory. It states, rule by rule, what CratonVM's verifier enforces, where the enforcement lives, which test pins it, and — in the last two sections — exactly what an attacker with control over a .class file can still do today.

Terminology used throughout:

• Pass 2 — structural class checks (verifier::verify_class_structure): access flags, final class/method constraints, Code attribute presence.
• Pass 3 / structural — JVMS §4.9.1 static constraints over a method body (verifier::verify_method_structural): decode, branch and handler bounds, local-index and max_locals conformance. Consults no class hierarchy.
• Pass 3 / type-state — JVMS §4.10 operand-stack and local type checking. Two algorithms: the split verifier (StackMapTable-driven linear walk, §4.10.1) and type inference (worklist dataflow to fixpoint, §4.10.2).

---

1. Verifier selection

The pre-Java-7 failover is new and closes a type-confusion hole. Previously a class file declaring major 50 and shipping a token StackMapTable skipped the worklist (the dispatch tested stack_map_table.is_none()) and then took the lenient linear walk, whose strict merge checks are gated on requires_stack_map — i.e. off for major ≤ 50. A branch to a target with no declared frame was therefore typed by whatever fell through into it. Reaching that target along the branch with a shallower operand stack is a run-time underflow the verifier had signed off on. JVMS §4.10 already defines the remedy for this exact version range (failover to §4.10.2 inference), and that is what the two pre_java7_partial_frames sites now do: any handler entry or branch target without a declared frame hands the whole method to the worklist, which merges at every edge and needs no declared frames at all.

Type inference (JVMS §4.10.2) — implementation status

Implemented, in two mirrored copies: bytecode_verifier::verify_by_inference (bytecode_verifier.rs:736, the main path) and verifier::verify_pre_java7_inference (verifier.rs:962, the path taken by the non-jsr methods of a jsr-bearing class).

Both are worklist dataflow to fixpoint over the instruction graph, merging frame states at every branch target (merge_inference_frame) and at every exception-handler entry whose protected range covers the current pc. The lattice is vtype::VType: Top, Int, Float, Long, Double, Null, ObjectRef, ArrayRef, UninitializedThis, Uninitialized(offset), ReturnAddress(pc), with category-2 slot pairing, array covariance (vtype.rs:370) and least-upper-bound merges (vtype.rs:328).

The one subset that is not modelled is subroutines (§4.10.2.5) — see §4 below. That subset does not fall through to acceptance by the inference engine; it is diverted before the walk starts.

---

2. Rule-by-rule coverage

file:line is the enforcement site. Line numbers drift; the function names do not.

JVMS §4.9.1 — static constraints on the Code array

The structural scan used to run only for jsr-bearing classes. Ordinary classes went straight to bytecode_verifier::verify_method, which validated the code array (through verified_code) but never looked at the exception table. A handler whose handler_pc landed mid-instruction was accepted, because the type-state walk only consults handler_pc as a map key and simply never matched it — while the interpreter, which does dispatch there, began decoding at a mid-instruction offset. verify_method now runs the scan first (bytecode_verifier.rs:190).

Three exception-table rules are enforced twice, at two layers. JVMS §4.7.3 states start_pc < end_pc, handler_pc < code_length and "catch_type is 0 or a CONSTANT_Class" as format constraints on the Code attribute, and cratonvm_reader checks all three while decoding it — so a class file carrying one of those shapes is a ClassReaderError and never reaches Pass 3 — on the eager and lazy decode paths alike (decode_attribute re-runs both checks, so a Code nested inside another attribute cannot slip past). The verifier keeps its own copy of each check regardless, because a CodeAttribute built in memory rather than decoded from bytes — the LazyAttribute::new_decoded form used by synthetic stubs, cached class data and tests — reaches the verifier without ever passing through the reader. The practical consequence for this table is that a corpus case for one of these three rules can only ever observe the reader's verdict, which is why the three corpus cases assert there (reject_at_parse) while the verifier's half is pinned by the in-memory verifier.rs unit tests cited alongside them. The boundary-landing rule in the row between them has no reader-side counterpart — the reader does not decode instructions — so it stays a pure corpus case.

JVMS §4.10.1 / §4.10.2 — type checking

JVMS §4.4 / §4.9.1 — constant-pool cross-checks

JVMS §5.4.5 / Pass 2 — class-level structural rules

---

3. Remaining gaps

Ordered by how much an attacker gains.

1. Pass 3 type-state is deferred entirely for user-defined-loader classes. class_manager.rs::define_class_with_options sets defer_loader_sensitive_pass3 = loader_aware_resolution() && loader is UserDefined, and loader_aware_resolution() defaults on. Every Spring / WildFly / H2 / Elasticsearch application class is defined by a user-defined loader, so for those classes no operand-stack or local type-state check is made at all. vm_util.rs deliberately does not repeat Pass 3 at link time either. The deferral exists for a real reason — the hierarchy adapter available at that point cannot always keep two loaders' same-named classes apart, so its assignability verdicts can be wrong, and a wrong verdict is a spurious VerifyError on bytecode HotSpot accepts. It is a statement about the hierarchy, not about the rest of the verifier. Partially closed: the deferred path now runs verifier::verify_class_structural_bytecode (the hierarchy-independent §4.9.1 scan) and rejects on failure. What remains deferred is exactly the type-state verdict. Closing it fully requires a loader-faithful hierarchy adapter at define time.

2. Subroutines (jsr / ret, JVMS §4.10.2.5) are not type-state verified. See §4.

3. §4.10.2.4 — an uninitialized(offset) value may survive a backward branch. JVMS requires that no uninitialized value be live across a backward branch (it would alias two distinct allocations at the same new offset). The worklist does not check this. Consequence: a crafted loop can make two live objects share the Uninitialized(offset) identity, so invokespecial <init> on one initializes both in the verifier's model. The receiver still has the right shape (the new site's class), so this is an initialization-order violation rather than a type confusion.

4. §4.10.1.8 protected-member access is not checked by the verifier. Access control is enforced at resolution time by access_control.rs (JVMS §5.4.4), which covers public/protected/ package-private/private visibility. The additional verifier-time rule — for a protected member of a superclass in another package, the receiver type must be assignable to the currently-verified class — is not enforced. Consequence: a class in package p can invoke q.Super's protected member on a receiver typed q.Super rather than on itself. Resolution-time access control still requires that the caller be a subclass, so the escalation is narrower than a full bypass.

5. tableswitch low ≤ high and lookupswitch key ordering are not checked. The decoder reads the operands and every target is bounds-checked, so this cannot reach an out-of-range jump; a mis-ordered lookupswitch degrades a run-time binary search to a wrong-but-in-range arm.

6. Name legality (JVMS §4.2.2) is not validated beyond emptiness and the descriptor-internal ./[/; rules. A method named foo;bar loads.

7. Concrete-class abstract-method implementation is not enforced (verify_abstract_method_implementation is compiled but not called — verifier.rs:1846). HotSpot also defers this to invocation time (AbstractMethodError), so this is a compatibility choice, not a hole.

8. The new-site owner-match (§4.10.1.9) runs only on the verifier.rs paths, not inside bytecode_verifier::verify_method. The type-state check still requires the receiver to be Uninitialized(offset) and initializes it to the constructor's owner, so a mismatch produces a wrongly-typed reference rather than an uninitialized one.

9. Two near-duplicate implementations of both the split verifier and the inference worklist exist (bytecode_verifier.rs and verifier.rs). They are kept in sync by hand. Every fix above had to be applied twice; a future fix applied once would leave the jsr-bearing-class path behind.

---

4. Configurations that weaken verification

Every entry in this table is observable: type_maps::verification_status distinguishes Unknown (not verified yet) from Skipped (never will be), and MethodTypeMaps::fast_path_veto() names the reason a method's proof is incomplete. Consumers that see either must scan conservatively and must not take the unchecked interpreter fast path.

---

5. What an attacker can still do with a malformed class today

Assume the attacker controls the full byte content of a .class file and can get it loaded. Ranked by severity.

1. Skip type-state verification entirely by using a custom class loader. With the default CRATONVM_LOADER_AWARE_RESOLUTION=1, a class defined through a user-defined ClassLoader.defineClass gets Pass 2 plus the structural §4.9.1 scan, and no §4.10 type-state check. Within the structural envelope — every branch in range and on a boundary, every local index below max_locals, every handler well-formed, operand-stack depth not checked — the attacker has free rein over types: store an int into a local and read it back as a reference, call a method on a receiver of the wrong class, return an unrelated type. This is a full memory-safety escape and it is the single most important open item. It is not a new regression; it predates this work and is documented here for the first time.

2. Skip everything with --noverify / -Xverify:none, or by reaching a skip_verification: true define path. Both are explicit operator or embedder choices, both are recorded as VerificationStatus::Skipped, and both are outside the verifier's control.

3. Run unverified operand-stack and local type-state inside a jsr subroutine by shipping a class file with major ≤ 50 that contains jsr/ret. The structural scan still applies (targets in range, on boundaries, ret covered by a reachable prologue, handler ranges valid), so this is not arbitrary — but inside the subroutine body the operand stack is unchecked. HotSpot loads the same class and applies §4.10.2.5 inlining; CratonVM loads it and does not. Logged as a warn! on every occurrence, and the affected methods publish zero oop-map rows with FastPathVeto::Subroutine, so the GC scans them conservatively and the unchecked interpreter fast path is denied.

4. Alias two allocations through one Uninitialized(offset) with a backward branch (gap 3). The resulting reference has the correct class, so this yields an object whose constructor ran twice or not at all, not a type confusion.

5. Invoke a protected superclass member on a foreign receiver of the declaring type (gap 4), within what resolution-time access control permits.

6. Load a class with names that are illegal per §4.2.2 (gap 6). No memory effect; it can confuse tooling and log output.

What an attacker cannot do any more, that they could before this work:

• reach the interpreter through an exception handler whose handler_pc is out of range or mid-instruction (any class, any loader);
• under-declare max_locals so that argument slots or a wide local operand index past the end of the runtime frame;
• split a long/double local pair and read the torn value back as a wide value;
• panic the verifier with wide lstore 65535 (index + 1 overflow) or with an unterminated L… descriptor in any NameAndType (an out-of-range slice);
• get a new / instanceof past the verifier with a constant-pool operand that is not a CONSTANT_Class, or a new of an array type;
• disable the operand type check on a field access by supplying a malformed field descriptor (which used to degrade to Top, and everything is assignable to Top);
• have a constructor return without ever calling this() / super();
• exploit a partial StackMapTable on a major-50 class to reach a frameless branch target typed from the fall-through edge.

---

6. Error contract

Every rejection is cratonvm_types::error::LinkageError::VerifyError { class_name, method_name, message }, surfaced to callers as VmError::Linkage(LinkageError::VerifyError { .. }). Messages name the rule and, where the walk knows it, the bytecode offset — verify_instruction failures are wrapped with "at bytecode offset {pc}: …" by both walkers, and the structural scan embeds at offset {pc} / handler_pc={n} directly.

There is no panic! / unwrap / expect on attacker-controlled input in the verifier: every constant-pool lookup returns Option and is converted to a VerifyError, every descriptor slice bound comes from vtype::field_descriptor_len (which never reports a length past the end of the input), and every index arithmetic that can overflow uses checked_add.

---

7. Test inventory

Run: cargo test -p cratonvm-classloading verifier.