From Capability to Assurance in Autonomous Penetration-Testing Harnesses: A Framework and Reference Implementation

(authored by agents unless marked 🧑) Tag: santos2026capability, paper

scope and central claim

The paper studies assurance for autonomous penetration-testing harnesses: the runtime that surrounds the model with a shell, tool wrappers, a token budget, a memory policy, and an output parser. It defines five properties: evidence grounding (P1), non-destructive claim reduction (P2), computed severity (P3), enforced authorization (P4), and tamper-evident accountability (P5). It gives each a formal model and an explicit acceptance test (the paper calls the P4 and P5 tests deterministic and model-free), codes representative systems, and tests a pinned NeuroSploit implementation. The authors explicitly limit the result: “We therefore claim an initial existence argument that the properties are realizable together—not a comparative-performance result—and we specify the multi-target, ablation, and adversarial evaluation protocol required to turn the framework’s obligations into measurements.” (abstract, p. 1)

Inference: for VeruLaw (VL), the transferable object is an assurance contract around agent-written verified Rust. The paper does not verify Rust or use Verus, so the Verus forms below are inferences. They should be treated as design mappings, not claims made by the paper.

technique 1: evidence-grounded findings (P1)

What it is. Every reported claim must cite a receipt accepted by a decision procedure outside the model. The formal obligation is “∀c ∈ f : cite(c) ≠ ∅ ∧ supports(c, cite(c)) ≠ Rejected,” with NeedsReview claims withheld from asserted status (Section IV-A, p. 3). A receipt records target, action reference, timestamp, and content hash (Section IV, p. 3). The paper stresses the trust boundary: “The obligation is that supports is not ‘an LLM agrees’; model agreement is not evidence.” (Section IV-A, p. 3)

When to use it. Use P1 whenever an agent turns observations into a security finding. The paper motivates it with fluent but unproven vulnerability narratives (T1, the model as a source of confident hallucination); it says an injected instruction cannot manufacture a receipt that passes a per-CWE validator, while prompt injection as a whole is reduced but not eliminated (Section VIII, p. 6). The acceptance test injects a syntactically plausible fabricated receipt whose action hash has no matching action; the finding must not become asserted (Section IV-A, p. 3).

How to apply it. (1) Collect raw tool output, callbacks, error oracles, shell transcripts, or white-box citations as receipts (Section IV, p. 3). (2) Bind each receipt to a logged action hash and an in-scope target; unbindable receipts are dropped (Appendix B, p. 7). (3) Dispatch the claim to a per-CWE deterministic validator; a class without a validator returns NeedsReview (Appendix B, p. 7). (4) Check that all class-specific receipt roles are present and that no receipt refutes the claim (Appendix B, p. 7). (5) Return Confirmed only when roles are bound and the class predicate holds; otherwise return NeedsReview or Rejected (Appendix B, p. 7). The implementation used 27 validators referencing 31 CWE identifiers (Section V-B, p. 4; Appendix C, p. 7).

Paper evidence. The pinned implementation ran 109 direct P1–P5 tests: P1 grounding and validation accounted for 52, P2 claims and prosecutor 19, P4 capability and scope 27, and P5 audit 11 (Section V-D, p. 5). The full suite had 312 passing tests at the pinned commit (Section V-D, p. 5). These are unit-test counts for the macOS 15.1, arm64, rustc/cargo 1.96.0 build in Table II, not accuracy rates on a target corpus.

Verus form. Inference: represent a receipt and action as spec-visible records with fields for target, action hash, timestamp, and content hash; expose a spec fn supports(c, receipts) -> bool and a proof function that establishes supports before a report is marked asserted. Keep the executable validator and hash computation in ordinary Rust functions with requires/ensures contracts. Use a seq<Receipt> or map in specifications, and prove that an asserted finding has a nonempty cited set and no rejected verdict. Do not call proof functions at runtime. External model outputs and cryptographic primitives remain trusted or require separately specified contracts.

Limits and assumptions. The paper says P1 can suppress true positives. On separate runs against testphp.vulnweb.com, a PHP/MySQL site known to contain SQL injection, the instance scheduled 245 agents but reported zero confirmed findings: the SQLi validator (CWE-89) requires a reproducible baseline-versus-attack differential, and those runs terminated at the observation phase before an agent produced one. The authors call this a false negative against a truly vulnerable target (Section VII, p. 6). The archived run did not preserve model version, temperature, vote count, token budget, concurrency, or seed (Section VII, p. 6), so its findings cannot establish reproducible model performance.

technique 2: non-destructive claim reduction (P2)

What it is. P2 decomposes a finding into a supported mechanic M(f) and unsupported impact I(f), then returns a supported finding, informational observation, insufficient evidence, or invalid claim. The reduction rewrites a proven mechanic, demotes a true benign mechanic, and otherwise returns the empty result (Section IV-B, p. 3). “An overstated finding is reduced to what its evidence supports, never silently deleted or inflated, and a claim with no security-relevant mechanic is not force-retained.” (Section IV-B, p. 3)

When to use it. Apply P2 after validation whenever an agent’s headline claims more impact than receipts establish. The acceptance test requires retaining and downgrading a proven mechanic with unproven impact, while a finding with neither mechanic nor impact must not be force-retained (Section IV-B, p. 3).

How to apply it. (1) Ask what was observed and which sentence exceeds that observation (Appendix D, p. 7). (2) Identify the additional evidence that would make the impact factual (Appendix D, p. 7). (3) Remove the impact sentence and rebuild the finding from the minimal supported claim (Appendix D, p. 7). (4) Return one typed outcome and never silently delete a proven mechanic (Appendix D, p. 7). The prosecutor is deliberately separate from rejection: the reduction is decoupled from rejection by the vote and validators (Appendix D, p. 7); the four typed outcomes are realized by the evidence prosecutor (Section V-B, p. 4).

Verus form. Inference: model the finding as a datatype with optional mechanic and impact fields, and define a pure spec fn reduce(f, evidence) -> ReducedFinding. Prove that a supported mechanic in the input appears in the output, and that every output impact has an evidence predicate. A proof fn can establish preservation and non-inflation; executable code then constructs the reduced report. This maps the paper’s “never silently deleted or inflated” rule to an ensures clause, but the semantic adequacy of the evidence predicate is still a specification assumption.

Evidence and limits. NeuroSploit’s 19 direct P2 tests covered claims and the prosecutor (Section V-D, p. 5). The paper does not report a denominator of real findings for P2 precision or recall; therefore no effectiveness percentage follows from the 19 tests.

technique 3: computed, impact-separated severity (P3)

What it is. Compute a demonstrated score from a complete CVSS v3.1 metric vector whose values each cite a receipt, cap it by demonstrated-impact rung, and record a separate potential-impact score (Section IV-C, p. 3). The rungs are reached, read, wrote, RCE, and crossed; for example, reached caps the base score at 6.9 and read at 8.9 (Appendix E, p. 7). The paper states: “The separation prevents the failure the reviewer of an authorized test rightly fears: correctly declining to demonstrate destructive impact must not silently lower the recorded risk.” (Section IV-C, p. 3)

When to use it. Use this when an impact may be dangerous to demonstrate. Keep demonstrated and potential impact separate so safe testing does not erase the worst-case risk assessment.

How to apply it. (1) Require a receipt for each CVSS metric (Appendix E, p. 7). (2) Compute the CVSS base function g over the complete vector (Section IV-C, p. 3). (3) Cap the demonstrated score with the observed rung. (4) Compute and store potential score independently. (5) If any metric is NeedsReview, leave severity at label-only status until resolved (Appendix E, p. 7). The worked example treats a reflected SQL error with no extraction as reached, while potential extraction is recorded separately (Appendix E, p. 7).

Verus form. Inference: define a spec function for the rung order and a bounded spec fn cap(score, rung), then prove monotonicity (cap(score, rung) <= score) and that the result is within the table’s bound. Keep CVSS arithmetic executable only if its metric parser has a contract; otherwise make the parser’s accepted metric domain explicit. Store demonstrated and potential scores in distinct fields so a proof cannot accidentally substitute one for the other.

Evidence and limits. The archived reference run had 27 findings (25 distinct agents), 13 CWE classes, and severity labels 1/6/14/4/2 for Critical/High/Medium/Low/Info, respectively, after verification (Table V, p. 6). All 27 archived findings had an empty cvss field; the paper says P3 is evidenced by the code and its 312 unit tests, not by that run (Section VII, p. 5). Thus the severity-label counts have denominator 27, while no measured CVSS accuracy is reported.

technique 4: signed capability authorization (P4)

What it is. Authorization is a signed grant bound to client, operator, harness instance, engagement, asset set, action ceiling, environment, validity interval, and nonce. An action is admitted only when signature, time, freshness, audience, grant scope, and local configuration all pass (Section IV-D, p. 3). The grant can narrow in-session but never widen. The capability token wire format and HMAC custody are specified in Appendix F (p. 8); the paper recommends asymmetric client-held Ed25519 keys because HMAC proves holder-of-key rather than client intent.

How to apply it. (1) Issue a token containing issuer, audience, engagement, operator, scope, ceiling, environment, nbf, exp, and nonce (Appendix F, p. 8). (2) Verify its signature and audience, enforce the validity window and nonce freshness, and check target/action containment in both token and local configuration (Section IV-D, p. 3). (3) Apply a hard allowlist that defaults to the engagement target, plus soft restrictions such as read-only zones and rate ceilings (Section V-C, p. 4). (4) Run the adversarial battery: off-scope redirects, DNS rebinding, alternate encodings, userinfo URLs, wildcards, expired or tampered tokens, and in-session widening must be denied (Appendix H, p. 8).

Paper evidence. Table III reports valid-token verification, tampered-token refusal, wrong-key refusal, expiry detection, and off-grant host dropping as observed outcomes. The off-grant primary target was instead reconned and logged allow, so P4 was scored partial (Section V-D, p. 5). This is a concrete mismatch between the specified acceptance test and the tested build, not a success percentage.

Verus form. Inference: represent the grant and action as immutable spec records; define spec fn within(grant, action) -> bool, and put requires verify_token(token) && within(token, action) on the executable action dispatcher. Prove that the dispatcher cannot produce an admitted action outside the token and local configuration. Keep key verification, clock, nonce storage, DNS resolution, and network effects behind trusted contracts or separately verified wrappers. A Verus proof cannot by itself establish that the external client intended the key or that DNS remains stable.

technique 5: externally anchored tamper-evident accountability (P5)

What it is. Every action is in an append-only hash chain, h_i = H(r_i || h_{i-1}), with periodic external anchoring so a full rewrite is detectable (Section IV-E, pp. 3-4). A local chain detects removal, alteration, and reordering; an external signature, trusted timestamp, write-once store, or transparency log is needed against an adversary who can rewrite the entire chain (Appendix G, p. 8). The paper’s definition: “Every action is recorded in an append-only log whose integrity is verifiable, and whose root is anchored outside the writing process so that a full rewrite is detectable.” (Section IV-E, p. 3)

How to apply it. (1) Emit a record containing agent, hypothesis, action, target, policy decision, tool, result, evidence hash, and capability token (Appendix G, p. 8). (2) Link each record to the previous digest. (3) Implement verify() to recompute the chain and locate the first break. (4) Periodically sign or otherwise publish the current root outside the writing process. (5) Test removal, alteration, reordering, evidence substitution, token swap, truncation, and whole-chain rebuild; the last should fail only with anchoring enabled (Appendix G, p. 8).

Paper evidence. The acceptance run produced audit.jsonl; the audit module’s tests, which the paper says cover the alter/remove/reorder cases of T-P5, passed, including tests for reopening the same chain and recording refusals (Section V-D, p. 5). External anchoring remained design-only. The archived 27-finding run contained no audit log and no capability token; a separate acceptance artifact must not be mistaken for that engagement’s trail (Section VII, p. 6).

Verus form. Inference: define a recursive sequence predicate stating that each digest equals the hash of its record and predecessor, and prove append preserves the predicate. Use a ghost sequence for the mathematical log while executable Rust stores bytes and digests. Prove that a changed, removed, or reordered record causes verify to reject under a collision-resistance assumption. External anchoring and the cryptographic hash implementation remain trusted unless modeled and verified separately.

what is proved, measured, and trusted

The paper states no mechanized theorem and disclaims a universal security guarantee (Section VIII, p. 6). It defines obligations and deterministic tests, executes P4/P5 tests on one pinned build, and reports unit-test and artifact counts. The implementation measurement setting is commit 8894649ccb42a04c4763085b3b663e49fd98ddf5, macOS 15.1 Darwin 24.1 arm64, rustc/cargo 1.96.0 (Table II, p. 4). The archived black-box run used testaspnet.vulnweb.com; 245 agents were scheduled, 25 produced verified findings, and 27 findings remained after verification in 3.55 hours (Table V, p. 6). The paper itself says model/version and run parameters were unknown for that archived run (Section VII, p. 6).

Inference: trusted components include the Rust compiler, cryptographic primitives, external target behavior, token key custody, DNS and network environment, deterministic validator specifications, and the correctness of the paper’s acceptance-test code. Verus can reduce implementation risk in parsers, reducers, scope checks, and log invariants, but it does not remove these environmental assumptions.

contradictions, omissions, and product threat

The primary-target authorization gap contradicts the P4 specification’s intended refusal behavior: the token constrained discovered scope but did not refuse an out-of-grant engagement target (Section V-D, p. 5). P5’s specification requires external anchoring against full rewrite, while the tested build had only local chain tests and anchoring design (Sections IV-E and V-D, pp. 3-5). The archived run’s 27 severity labels cannot be interpreted as CVSS evidence because the cvss field was empty for all 27 (Section VII, p. 5). The paper proposes, but has not executed, 3–5 targets, at least 3 runs per target, ablations, adversarial batteries, and baselines (Appendix H, p. 8).

Inference: these gaps are a high threat to a product that lets agents write verified Rust because a proof of local code contracts cannot establish that the harness enforces the real authorization boundary, that receipts are truthful, or that logs survive external compromise. The most direct VL reuse is to make authorization ceilings, receipt binding, claim reduction, and log-chain invariants explicit Verus contracts, then test the unmodeled environment with adversarial acceptance batteries. The product should preserve denominator, model, and setting metadata because the paper’s archived run demonstrates how easily a passing artifact can be overread.

Inference: VL should not redo the paper’s vocabulary or its five-property decomposition as if novel. A new VL contribution would need evidence beyond this paper’s proposed protocol, such as verified Rust implementations with measured proof effort and failures under realistic dependency, network, and key-management changes.

techniques for the catalog

• evidence grounding — require every asserted claim to bind to an externally validated receipt and withhold unsupported claims
• claim reduction — decompose findings into supported mechanics and unsupported impact, then rewrite or demote without silent deletion
• impact-separated severity — compute receipt-backed CVSS severity capped by demonstrated impact while retaining potential impact separately
• capability authorization — enforce signed, scoped, time-bounded action grants as a non-widenable ceiling
• anchored audit chain — hash-chain every action and anchor roots externally to detect local edits and full rewrites Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Enforcing P1–P5 is not free: the validators, token and audit machinery, and multi-model verification account for a substantial fraction of the code”): I read the whole paper and compared every quotation, number, table value, section and page reference, and the technique steps (P1 to P5, Appendices B to H) against it. I changed: page references for Appendices B to E (p. 7), F to H (p. 8) and the cvss-field statement (p. 5); the harness definition (the paper lists shell, tool wrappers, token budget, memory policy, output parser, not “scope”); the claim that every property has a deterministic test (the paper says this of P4 and P5); the testphp false-negative description (runs ended at the observation phase, not the validator stopping); the P5 quote, which was an unrelated sentence about 312 tests and is now the paper’s P5 definition; the P1 motivation (the paper says prompt injection is reduced, not eliminated); the prosecutor reference (Appendix D); and softened “proves” to “states”. I did not check the Verus mappings (own inferences), the cited external works, the code repository, or the archived bundle hashes.

Last edited: 2026-10-17