## https://sploitus.com/exploit?id=CABE69E8-A0DC-5D30-94EE-387793C24681
# exploit-counter
[](https://github.com/nickharris808/exploit-counter/actions/workflows/ci.yml)
[](https://pypi.org/project/exploit-counter/)
[](https://pypi.org/project/exploit-counter/)
[](LICENSE)
**Turn "we found no escapes" into an exact integer.**
"We fuzzed it and found nothing" is unfalsifiable, and everyone in the room knows it. It is equally
consistent with *the guard is correct* and *we did not look hard enough*. This package replaces that
sentence with a number:
> Weakening this guard admits **exactly 509** states the safety property forbids โ a per-draw hit
> probability of 0.0078, so a uniform fuzzer needs ~129 draws to find one.
```
pip install exploit-counter
```
## 30-second quickstart
The examples ship inside the package, so this works immediately after `pip install` โ no repository
checkout needed:
```bash
exploit-counter demo
```
```
exploit-counter demo -- CVE-2014-0160 (Heartbleed) shape
safety: 3 + payload = 95%
```
The interval is **Clopper-Pearson**, deliberately, over the faster normal-approximation intervals.
It is conservative in coverage: it over-covers, so the true count falls inside at least as often as
the stated confidence. For a risk figure a decision depends on, over-covering is the correct
direction to fail. A Wald interval is tighter and wrong near zero โ exactly the regime a security
count lives in.
The zero-hit case is handled exactly rather than reported as zero: 0 hits in *n* draws gives an
upper bound of `1 - (alpha/2)^(1/n)`. "We sampled and saw nothing" produces a real bound, not a claim
of absence.
Sampling is seeded and deterministic, so a published figure reproduces.
## Honest scope
- **Sampling cannot establish a zero.** `is_sound_guard` returns `None`, not `False`, when only a
bracket is available. Do not coerce it.
- **Multi-conjunct safety properties are upper-bounded, not exact.** Regions may overlap; the counter
sums them, which over-counts. Over-counting never reports a smaller attack surface than exists. The
single-conjunct case โ which is most real guards โ is exact.
- **This is a triggerability count under a uniform sampling model.** It is not CVSS, not impact, and
not a claim that any counted state is exploitable in the weaponised sense. It bounds *reachability
of a forbidden state*, which is a floor on badness, not a severity score.
- **The count is only as meaningful as the domain you declare.** An unbounded variable has no finite
model count; `box_from_atoms` will not invent bounds for you.
## API
| Function | Purpose |
|---|---|
| `over_acceptance(domain, guard, safety, box)` | how many states the guard wrongly admits |
| `count_conjunction(atoms, box)` | exact model count, or `None` if over the cap |
| `count_models(atoms, box)` | `(exact, None)` or `(None, bracket)` โ never both |
| `monte_carlo_count(atoms, box)` | sampled count with a Clopper-Pearson bracket |
| `clopper_pearson(k, n, alpha)` | the exact binomial interval on its own |
| `box_from_atoms(vars, domain)` | derive integer bounds from single-variable atoms |
## Relationship to certkit
Atoms come from [`certkit`](https://github.com/nickharris808/certkit), which also defines the certificate format and the
independent checker. The division is deliberate: `certkit` answers *is this guard sound?* and
`exploit-counter` answers *if not, by exactly how much?* They share one atom type so a spec written
for one works with the other unmodified.
## Tests
```bash
pip install -e ".[dev]"
pytest
```
37 tests. The exact leg is checked against brute-force enumeration on every shape small enough to
enumerate โ if the closed form and the enumeration disagree, the closed form is wrong. The
Clopper-Pearson coverage property is verified by simulation rather than asserted.
---
## The closed core
These packages are the *checking* half. They deliberately contain no proof search, which is what keeps
them small enough to audit โ and it means something upstream has to produce certificates.
For obligations over full machine-word domains, enumeration does not scale and a decision procedure
that does not enumerate is required: solver-free elimination emitting replayable certificates. That
engine, the repair synthesiser that derives a minimal guard from a refutation, and the evolutionary
search that drives them are **not** in this repository and are available commercially.
The split is deliberate and permanent. **The checker is free and always will be** โ a certificate you
cannot independently verify is worth nothing, so charging for verification would defeat the format.
What costs money is *producing* certificates at scale.
## License
Apache-2.0.