santh-writ 0.1.1

CPU symbolic execution + exploit witness construction. Takes a weir-produced source→sink path and returns a concrete input that drives execution to the sink. Z3-backed.
docs.rs failed to build santh-writ-0.1.1
Please check the build logs for more information.
See Builds for ideas on how to fix a failed build, or Metadata for how to configure docs.rs builds.
If you believe this is docs.rs' fault, open an issue.

writ - CPU symbolic execution + exploit witness construction

Internal Santh tooling. writ is the symbolic-execution backend for surgec and depends on workspace-internal crates (weir, vyre). It is not published to crates.io and has no supported use outside the Santh workspace.

writ upgrades a Class 2 finding (path proven by weir) into a Class 1 finding (concrete exploit input that triggers the path). Z3-backed today; future backends (cvc5, bitwuzla) plug in behind the same WitnessProvider trait.

Architecture

weir::Path  +  SinkConstraintKind   →   WitnessRequest
                                        ↓
                                   WitnessProvider
                                        ↓
                          ┌─────────────┴─────────────┐
                          ↓                           ↓
                   writ::Z3Backend            scry::GpuBackend (future)
                   (CPU, libz3)               (GPU, vyre-native research)
                          ↓                           ↓
                   ConcreteInput               ConcreteInput
                          ↓                           ↓
                          └─────── Class 1 finding ───┘

writ is the CPU wrapper. The GPU equivalent (scry) lives in a separate crate so CPU primitives never leak into GPU code paths. Both satisfy the same trait; surgec is backend-agnostic.

Status

  • ✅ WitnessProvider trait surface
  • ✅ WitnessRequest / WitnessOutcome / ConcreteInput types
  • ✅ SinkConstraintKind enum (8 launch sink classes)
  • ✅ Z3Backend plumbing - opens solver, sets time budget
  • ⏳ Per-language statement→SMT encoders (one per language; lands in subsequent sessions)
  • ⏳ Sink-payload TOML library (one TOML per SinkConstraintKind)
  • ⏳ Input rendering (SMT model → curl command / argv / file content)
  • ⏳ Concolic fallback for paths exceeding the symbolic budget

Until the encoders land, Z3Backend::witness returns Unsupported(...) for every request. That is the truthful answer: the SMT plumbing is wired, the encoders are not. Surgec consults the outcome and keeps the Class 2 finding; future encoder additions upgrade existing paths to Class 1 without any rule changes.

Why CPU first

The library is real and ships in days, not quarters. GPU symbolic execution (scry) is a multi-quarter research project. We launch on writ; scry is a moat-extension that arrives later without changing the surface surgec consumes.

License

MIT - same as the rest of the Santh workspace.