Do not trust the serialized VM bytecode in rocqchk

checker/checkFlags.ml

@@ -32,3 +32,8 @@ let set_local_flags flags env =
   }
   in
   Environ.set_typing_flags flags env
+
+(* Set from the -bytecode-compiler command line option. The checker consults
+   this rather than the environment's flag when deciding whether to recompile
+   the VM bytecode of a library. *)
+let enable_vm = ref false

checker/checkFlags.mli

@@ -10,3 +10,6 @@
 
 val set_local_flags : Declarations.typing_flags -> Environ.env -> Environ.env
 (** Set flags except for those ignored by the checker (see .ml file for those). *)
+
+(** Whether the user asked for the VM, i.e. the value of -bytecode-compiler. *)
+val enable_vm : bool ref

checker/checkLibrary.ml

@@ -60,7 +60,6 @@ type library_t = {
   library_opaques : seg_proofs;
   library_deps : (compilation_unit_name * Safe_typing.vodigest) array;
   library_digest : Safe_typing.vodigest;
-  library_vm : Vmlibrary.on_disk;
 }
 
 module LibraryOrdered =
@@ -125,12 +124,12 @@ let check_one_lib admit senv (dir,m) =
     if LibrarySet.mem dir admit then
       (Flags.if_verbose Feedback.msg_notice
          (str "Admitting library: " ++ pr_dirpath dir);
-       Safe_checking.unsafe_import (fst senv) md m.library_vm dig),
+       Safe_checking.unsafe_import (fst senv) md dig),
       (snd senv)
     else
       (Flags.if_verbose Feedback.msg_notice
          (str "Checking library: " ++ pr_dirpath dir);
-       Safe_checking.import (fst senv) (snd senv) md m.library_vm dig)
+       Safe_checking.import (fst senv) (snd senv) md dig)
   in
     register_loaded_library m; senv
 
@@ -295,14 +294,13 @@ type library_disk = {
   md_objects : library_objects;
 }
 
-let mk_library sd md f table digest vm = {
+let mk_library sd md f table digest = {
   library_name = sd.md_name;
   library_filename = f;
   library_compiled = md.md_compiled;
   library_opaques = table;
   library_deps = sd.md_deps;
   library_digest = digest;
-  library_vm = vm;
 }
 
 let name_clash_message dir mdir f =
@@ -338,30 +336,27 @@ let marshal_in_segment (type a) ~validate ~value ~(segment : a ObjFile.segment)
 let summary_seg : summary_disk ObjFile.id = ObjFile.make_id "summary"
 let library_seg : library_disk ObjFile.id = ObjFile.make_id "library"
 let opaques_seg : seg_proofs ObjFile.id = ObjFile.make_id "opaques"
-let vm_seg = Vmlibrary.vm_segment
 
-let intern_from_file ~intern_mode ~enable_VM (dir, f) =
+(* The [vmlibrary] segment is deliberately not read: the checker compiles the VM
+   bytecode itself from the declarations it checks (see [Safe_checking]), so the
+   serialized bytecode is neither trusted nor needed. *)
+let intern_from_file ~intern_mode (dir, f) =
   let validate = intern_mode <> Dep in
   Flags.if_verbose chk_pp (str"[intern "++str f++str" ...");
-  let (sd,md,table,vmlib,digest) =
+  let (sd,md,table,digest) =
     try
       (* First pass to read the metadata of the file *)
       let ch = System.with_magic_number_check raw_intern_library f in
       let seg_sd = ObjFile.get_segment ch ~segment:summary_seg in
       let seg_md = ObjFile.get_segment ch ~segment:library_seg in
       let seg_opaque = ObjFile.get_segment ch ~segment:opaques_seg in
-      let seg_vmlib = ObjFile.get_segment ch ~segment:vm_seg in
       let () = ObjFile.close_in ch in
       (* Actually read the data *)
       let ch = open_in_bin f in
 
       let sd = marshal_in_segment ~validate ~value:Values.v_libsum ~segment:seg_sd f ch in
       let md = marshal_in_segment ~validate ~value:Values.v_lib ~segment:seg_md f ch in
       let table = marshal_in_segment ~validate ~value:Values.v_opaquetable ~segment:seg_opaque f ch in
-      let vmlib = if enable_VM
-        then marshal_in_segment ~validate ~value:Values.v_vmlib ~segment:seg_vmlib f ch
-        else Vmlibrary.(export (set_path dir empty))
-      in
       (* Verification of the final checksum *)
       let () = close_in ch in
       let () = System.check_caml_version ~caml:sd.md_ocaml ~file:f in
@@ -371,21 +366,21 @@ let intern_from_file ~intern_mode ~enable_VM (dir, f) =
       Flags.if_verbose chk_pp (str" done]" ++ fnl ());
       let digest =
         Safe_typing.Dvo_or_vi seg_md.hash in
-      sd,md,table,vmlib,digest
+      sd,md,table,digest
     with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in
   depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
   opaque_tables := LibraryMap.add sd.md_name table !opaque_tables;
-  mk_library sd md f table digest (Vmlibrary.inject vmlib)
+  mk_library sd md f table digest
 
-let intern_from_file ~intern_mode ~enable_VM dirf : library_t =
+let intern_from_file ~intern_mode dirf : library_t =
   NewProfile.profile "intern_from_file"
     ~args:(fun () -> [("name", `String (DirPath.to_string (fst dirf)))])
-    (fun () -> intern_from_file ~intern_mode ~enable_VM dirf)
+    (fun () -> intern_from_file ~intern_mode dirf)
     ()
 
 (* Read a compiled library and all dependencies, in reverse order.
    Do not include files that are already in the context. *)
-let rec intern_library ~intern_mode ~enable_VM seen (dir, f) needed =
+let rec intern_library ~intern_mode seen (dir, f) needed =
   if LibrarySet.mem dir seen then failwith "Recursive dependencies!";
   (* Look if in the current logical environment *)
   try let _ = find_library dir in needed
@@ -394,13 +389,13 @@ let rec intern_library ~intern_mode ~enable_VM seen (dir, f) needed =
   if List.mem_assoc_f DirPath.equal dir needed then needed
   else
     (* [dir] is an absolute name which matches [f] which must be in loadpath *)
-    let m = intern_from_file ~intern_mode ~enable_VM (dir,f) in
+    let m = intern_from_file ~intern_mode (dir,f) in
     let seen' = LibrarySet.add dir seen in
     let deps =
       Array.map (fun (d,_) -> try_locate_absolute_library d) m.library_deps
     in
     let intern_mode = match intern_mode with Rec -> Rec | Root | Dep -> Dep in
-    (dir,m) :: Array.fold_right (intern_library ~intern_mode ~enable_VM seen') deps needed
+    (dir,m) :: Array.fold_right (intern_library ~intern_mode seen') deps needed
 
 (* Compute the reflexive transitive dependency closure *)
 let rec fold_deps seen ff (dir,f) (s,acc) =
@@ -424,12 +419,11 @@ let fold_deps_list ff modl acc =
   snd (fold_deps_list LibrarySet.empty ff modl (LibrarySet.empty,acc))
 
 let recheck_library senv ~norec ~admit ~check =
-  let enable_VM = (Environ.typing_flags (Safe_typing.env_of_safe_env senv)).enable_VM in
   let ml = List.map try_locate_qualified_library check in
   let nrl = List.map try_locate_qualified_library norec in
   let al =  List.map try_locate_qualified_library admit in
-  let needed = List.fold_right (intern_library ~intern_mode:Rec ~enable_VM LibrarySet.empty) ml [] in
-  let needed = List.fold_right (intern_library ~intern_mode:Root ~enable_VM LibrarySet.empty) nrl needed in
+  let needed = List.fold_right (intern_library ~intern_mode:Rec LibrarySet.empty) ml [] in
+  let needed = List.fold_right (intern_library ~intern_mode:Root LibrarySet.empty) nrl needed in
   let needed = List.rev needed in
   (* first compute the closure of norec, remove closure of check,
      add closure of admit, and finally remove norec and check *)

checker/coqchk_main.ml

@@ -171,7 +171,10 @@ let make_senv () =
     if !enable_vm && not Coq_config.bytecode_compiler then begin
       warn_no_bytecode ();
       senv
-    end else Safe_typing.set_VM !enable_vm senv
+    end else begin
+      CheckFlags.enable_vm := !enable_vm;
+      Safe_typing.set_VM !enable_vm senv
+    end
   in
   let senv = Safe_typing.set_allow_sprop true senv in (* be smarter later *)
   Safe_typing.set_native_compiler false senv

checker/mod_checking.ml

@@ -290,6 +290,16 @@ let rec check_module env opac mp mb opacify =
       let opacify = collect_constants_without_body (mod_type mb) mp opacify in
       (* TODO: a bit wasteful, we recheck the types of parameters twice *)
       let sign_struct = Modops.annotate_struct_body sign_struct (mod_type mb) in
+      (* The implementation is checked in its own right, hence its bytecode is
+         compiled too; it is local to this check and never exported. With the VM
+         disabled the bytecode is never run, so we skip the recompilation. *)
+      let env, sign_struct =
+        if !CheckFlags.enable_vm then
+          let vmtab, sign_struct =
+            Modops.compile_signature env (Environ.vm_library env) mp reso sign_struct in
+          Environ.set_vm_library vmtab env, sign_struct
+        else env, sign_struct
+      in
       let opac = check_signature env opac sign_struct mp reso opacify in
       Some (sign_struct, reso), opac
     | Algebraic me -> Some (check_mexpression env me (mod_type mb) mp delta_mb), opac

checker/safe_checking.ml

@@ -10,11 +10,7 @@
 
 open Environ
 
-let import senv opac clib vmtab digest =
-  let senv = Safe_typing.check_flags_for_library clib senv in
-  let dp = Safe_typing.dirpath_of_library clib in
-  let mb = Safe_typing.module_of_library clib in
-  let retro = Safe_typing.retroknowledge_of_library clib in
+let env_of_library senv clib =
   let env = Safe_typing.env_of_safe_env senv in
   let qualities, univs = Safe_typing.univs_of_library clib in
   let check_quality q =
@@ -23,18 +19,43 @@ let import senv opac clib vmtab digest =
   let () = assert (Sorts.QGlobal.Set.for_all check_quality (fst qualities)) in
   let env = Environ.push_qualities (Sorts.Quality.Set.of_qglobals @@ fst qualities) env in
   let env = Environ.merge_elim_constraints ~rigid:true (snd qualities) env in
-  let env = push_context_set ~strict:true univs env in
-  let env = Environ.link_vm_library vmtab env in
+  push_context_set ~strict:true univs env
+
+(* The checker does not read the [vmlibrary] segment of the file at all: the
+   bytecode of every constant is recompiled from the declarations about to be
+   checked (see [Safe_typing.recompile_vm_library]), and the resulting table is
+   handed to [Safe_typing.import] in place of the one stored in the file.
+
+   With -bytecode-compiler no, the default, no bytecode is ever run, so there is
+   nothing to recompile and we hand over an empty table. *)
+let vm_library_of env clib =
+  if !CheckFlags.enable_vm then Safe_typing.recompile_vm_library env clib
+  else Safe_typing.empty_vm_library env clib, clib
+
+let import senv opac clib digest =
+  let senv = Safe_typing.check_flags_for_library clib senv in
+  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 = vm_library_of env clib in
+  let env = Environ.set_vm_library vmtab env in
+  let mb = Safe_typing.module_of_library clib in
   let opac = Mod_checking.check_module env opac retro (Names.ModPath.MPfile dp) mb in
+  let vmtab = Vmlibrary.inject (Vmlibrary.export vmtab) in
   let (_,senv) = Safe_typing.import clib vmtab digest senv in senv, opac
 
-let import senv opac clib vmtab digest : _ * _ =
+let import senv opac clib digest : _ * _ =
   NewProfile.profile "import"
     ~args:(fun () ->
         let dp = Safe_typing.dirpath_of_library clib in
         [("name", `String (Names.DirPath.to_string dp))])
-    (fun () ->import senv opac clib vmtab digest)
+    (fun () ->import senv opac clib digest)
     ()
 
-let unsafe_import senv clib vmtab digest =
+let unsafe_import senv clib digest =
+  (* Admitted libraries are trusted for their declarations, but their bytecode is
+     recompiled all the same, so that the trusted surface is exactly the same. *)
+  let env = env_of_library senv clib in
+  let vmtab, clib = vm_library_of env clib in
+  let vmtab = Vmlibrary.inject (Vmlibrary.export vmtab) in
   let (_,senv) = Safe_typing.import clib vmtab digest senv in senv

checker/safe_checking.mli

@@ -16,12 +16,10 @@ val import
   : safe_environment
   -> Mod_checking.opaques
   -> compiled_library
-  -> Vmlibrary.on_disk
   -> vodigest -> safe_environment * Mod_checking.opaques
 
 val unsafe_import
   : safe_environment
   -> compiled_library
-  -> Vmlibrary.on_disk
   -> vodigest
   -> safe_environment

dev/doc/critical-bugs.md

@@ -98,6 +98,7 @@ This file recollects knowledge about critical bugs found in Coq since version 8.
       - [guard condition issue made it inconsistent with propositional extensionality in library Sets](#guard-condition-issue-made-it-inconsistent-with-propositional-extensionality-in-library-sets)
     - [Deserialization](#deserialization)
       - [deserialization of .vo data not properly checked](#deserialization-of-vo-data-not-properly-checked)
+      - [rocqchk trusts the serialized VM bytecode segment](#rocqchk-trusts-the-serialized-vm-bytecode-segment)
   - [Probably non exploitable fixed bugs](#probably-non-exploitable-fixed-bugs)
       - [bug in 31bit arithmetic](#bug-in-31bit-arithmetic)
 
@@ -1168,6 +1169,28 @@ For instance `α` and `__U03b1_` were the same in the native compiler.
 - risk: can lead to segfaults or arbitrary code execution on crafted .vo files
     (files produced by coqc are fine)
 
+#### rocqchk trusts the serialized VM bytecode segment
+
+- component: rocqchk (trusts the vmlibrary segment of a .vo, and the code
+    descriptors stored in the declarations)
+- introduced: 8.20 (dedicated vmlibrary .vo segment, e6535d48bd)
+- impacted released versions: 8.20-9.3
+- impacted rocqchk versions: same, only with -bytecode-compiler yes
+- fixed in: 9.4 (fix pull request: rocq-prover/rocq#22353), by not reading the
+    vmlibrary segment at all and recompiling the bytecode of every constant from
+    the body being checked
+- found by: Claude Opus/Fable (fix by Archana Burra); reproducer by Jason Gross
+- GH issue number: rocq-prover/rocq#22352
+- exploit: two `rocq compile` builds of one constant differing only in its value
+    produce byte-identical opaques/summary segments, so splicing one .vo's library
+    onto the other's vmlibrary yields a well-formed file whose VM bytecode disagrees
+    with the typechecked body; a library compiled against that file can then hold a
+    VMcast that only typechecks because the compiler believed the bogus bytecode,
+    and rocqchk -bytecode-compiler yes accepted the resulting proof of False, with
+    no axioms reported
+- risk: proof of False accepted by rocqchk, but only with the non-default
+    -bytecode-compiler yes on a crafted .vo (files produced by `rocq compile` are fine)
+
 There were otherwise several bugs in beta-releases, from memory, bugs with beta versions of primitive projections or template polymorphism or native compilation or guard (e7fc96366, 2a4d714a1).
 
 ## Probably non exploitable fixed bugs

doc/changelog/01-kernel/22353-rocqchk-verify-vm-bytecode-Fixed.rst

@@ -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
+  recompiles the bytecode of every constant from the body it typechecks, so that
+  the code the VM runs and the checked body agree by construction; a crafted
+  ``.vo`` whose serialized bytecode disagreed with its body could previously make
+  a VM conversion prove ``False`` and still pass the checker
+  (`#22353 <https://github.com/rocq-prover/rocq/pull/22353>`_,
+  fixes `#22352 <https://github.com/rocq-prover/rocq/issues/22352>`_,
+  by Archana Burra and Jason Gross).

kernel/mod_declarations.ml

@@ -115,6 +115,9 @@ let module_body_of_type mtb =
 let set_implementation e mb =
   { mb with mod_expr = ModBodyVal e }
 
+let set_signature typ mb =
+  { mb with mod_type = typ }
+
 let set_algebraic_type mb alg =
   { mb with mod_type_alg = Some alg }
 

kernel/mod_declarations.mli

@@ -90,6 +90,10 @@ val functorize_module : (Names.MBId.t * module_type_body) list -> module_body ->
 val set_implementation : module_implementation -> module_body -> module_body
 val set_algebraic_type : module_type_body -> module_expression -> module_type_body
 
+val set_signature : module_signature -> 'a generic_module_body -> 'a generic_module_body
+(** Replace the expanded type, keeping the implementation and the algebraic
+    type. *)
+
 (** {6 Substitution} *)
 
 type subst_kind

kernel/modops.ml

@@ -208,6 +208,72 @@ let add_module mp mb env =
 let add_module_parameter mbid mtb env =
   add_module (MPbound mbid) (module_body_of_type mtb) env
 
+(** {6 Recompiling the VM bytecode of a module}
+
+    The checker does not trust the VM bytecode serialized in a [.vo] file, nor
+    the code descriptors [const_body_code] stored in the declarations: both are
+    attacker-controlled data the typechecker cannot validate. Instead it
+    recompiles the bytecode of every constant from the body it is about to
+    check, and records it in a table of its own, so that the code the VM runs
+    agrees with the checked body by construction. *)
+
+let push_bytecode vmtab code =
+  let open Vmemitcodes in
+  match code with
+  | BCdefined (mask, code, patches) ->
+    let vmtab, index = Vmlibrary.add code vmtab in
+    vmtab, BCdefined (mask, index, patches)
+  | (BCalias _ | BCconstant | BCuncompiled) as code -> vmtab, code
+
+let compile_constant_bytecode env vmtab cb =
+  let code =
+    Vmbytegen.compile_constant_body ~fail_on_error:false env
+      cb.const_universes cb.const_body
+  in
+  let vmtab, code = push_bytecode vmtab code in
+  vmtab, { cb with const_body_code = code }
+
+(* The environment is threaded exactly as in [add_structure], so that each
+   constant is compiled in the environment it is declared in. *)
+let rec compile_structure env vmtab mp res struc =
+  let fold (env, vmtab, accu) (lab, sfb) = match sfb with
+  | SFBconst cb ->
+    let c = constant_of_delta_kn res (KerName.make mp lab) in
+    let vmtab, cb = compile_constant_bytecode env vmtab cb in
+    Environ.add_constant c cb env, vmtab, (lab, SFBconst cb) :: accu
+  | SFBmind mib ->
+    let mind = mind_of_delta_kn res (KerName.make mp lab) in
+    Environ.add_mind mind mib env, vmtab, (lab, sfb) :: accu
+  | SFBmodule mb ->
+    let mp = MPdot (mp, lab) in
+    let vmtab, mb = compile_module_bytecode env vmtab mp mb in
+    add_module mp mb env, vmtab, (lab, SFBmodule mb) :: accu
+  | SFBmodtype mtb ->
+    let mp = MPdot (mp, lab) in
+    let vmtab, mtb = compile_module_bytecode env vmtab mp mtb in
+    Environ.add_modtype mp mtb env, vmtab, (lab, SFBmodtype mtb) :: accu
+  | SFBrules rrb ->
+    Environ.add_rewrite_rules rrb.rewrules_rules env, vmtab, (lab, sfb) :: accu
+  in
+  let (_ : env), vmtab, accu = List.fold_left fold (env, vmtab, []) struc in
+  vmtab, List.rev accu
+
+and compile_signature env vmtab mp res = function
+  | MoreFunctor (arg_id, mtb, body) ->
+    let vmtab, mtb = compile_module_bytecode env vmtab (MPbound arg_id) mtb in
+    let env = add_module_parameter arg_id mtb env in
+    let vmtab, body = compile_signature env vmtab mp res body in
+    vmtab, MoreFunctor (arg_id, mtb, body)
+  | NoFunctor struc ->
+    let vmtab, struc = compile_structure env vmtab mp res struc in
+    vmtab, NoFunctor struc
+
+and compile_module_bytecode : 'a. env -> Vmlibrary.t -> ModPath.t ->
+  'a generic_module_body -> Vmlibrary.t * 'a generic_module_body =
+  fun env vmtab mp mb ->
+  let vmtab, sign = compile_signature env vmtab mp (mod_delta mb) (mod_type mb) in
+  vmtab, set_signature sign mb
+
 (** {6 Strengthening a signature for subtyping } *)
 
 let strengthen_const mp_from l cb resolver =