Do not trust the serialized VM bytecode in rocqchk by JasonGross · Pull Request #22353 · rocq-prover/rocq

JasonGross · 2026-08-18T04:37:31Z

rocqchk -bytecode-compiler yes typechecks each constant's body but takes the VM bytecode from the .vo's vmlibrary segment, with nothing tying the two together. A .vo whose bytecode disagrees with its bodies proves False and passes the checker (#22352).

This stops reading that segment. The checker compiles bytecode itself, from the bodies it just typechecked, and uses that — so the code it runs agrees with the term it checked by construction, and there is no comparison to get wrong.

const_body_code is replaced wholesale: the compiled code, the unused-argument mask, the patches and the BCalias routing all come from our own compilation, and nothing from the file survives. The mask matters independently of the VM — Conversion.eqappr passes it to convert_stacks ~mask, so a lying mask makes ordinary conversion skip comparing arguments, reachable with the default -bytecode-compiler no. I have not built an exploit for that, only closed it.

Admitted and -norec libraries get the same treatment: their bytecode is compiled from the declarations that were loaded. The trust surface is then exactly "the declarations we read", with no special case.

Earlier approach, for reviewers following the thread

The first version recompiled the bytecode and compared it against the stored bytecode. That is unworkable and has been removed. Stored and recompiled code legitimately differ in at least four ways — user vs canonical names in relocations, get_alias collapsing, the unused-argument mask, and inlining of const_inline_code bodies — and it false-rejected ordinary code. Module N := M. was enough. Thanks to @SkySkimmer for pointing out that inlining puts an equality-based fix out of reach.

Effect on the failure mode

The tampered .vo itself is now accepted, correctly: its declarations are well typed, only its bytecode segment lies, and nothing reads that. The unsoundness shows up in a library compiled against it, whose VMcast only typechecked because rocq compile believed the bogus bytecode — and that library is rejected with a plain Type error: ActualType, identical to what the non-VM checker already reports. The test asserts exactly that, and fails on master.

Checked

12 module/functor shapes accepted (the previous design false-rejected 4 of them), cross-library VM conversions through aliases and functor applications, Corelib 67/67 with -bytecode-compiler yes (master: 65/67, the two failures being #22360), test-suite/modules, and a 1853-file sweep of success/bugs under -norec with the VM on — identical results to master.

Since the segment is no longer read, #22360 no longer applies to the checker; it is still worth landing for votour.

Fixes #22352.

Opened autonomously by Claude (Opus 5) on behalf of Jason Gross (jason@theorem.dev).

SkySkimmer · 2026-08-18T08:48:57Z

Does this work when modules are involved? Especially functor applications.

JasonGross · 2026-08-18T16:59:30Z

Does this work when modules are involved? Especially functor applications.

Apparently not:

Unset Elimination Schemes.
Inductive bool : Set := true | false.
Definition negb (b:bool) : bool := match b with true => false | false => true end.

Module M.
  Axiom ax : bool.
  Definition d := negb ax.
End M.
Module N := M.

is enough to trigger an error with this PR.

AI elaborates on two issues

Two distinct mechanisms, both from the stored code for a strengthened or substituted field being produced by renaming — Vmbytegen.compile_alias (kernel/modops.ml:222) then subst_body_code — while the check regenerates it with compile_constant_body, which optimises against the current environment:

User vs canonical names. N.ax carries BCalias A.M.ax; N.d's reloc is only substituted, so it still names A.N.ax, whereas recompiling negb N.ax follows the alias and emits A.M.ax. eq_reloc_info compares with Constant.UserOrd.equal (kernel/vmemitcodes.ml:38), so delta-equivalent code compares unequal. Using CanOrd for that one comparison inside the new equal_to_patch_and_patches fixes every case of this shape I have, and the tampered files are still rejected.

Environment-dependent code generation across functor application, which CanOrd does not fix. Inside a functor the parameter's fields are Undef/BCconstant; after application the argument's fields may be aliases, or may ignore arguments, so recompilation legitimately yields different and better-optimised code. With Definition f (b:bool) := true in the argument, genlambda's unused-argument mask erases an entire subcomputation on recompile and tp_code itself differs.

So structural equality on the compiled form is the wrong comparison. Either it has to compare up to delta-equivalence and alias/mask collapsing, or the check has to re-derive the stored code the way the kernel does (subst_body_code over the functor's code) instead of recompiling. Marking this draft until it's sorted

Do you have thoughts on whether we should

Make the equality comparison compare up to delta-equivalence and alias/mask collapsing
Make equality re-derive the stored code the way the kernel does (subst_body_code over the functor's code) instead of recompiling
Drop and recompile in general
Drop and recompile in general and warn on inequality instead of error

?

SkySkimmer · 2026-08-18T17:26:27Z

There's also inlining so trying to adapt the equality doesn't really seem possible IMO

JasonGross · 2026-08-18T19:48:47Z

Do we care enough to make vm recompilation of libraries lazy when loading with -norec / -admit? (We should not trust the vm code in -admit libs; I want rocqchk to be composable (if you check a module and then -admit it in another check, this should be as robust as not admitting it in the first place).)

ppedrot · 2026-08-24T14:18:04Z


 val dirpath_of_library : compiled_library -> DirPath.t
 val module_of_library : compiled_library -> Mod_declarations.module_body
+val replace_module_of_library : compiled_library -> Mod_declarations.module_body -> compiled_library


I think I'd rather have this function perform the recompilation rather than just trusting the module body, and move the compilation code somewhere around the kernel VM API.

Should be fixed

ppedrot · 2026-08-24T14:19:20Z

+  let dp = Safe_typing.dirpath_of_library clib in
+  let retro = Safe_typing.retroknowledge_of_library clib in
+  let env = env_of_library senv clib in
+  let vmtab, clib = compile_vm_library env clib in


Is is me or are we now unconditionally recompiling the VM segment even when the VM is disabled?

Thanks, fixed

ppedrot · 2026-08-26T19:58:26Z

@coqbot run full ci

silene · 2026-08-31T15:25:41Z

@@ -0,0 +1,10 @@
+- **Fixed:**
+  ``rocqchk`` with ``-bytecode-compiler yes`` no longer trusts the VM bytecode
+  serialized in a ``.vo``: it does not read the ``vmlibrary`` segment at all, and


Does that mean that rocqchk will not report a crafted .vo file? Could we instead have it complain loudly if there is a discrepancy?

That is what I tried to do originally, but the vm bytecode differs depending on whether a constant was constructed "in the normal way" or whether it is a result of module functor application / module inclusion with parameter inlining. I figured it was better to drop the vm segment entirely (in the same way the checker ignores .coq-native) rather than pull in all the functor machinery.

I see. Sorry for the noise. I had missed the edits to the original post.

ppedrot · 2026-08-31T15:53:28Z

+   read. *)
+let recompile_vm_library env lib =
+  let vmtab = Vmlibrary.set_path lib.comp_name (Environ.vm_library env) in
+  if not (Environ.typing_flags env).enable_VM then vmtab, lib


On second reading this check doesn't belong there, it should be the job of the checker to decide whether to recompile or not, and it should do so with the user-facing flag rather than the flag from the environment.

ppedrot · 2026-08-31T15:54:58Z

@JasonGross I think this deserves to be squashed (and maybe to have my freshest nitpick fixed). Also, I'm waiting for input from @SkySkimmer to be sure he is fine with this PR before merging it.

rocqchk with -bytecode-compiler yes typechecked each constant's body but took the VM bytecode from the separately serialized vmlibrary segment of the .vo, with nothing binding the two together. A crafted file whose vmlibrary disagrees with its library makes a VM conversion prove False, and rocqchk accepts the result with no axioms reported. The checker now compiles the bytecode itself, from the bodies it checks, so the two agree by construction. The vmlibrary segment is not read at all, and the code descriptor stored in each declaration (const_body_code) is replaced rather than kept: BCalias and the unused-argument mask are attacker-controlled too, and the mask is used by ordinary conversion as well. Libraries imported with -admit or as dependencies of -norec get the same treatment, so the trusted surface is uniformly the declarations that are read. Recompiling the bytecode and comparing it against the stored one instead is not workable: stored and recompiled code legitimately differ in relocation names (user vs canonical), in alias collapsing, in the unused-argument mask, and in the inlining of const_inline_code bodies. The compilation itself lives in Modops, next to add_structure, which threads the environment the same way; Safe_typing.recompile_vm_library performs it and substitutes the result, so the kernel exposes no setter that takes a module body on trust. Whether to recompile at all is the checker's decision, taken from the user-facing -bytecode-compiler flag: with the default, no bytecode is ever run, so the traversal is skipped and an empty table handed over. Fixes rocq-prover#22352. Co-authored-by: Jason Gross <jason@theorem.dev> Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

JasonGross · 2026-08-31T17:12:44Z

@ppedrot updated. And with rocq-prover/bot#384 you can now have coqbot squash for you

JasonGross requested review from a team as code owners August 18, 2026 04:37

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Aug 18, 2026

coqbot-app Bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Aug 18, 2026

SkySkimmer reviewed Aug 18, 2026

View reviewed changes

Comment thread test-suite/misc/rocqchk_vm_bytecode.sh

SkySkimmer reviewed Aug 18, 2026

View reviewed changes

Comment thread dev/doc/critical-bugs.md Outdated

JasonGross force-pushed the coqchk-verify-vm-bytecode branch from dce008b to 2b60b53 Compare August 18, 2026 15:46

JasonGross changed the title ~~Verify serialized VM bytecode in coqchk~~ Verify serialized VM bytecode in rocqchk Aug 18, 2026

coqbot-app Bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Aug 18, 2026

JasonGross marked this pull request as draft August 18, 2026 16:59

JasonGross force-pushed the coqchk-verify-vm-bytecode branch from 2b60b53 to 89832f7 Compare August 18, 2026 20:15

JasonGross changed the title ~~Verify serialized VM bytecode in rocqchk~~ Do not trust the serialized VM bytecode in rocqchk Aug 18, 2026

JasonGross mentioned this pull request Aug 18, 2026

Backport three rocqchk fixes (vm_caml_prim arity, -norec validation order, VM bytecode trust) theorem-labs/rocq#9

Merged

JasonGross marked this pull request as ready for review August 19, 2026 16:17

ppedrot added this to the 9.2.1 milestone Aug 24, 2026

ppedrot reviewed Aug 24, 2026

View reviewed changes

ppedrot self-assigned this Aug 26, 2026

ppedrot approved these changes Aug 26, 2026

View reviewed changes

coqbot-app Bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Aug 26, 2026

JasonGross added the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 29, 2026

coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 29, 2026

silene reviewed Aug 31, 2026

View reviewed changes

ppedrot reviewed Aug 31, 2026

View reviewed changes

JasonGross added the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 31, 2026

JasonGross force-pushed the coqchk-verify-vm-bytecode branch from 9d8b43a to 1ec462f Compare August 31, 2026 17:02

coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Aug 31, 2026

github-actions Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 1, 2026

Uh oh!

Conversation

JasonGross commented Aug 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Earlier approach, for reviewers following the thread

Effect on the failure mode

Checked

Uh oh!

Uh oh!

SkySkimmer commented Aug 18, 2026

Uh oh!

Uh oh!

JasonGross commented Aug 18, 2026

Uh oh!

SkySkimmer commented Aug 18, 2026

Uh oh!

JasonGross commented Aug 18, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ppedrot Aug 24, 2026

Choose a reason for hiding this comment

Uh oh!

JasonGross Aug 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ppedrot Aug 24, 2026

Choose a reason for hiding this comment

Uh oh!

JasonGross Aug 24, 2026

Choose a reason for hiding this comment

Uh oh!

ppedrot commented Aug 26, 2026

Uh oh!

silene Aug 31, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

JasonGross Aug 31, 2026

Choose a reason for hiding this comment

Uh oh!

silene Aug 31, 2026

Choose a reason for hiding this comment

Uh oh!

ppedrot Aug 31, 2026

Choose a reason for hiding this comment

Uh oh!

ppedrot commented Aug 31, 2026

Uh oh!

JasonGross commented Aug 31, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

JasonGross commented Aug 18, 2026 •

edited

Loading

JasonGross commented Aug 18, 2026 •

edited

Loading

JasonGross Aug 24, 2026 •

edited

Loading

silene Aug 31, 2026 •

edited

Loading