Transition RESOLVE to new Facts and Reach format

Makefile

@@ -58,7 +58,7 @@ check-with-klee:
 	$(MAKE) check RESOLVE_BUILD_KLEE=ON
 
 test: configure
-	cmake --build $(RESOLVE_CMAKE_BUILD_DIR) --target test-CVEAssert test-libresolve test-reach-rs
+	cmake --build $(RESOLVE_CMAKE_BUILD_DIR) --target test-CVEAssert test-libresolve test-resolve-reach
 
 test-with-klee:
 	$(MAKE) test RESOLVE_BUILD_KLEE=ON

docs/components/facts.md

@@ -1,8 +1,46 @@
 # Facts
 
-Fact generation is a static program analysis technique that extracts structured information about a program from its source code or intermediate representation (i.e. [LLVM-IR](https://llvm.org/docs/LangRef.html)). A *fact* is a piece of information that describes some property of a program. Facts can be used to describe relationships between code and data. The `EnhancedFacts` pass plugin constructs program facts based on the program's control- and data-flow, and embeds these facts into custom ELF sections for downstream analysis.
+Facts are information about a program, extracted from [LLVM IR](https://llvm.org/docs/LangRef.html) at compile-time. Each fact describes a program node, property, or relationship. The collection of facts can form a Control Flow Graph, though they carry additional metadata beyond just that.
 
-These facts are compressed with zstd and stored inside a custom ELF section in the compiled binary called `.facts`. Reachability analysis can be performed by the [reach](reach.md) tool, which consumes these facts in its analysis. The [reachability example](../examples/reachability.md) walks through generating and querying facts end-to-end.
+[resolvecc](resolve-cc.md) will produce and embed facts into a `.facts` section inside the compiled ELF in a compact binary format, typically compressed with zstd.
 
-!!! note
-    Developed for easy parsing and to encourage compatibility with third party tools, the facts format can consume quite a bit of storage and memory, particularly when uncompressed, due to being text-based. 
+The [reach](reach.md) command consumes these facts from an ELF file, shared objcet, or an extracted `.facts` file. The [reachability example](../examples/reachability.md) shows a complete end-to-end example of this.
+
+## Binary Format Specification
+
+The binary format is typically compressed with zstd when it is attached to compiled objects. A zstd frame can be identified by the leading bytes: `28 B5 2F FD`.
+
+For definitive structure, consult the [Rust schema](https://github.com/riversideresearch/resolve/tree/main/resolve-facts/rs/src/schema.rs).
+
+The uncompressed facts stream has no top-level header. It contains one or more modules in sequence:
+
+```text
+Facts stream
+├── ModuleHeader (16 bytes)
+│   ├── version:         u32
+│   ├── node_count:      u32
+│   ├── edge_count:      u32
+│   └── string_pool_len: u32
+├── Node[node_count] (32 bytes each)
+│   ├── meta:          u32 (multiple bitmasks)
+│   ├── idx:           u32
+│   ├── name:          u32 (string offset)
+│   ├── opcode:        u32 (string offset)
+│   ├── source_line:   u32
+│   ├── source_col:    u32
+│   ├── source_file:   u32 (string offset)
+│   └── function_type: u32 (string offset)
+├── Edge[edge_count] (12 bytes each)
+│   ├── src:   u32 (NodeID)
+│   ├── dst:   u32 (NodeID)
+│   └── kinds: u32 (bitmask)
+├── String pool (string_pool_len bytes)
+│   └── repeated [byte length: u32][UTF-8 bytes ...]
+└── Next module, if present
+```
+
+A node ID is its index in the node array of its module. The `meta` field stores the node type, property flags, linkage, and call type.
+
+The `kinds` field is a bit set. One source and destination pair can have multiple relationships, such as `Calls`, `Contains`, or `ControlFlowTo`.
+
+The string pool has four-byte alignment. The writer adds zero padding after the final string when the pool requires it.

docs/components/reach.md

@@ -1,114 +1,96 @@
 # Reach
 
-`reach` performs static reachability queries on `resolve` program metadata. It consumes the [fact files](facts.md) extracted from binaries by `linker` and determines whether a path exists from the program entry point to a specified vulnerability. When a path is found, `reach` packages the results into a `.json` object and writes them either to a user-specified path or to `stdout` by default. 
+`resolve reach` determines whether a program entry point can reach a vulnerable function. It uses static control-flow data from RESOLVE facts.
 
-A Python wrapper, `reach.py`, provides a convenient command-line interface to interact with `reach`. For more information about `reach`, see the [`reach`](https://github.com/riversideresearch/resolve/tree/main/reach) documentation.
+The command accepts facts from these sources:
 
-!!! tip
-    For a hands-on, end-to-end walkthrough of a reachability query, see the [reachability example](../examples/reachability.md).
+- An ELF executable or shared library that contains a `.facts` section.
+- An extracted `.facts` file.
+- A directory that contains one or more `.facts` files.
+- Multiple inputs through repeated `-f` arguments.
 
-## Developer Information
+The command writes one JSON result for each entry in `vulnerabilities.json`.
 
-### Run
+## Use the command
 
+```bash
+resolve reach \
+  --input vulnerabilities.json \
+  --facts program.facts \
+  --output reach.json
 ```
-cmake -B build && cmake --build build/
-./build/reach --help
-```
 
-### Description
+The command uses `main` as the default entry point. Use `--entry` to select a different function.
+
+```bash
+resolve reach -i vulnerabilities.json -f program.facts -e service_main
+```
 
-This development is factored into a library part (under `lib/`) and an
-executable tool (under `src/`) that uses the library.
+If you omit `--output`, the command derives the path from the input name. For example, `vulnerabilities.json` produces `vulnerabilities.reach.json`.
 
-See the `--help` output for command line arguments/options.
+Use `--src` to read a package version from a Vcpkg manifest. The result becomes unreachable when the installed version is outside the vulnerable range.
 
-The minimum required arguments for performing a reachability query are
-`--facts_dir` (path to directory containing facts files extracted from
-the program binary), and the `--src` and `--dst` node IDs. The tool
-will construct a control-flow graph from the facts in `facts_dir`, and
-attempt to find the shortest path from `src` to `dst` in it.
+## Dynamic-link analysis
 
-The `src` and `dst` node IDs should match how they appear in the facts
-files, which is determined by the [**RESOLVE** LLVM
-pass](https://github.com/riversideresearch/resolve/blob/main/resolve-cc/src/ResolveFactsPluginPass.cpp)
-that generates the facts.
+Use `--dynlink` to include compatible external-linkage functions as indirect-call targets.
 
-For example, if `nodeprops.facts` contains the following line:
+```bash
+resolve reach -i vulnerabilities.json -f program.facts --dynlink
 ```
-/src/guestbook/src/main.cpp:f_GLOBAL__sub_I_main.cpp,Function
+
+Use `--dlsym-log` with `--dynlink` to restrict those targets to observed symbols.
+
+```bash
+resolve reach \
+  -i vulnerabilities.json \
+  -f program.facts \
+  --dynlink \
+  --dlsym-log dlsym.json
 ```
-there is a node of type `Function` with ID
-`/src/guestbook/src/main.cpp:f_GLOBAL__sub_I_main.cpp`.
 
-Arguments can also be specified in an input JSON file instead of as
-command line arguments. See the `--input` argument. If an argument is
-provided in both the input file and at the command line, the command
-line argument takes precedence. The input file format is specified by
-the struct `config` in `src/config.hpp` (the JSON deserializer is
-auto-generated from this definition).
+The log has this structure:
+
+```json
+{
+  "loaded_symbols": [
+    {
+      "symbol": "plugin_entry",
+      "library": "libplugin.so"
+    }
+  ]
+}
+```
 
-The input file format supports multiple queries (see struct `query`
-and the `queries` field of struct `config` in `src/config.hpp`).
+The graph matches the `symbol` value. The `library` value remains available for future matching changes.
 
-### Architecture
+## Architecture
 
-The implementation is organized roughly as follows:
+The Rust command owns input parsing, function lookup, version comparison, and report generation. It calls `libreach` through a small C interface.
 
 ```mermaid
-graph LR;
-    A[/input.json<br>cmd args/]-.->B;
-    B[main.cpp]-->C;
-    C[[facts.hpp]]-->|facts database|D;
-    D[[graph.hpp]]-->|constructed graph|E;
-    E[[search.hpp]]-->|discovered paths|B;
+graph LR
+    A[vulnerabilities.json] --> B[resolve-reach]
+    F[ELF or binary facts] --> B
+    B --> C[libreach]
+    C --> B
+    B --> O[reachability report]
+```
+
+The command loads all facts once. Then it builds one graph and uses that graph for all unresolved sinks.
+
+## Developer commands
+
+Build the command:
+
+```bash
+cmake -B build
+cmake --build build --target resolve-reach
+```
 
-    F[(nodes.facts<br>nodeprops.facts<br>edges.facts)]-.->C;
+Run its existing tests:
 
-    B-.->O[/output.json/]
+```bash
+cmake --build build --target test-resolve-reach
 ```
 
-The main reads the input config (plus command line arguments), and
-then uses the functionality declared in `lib/facts.hpp` to load the
-facts files from the disk into an in-memory database. This database is
-used by `lib/graph.hpp` to build a graph, which is passed to
-`lib/search.hpp` for finding paths. Finally, the paths are packaged
-into a JSON object and written to the provided output path or to
-stdout if no path was given.
-
-### Code
-
-Under `lib/`:
-
-- facts.hpp, facts.cpp
-    - in-memory representation of fact databases, and loading from .facts files
-    - defns related to dlsym loaded symbol logs from dynamic analysis
-- graph.hpp, graph.cpp
-    - weighted directed graphs with integer node labels, and functions
-    for constructing them from facts databases
-    - `handle_map`s for mapping between string node IDs and their
-    integer labels (handles)
-- search.hpp, search.cpp
-    - pathfinding algorithms on graphs. Currently:
-        - BFS
-	    - Dijkstra's shortest path
-	    - Yen's K-shortest paths
-    - also computing distance maps for KLEE (min distance of each node
-    in the graph to a specified destination node)
-- util.hpp
-    - misc helper functions
-        - `at` function for vector and unordered_map with slightly better
-      error reporting
-	    - `time` function for measuring time to execute a given function
-- distmap.hpp, distmap.cpp
-    - compute distance maps and blacklists for directed KLEE
-
-Under `src/`:
-
-- config.hpp
-    - specifications of the tool's input and output formats as structs
-    - JSON serializers and deserializers are auto-generated from these
-    specifications via the Lohmann JSON library
-- main.cpp
-    - parse arguments, load facts, build graph, perform queries, output
-    results
+See the [reachability example](../examples/reachability.md) for a complete workflow.

docs/examples/reachability.md

@@ -23,18 +23,15 @@ We want to ask **RESOLVE**: starting from `main`, can execution actually reach `
 
 ## A Vulnerability Specification
 
-First, describe the vulnerability we want to analyze in a JSON file (let's call it [`vulnerabilities.json`](../concepts/vulnerabilities-json.md) on disk). Each entry in the array is a *sink* (a function we would like to try to reach). All of the following fields are required, and will be fed-through into our final report:
+First, describe the vulnerability in a [`vulnerabilities.json`](../concepts/vulnerabilities-json.md) file on disk. Each entry identifies one affected function, which is called a sink.
 
 ```json
 {
     "vulnerabilities": [
         {
             "cve-id": "CVE-0000-00000",
-            "cve-description": "Null pointer dereference reachable from the program entry point.",
             "package-name": "reachability-example",
             "package-version": "vers:generic/*",
-            "cwe-id": "476",
-            "cwe-name": "NULL Pointer Dereference",
             "affected-function": "do_npd",
             "affected-file": "main.c"
         }
@@ -53,34 +50,26 @@ Reachability analysis runs on program *facts* (see: [RESOLVE facts](../component
 resolvecc main.c -o main
 ```
 
-## Extracting the Facts
-
-Next, pull the embedded facts back out of the binary into a `main.facts` file with `resolve get-facts`:
-
-```bash
-resolve get-facts -i main
-```
-
-This writes `main.facts` (alongside a compressed `main.facts.zst`) into the current directory.
-
 ## Running the Reachability Query
 
-Now we have everything [`resolve reach`](../components/reach.md) needs: the vulnerability specification and the facts. Point it at both and choose an output path for the report:
+[`resolve reach`](../components/reach.md) reads embedded facts directly from the compiled ELF. Pass the path of the program and select an output file:
 
 ```bash
-resolve reach -i vulnerabilities.json -f main.facts -o out.json
+resolve reach -i vulnerabilities.json -f main -o out.json
 ```
 
 !!! tip
     If your entry point is not `main`, pass `-e <function>` to `resolve reach`. For projects with a vcpkg source tree, pass `-s <src-dir>` so the report can additionally check whether the pinned package version falls in the vulnerable range.
 
-`resolve reach` locates the entry point (`main` by default), locates each sink in the facts, and searches the control-flow graph for a path between them. Along the way it prints what it found:
+!!! note
+    If you need a separate facts file, use `resolve get-facts -i main`. This command writes `main.facts` and `main.facts.zst`. You can pass `main.facts` to `resolve reach`.
+
+`resolve reach` locates the entry point and each sink. Then it searches the control-flow graph for a path.
 
 ```txt
-Found function 'main' in module 'src/main.c'
-Found function 'do_npd' in module 'src/main.c'
-[RW]: Invoking reach 'reach -f main.facts -i reach_wrap_input.json -o reach_wrap_output.json'
-[RW]: Wrote out.json.
+[REACH] Loaded 1 facts modules from 1 input files.
+[REACH] Built a libreach graph with 3 edges.
+[REACH] Wrote 'out.json'.
 ```
 
 ## Interpreting the Report
@@ -97,24 +86,24 @@ The report in `out.json` classifies each sink and, when it is reachable, spells
                 "conclusion": "Statically Reachable",
                 "reason": "Control Flow Graph analysis found the following candidate path...",
                 "call_path": [
-                    "Function(main) ((1556769911, 9))",
-                    "DirectCall -> Function(do_npd) ((1556769911, 1))"
+                    "Function(main) ((0, 9))",
+                    "DirectCall -> Function(do_npd) ((0, 1))"
                 ],
                 "control_flow_path": [
-                    "Function(main) ((1556769911, 9))",
-                    "Contains -> BasicBlock() ((1556769911, 10))",
-                    "DirectCall -> Function(do_npd) ((1556769911, 1))"
+                    "Function(main) ((0, 9))",
+                    "Contains -> BasicBlock(0) ((0, 10))",
+                    "DirectCall -> Function(do_npd) ((0, 1))"
                 ]
             }
         }
     ]
 }
 ```
 
-The `call_path` is the human-readable answer: `main` makes a `DirectCall` to `do_npd`, so the vulnerability is reachable. The `control_flow_path` is the same route at basic-block granularity.
+`call_path` gives an exact answer here: `main` makes a `DirectCall` to `do_npd`, so the vulnerability is statically reachable! The `control_flow_path` is the same route at basic-block granularity.
 
 !!! note
-    The classification is **potentially reachable (statically reachable)**, not **explicitely exploitable**. Reachability analysis only proves that a path exists in the control-flow graph; it does not prove a concrete input can drive execution down that path. Producing such an input is the job of [input synthesis](input-synthesis.md).
+    The classification is **potentially reachable (statically reachable)**, not **explicitly exploitable**. Reachability analysis proves that a control-flow path exists. It does not prove that a concrete input can use that path. [Input synthesis](input-synthesis.md) produces such an input.
 
 ### Other Classifications
 
@@ -126,17 +115,14 @@ Depending on what `resolve reach` finds, a sink can come back as:
 | `unreachable` | Not Reachable | The function exists in the program, but no path reaches it from the entry point. |
 | `unreachable` | Not Found | The affected function was not found in the compiled program metadata (e.g. it was inlined, dead-code eliminated, or never linked in). |
 
-## TDLR (Quick Reference)
+## TLDR (Quick Reference)
 
 Given source code, you can run a reachability query with:
 
 ```bash
 resolvecc main.c -o main
-resolve get-facts -i main
-resolve reach -i vulnerabilities.json -f main.facts -o out.json
+resolve reach -i vulnerabilities.json -f main -o out.json
 ```
 
 !!! tip
     Once a path is confirmed, synthesize a concrete triggering input with input synthesis (above), or instrument a fix at compile time with [remediation](remediation.md).
-
-

examples/misc/eboss_eval/src/analyze-images/compose-analyze-image.yml

@@ -92,7 +92,6 @@ services:
       /opt/resolve/bin/resolve-reach \
       -i /challenge/vulnerabilities.json \
       -o /facts-dir/reach_out.json \
-      -f /facts-dir/build/ \
-      -r /opt/resolve/bin/reach
+      -f /facts-dir/build/analyze-image.facts
       "
     depends_on: [server-remediated]

examples/misc/openssl.sh

@@ -11,7 +11,7 @@ set -e
 SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
 REPO_ROOT="$(cd "$SCRIPT_DIR/.." && pwd)"
 EXTRACT_FACTS_SCRIPT="/opt/resolve/bin/extract_facts.py"
-REACH_WRAPPER="/opt/resolve/bin/resolve-reach"
+REACH_COMMAND="/opt/resolve/bin/resolve-reach"
 
 export CC="/usr/bin/clang"
 export CXX="/usr/bin/clang++"
@@ -50,11 +50,10 @@ mkdir openssl_facts
 # Run reach analysis
 # -------------------
 echo "[+] Running reachability analysis." 
-"$REACH_WRAPPER" \
+"$REACH_COMMAND" \
     -i openssl_vulnerabilities.json \
     -o openssl_reach_out.json \
     -f openssl_facts/libcrypto.facts \
-    -e "CMS_RecipientInfo_decrypt" \
-    -r /opt/resolve/bin/reach
+    -e "CMS_RecipientInfo_decrypt"
 
 # TODO: Add remediation portion check for exit code 3 for successful remediation