Skip to content
Reverse Engineering
OCaml
Rocq - Coq

Rocq - Coq

Coq (now Rocq) is a proof assistant, and its compiled artifacts are not machine code at all: a .vo file holds the serialized terms of a development and the companion .glob file lists the names and cross-references. Reversing one means reading the inductive types and definitions, for example following a match that maps one constructor to another rather than disassembling instructions.

Inspecting a compiled module

Do not try to parse the binary .vo by hand (it is a marshalled OCaml structure). Instead, load it back into the toplevel and let Coq print the source-level terms.

  • Put the file on the load path and Require it, then Print its contents. The module name is the .vo filename, and -R/-Q maps the physical directory to a logical path.

    # coqtop (or rocqtop on recent versions). The .vo must be built with a
# compatible compiler version.
coqtop -R . Top
    Require Import Top.a.        (* a.vo *)
Print All.                   (* every inductive and definition of the module *)
Print myFunction.            (* a specific definition *)
Search _ (_ -> _).           (* find terms by type *)

  • The companion .glob file is plain text and lists every defined and referenced identifier with its kind and position. Read it directly to recover the names to Print, even when no source is available.

  • Other useful tools: coqchk typechecks a .vo standalone, SerAPI (sertop) serializes terms programmatically, and coq-dpdgraph draws the dependency graph between definitions.

Reading the logic as a graph

A definition that decides something is usually a match over the constructors of an inductive type. Read the body as a mapping from constructor to constructor and treat it as a directed graph:

  • the start is the constructor that is a source but never a target,
  • follow each edge until you reach the terminal (a success/identity case),
  • a decoy terminal is often present but never produced.

The constructor names along the path frequently spell the answer directly, so recovering the flag is just a matter of walking the chain in order.