Commit Graph
1113 Commits
Author SHA1 Message Date
Marius Ciepluch 09c3ffd621 feat(access-control-prover): 11.4 verify and promote proposed target knowledge 2026-10-29 20:34:52 +01:00
Marius Ciepluch c0e1360149 feat(access-control-prover): 11.3 extract existing target knowledge into candidate records 2026-10-29 20:29:15 +01:00
Marius Ciepluch c279513def feat(access-control-prover): 11.2 generic call-site registration strategy 2026-10-29 20:23:50 +01:00
Marius Ciepluch 86709daf2e feat(access-control-prover): 11.1 entry-recognition strategy registry 2026-10-29 20:19:31 +01:00
Marius Ciepluch 82e4a1ad97 feat(access-control-prover): 10.6 three-way judgments in the prover 2026-10-29 19:34:44 +01:00
Marius Ciepluch 95dfddb018 feat(access-control-prover): 10.5 multi-path aggregation in the opt-in abstract mode 2026-10-29 19:20:24 +01:00
Marius Ciepluch f700b99637 feat(access-control-prover): 10.4 one judgment per path 2026-10-29 19:17:37 +01:00
Marius Ciepluch 7eb491dc82 feat(access-control-prover): 10.3 authority matching through promoted implications 2026-10-29 19:11:30 +01:00
Marius Ciepluch cf60e02804 feat(access-control-prover): 10.2 witness kind, scope and resource matching 2026-10-29 19:05:51 +01:00
Marius Ciepluch 8ad304ffeb feat(access-control-prover): 10.1 abstract dominance relations without prover fallback 2026-10-29 19:01:25 +01:00
Marius Ciepluch f23d3f986d feat(access-control-prover): 9.4 exact evidence paths from summaries 2026-10-29 18:46:41 +01:00
Marius Ciepluch 06d5363ce2 feat(access-control-prover): 9.3 summary caches and explicit exploration cutoffs 2026-10-29 18:37:06 +01:00
Marius Ciepluch c237626f7a feat(access-control-prover): 9.2 monotone summaries over recursive call components 2026-10-29 18:30:18 +01:00
Marius Ciepluch fffa3e0002 feat(access-control-prover): 9.1 local function summaries 2026-10-29 18:25:23 +01:00
Marius Ciepluch 2466670ba3 feat(access-control-prover): 8.4 inheritance and base-declaration attachment through repo-defined descendants 2026-10-29 16:10:44 +01:00
Marius Ciepluch 8ef2629e0b feat(access-control-prover): 8.3 exact, finite-candidate and unresolved call targets 2026-10-29 16:04:51 +01:00
Marius Ciepluch 6f2154fae0 feat(access-control-prover): 8.2 stable declaration identities and per-change symbol index 2026-10-29 15:45:29 +01:00
Marius Ciepluch 9eee4d7f35 feat(access-control-prover): 8.1 capture call receiver and arity evidence in the semantic IR 2026-10-29 15:33:18 +01:00
Marius Ciepluch 03807f4ddd feat(access-control-prover): task 7.4 - judgment, trace and coverage contracts with abstract state 2026-10-29 15:23:43 +01:00
Marius Ciepluch 2f97fb2693 feat(access-control-prover): 7.3 authority abstract values and promoted implication facts 2026-10-29 15:06:53 +01:00
Marius Ciepluch 351583a04f feat(access-control-prover): 7.2 resource abstract values and operation-fact fields 2026-10-29 14:48:53 +01:00
Marius Ciepluch 5697a7fe9e feat(access-control-prover): 7.1 evidence-relation algebra and completeness value 2026-10-29 14:11:13 +01:00
Marius Ciepluch 0d2b4cf15d docs(spec) access-control-prover: abstract-interpretation amendment -- evidence algebra, stable symbols, label-blind acquisition, admission discipline 2026-10-29 13:31:40 +01:00
Marius Ciepluch 152f405bcf docs(spec,steering): lift access-control-prover to capability level; engine/target split, pattern discipline, complexity caps, breadth map 2026-10-29 12:27:44 +01:00
Marius Ciepluch f09dc66592 docs(spec) access-control-prover: design amendment -- resolution, resource-bound guards, programmatic registration 2026-10-29 12:10:37 +01:00
Marius Ciepluch 3de96c88f6 docs(steering): terminology rule -- name the behavior, not the virtue 2026-10-29 11:57:51 +01:00
Marius Ciepluch bc896d2779 docs(spec) access-control-prover: post-measurement requirements amendment 2026-10-29 11:57:15 +01:00
Marius Ciepluch 37b0a593a7 docs(roadmap): gate 5 decision -- fix trace resolution first, injection spec deferred 2026-10-28 20:12:37 +01:00
Marius Ciepluch efdb66bc73 measure(ablation) gate 3: miss and false-alarm trace-component taxonomy 2026-10-28 20:06:40 +01:00
Marius Ciepluch 0b1d41d01b measure(judge) gate 2: zero-shot judge over prover findings 2026-10-28 19:43:59 +01:00
Marius Ciepluch b247da9e82 chore: add copilot instructions 2026-10-28 18:59:01 +01:00
Marius Ciepluch a60e9bda9d measure(search): 2026-10-07 shiftleft sql-vuln pilot records 2026-10-28 18:59:01 +01:00
Marius Ciepluch fcf05f7755 bench(unseen): p1 pool, draft and bisect freeze artifacts 2026-10-28 18:59:01 +01:00
Marius Ciepluch c5341d79a2 measure(prover): gate 1 on the 23-repo training pool: recall 65.2% (Wilson 44.9-81.2), 15.0 FA/100, 0 instrument failures; 4/5 on the hunt overlap incl. trigger.dev 2026-10-28 18:59:01 +01:00
Marius CiepluchandClaude Fable 5.1 03d925fffa spec/steering: the decision strategy corrected: software features do not decide safety; the trace does, the pool measures and never trains
Maintainer's finding of 2026-10-14 recorded in hunter-learning-loop (a dated section that overrides the shape
annotations as the model's input), its design (amendment pointing to the prover's trace) and the steering
overview's current state.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 19:40:12 +02:00
Marius CiepluchandClaude Fable 5.1 03b114cbeb feat(prover): delivery D: control flow decides dominance; the trace carries each guard's relation, effect and the operation's control context
Opus agent delivery under spec access-control-prover, requirement 10. `semantic/cfg.py` builds a control-flow
graph per function from the syntax tree (if/else, switch arms, loops, try/catch/finally, return, throw, break,
continue, exit, assert) with dominators and a per-line control context, and leaves a function without a graph
rather than a wrong one. `obligations/cfg_dominance.py::CfgDominance` discharges a statement guard only when it
lies on every path to the operation and the operation is unreachable from its failing arm; a predicate whose
result nothing consumes is `value_only` and never discharges; router, decorator and earlier-hop witnesses behave
as before; without a graph the order rule applies and `cfg_unavailable` is recorded. The trace's guards carry
`relation` and `effect`, the trace carries `operation_context`; Java parameter lists carry names only; a
handler-named operation's arguments are the handler's parameters. The checker's default stays order-based.

Smoke on the 23 fix changes: 15 caught, 55 of 93 locations, precision 15 of 15, no failure, no change over
120 s (unchanged from delivery B). Gate: 3575 tests pass; the reserved-repository guard passes on the export.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 19:01:07 +02:00
Marius CiepluchandClaude Fable 5.1 6c3d4a7d72 spec(access-control-prover): a guard whose passing branch alone holds the operation discharges it (effect branches)
Raised by the implementing agent: the design named only exits on the failing arm; if (can(x)) { op(); } is the
common shape and the operation is unreachable from the failing arm there too.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 18:28:10 +02:00
Marius CiepluchandClaude Fable 5.1 2f628b921b feat(prover): delivery C: the ordered trace with argument provenance for every examined pair
Codex delivery under spec access-control-prover, requirement 9. `semantic/obligations/trace.py` serialises each
(entry, operation) pair the prover examined, discharged or unguarded: the entry with its boundary, access and
parameters; each hop in order with its call line, the guards before the call and the values forwarded; the
operation with the provenance of each argument traced through the function's binds; the guards after it; the
verdict. One canonical text form and one JSON form, no language, framework, repository, size or count fields.
The prover result, the arm record and each unguarded finding carry the traces. On the ec2-plugin fix: 32
traces, 4 unguarded. Gate: 3534 tests pass; the reserved-repository guard passes on the tracked export.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 18:22:45 +02:00
Marius CiepluchandClaude Fable 5.1 52ecbb76ab spec(access-control-prover): control flow decides dominance; the trace carries each guard's relation, effect and the operation's control context
Requirement 10, the structural control-flow graph per function and CfgDominance behind the existing protocol,
tasks 4.4 and 4.5. Textual order stays the checker's default; the prover selects control flow.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 18:07:09 +02:00
Marius CiepluchandClaude Fable 5.1 12d09faeed spec(access-control-prover): the ordered trace with argument provenance is the prover's output for every examined pair
The maintainer's correction: counts over a function, language or framework carry nothing about safety; the
object a decision model may see is the path from an attacker-reachable entry to a protected operation, with the
checks on it in control-flow order and the provenance of the operation's arguments. Requirement 9, the trace
contract and tasks 4.2 and 4.3.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 17:56:50 +02:00
Marius CiepluchandClaude Fable 5.1 17e07b36c4 feat(prover): delivery B: handler-named operations, Symfony, Livewire, Remix and Tornado entries, enforcement witnesses, memoised path walk
Codex delivery under spec access-control-prover plus one fix of mine. Operation rows may now name a handler by
name pattern and framework (Jenkins form validation and list filling, Tornado request methods, Remix actions);
the mapper recognises Symfony, Livewire and Laravel controllers, Remix exports and Tornado handlers;
`obligations/enforcement.py` turns Laravel route middleware, Symfony attributes and security.yaml rules and
Tornado's authenticated decorator into router and decorator witnesses. The path walk looks each node's callers
up once per change and does not walk a tree with no recognised entry: one seatunnel change fell from 670 s to
35 s. One name Codex could not source (Tornado get_current_user) is left out and said so in the facts header.

Smoke on the 23 fix changes: 15 pushes caught (65 percent, Wilson 45 to 81), 55 of 93 locations, precision
15 of 15 flagged, no instrument failure, no change over 120 s. Delivery A caught 7.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 17:31:07 +02:00
Marius CiepluchandClaude Fable 5.1 7f1b820d5a style(prover-arm): format
The previous commit was gated through a pipe whose exit status was tail's, not ruff's; CI caught the
unformatted file.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 17:03:35 +02:00
Marius CiepluchandClaude Fable 5.1 5980bf8377 fix(prover-arm): the byte table holds only files that were read, so a zero-byte read stays on the record and the summary refuses it
CI failed test_unchanged_file_empty_read_refuses: the previous fix skipped failed records in the zero-byte rule.
Now the arm records a file's size only after reading it (a git-empty file is counted under empty_files and
not listed), a real zero-byte read keeps its zero and the summary refuses it on every record as the test says.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 17:00:13 +02:00
Marius CiepluchandClaude Fable 5.1 beb272a5ec feat(prover): access-control prover, delivery A: path records, Stapler and Jetty entries, Java operation rows, the prover and its scoring arm
Codex delivery under spec access-control-prover. `semantic/obligations/paths.py` builds entry-to-function path
records from the cached caller index; `mapping.py` names Stapler web methods and Jetty handlers as entries;
`check_obligations` gains the opt-in premise `assume_entries_protected` with the label `unguarded_path`;
`hunt/prover.py` proves a change with no model call and states its coverage; `benchmarks/valid/prover_arm.py`
scores it with the valid-benchmark metrics. Two fixes after the first smoke run: a product file git holds empty
is read, not unread (four changes failed on `__init__.py` and empty assets), and absent-input reasons are
counted by name.

Smoke on the 23 fix changes of the training pool: 7 pushes caught (30 percent, Wilson 16 to 51), 28 of 93
locations, precision 7 of 8 flagged, no instrument failure; three changes over the 120 second bound. Twelve of
the 17 Jenkins fixes reach the fixed method but check no operation because the method is the operation;
the spec now carries handler-named operations for delivery B.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 16:50:04 +02:00
Marius CiepluchandClaude Fable 5.1 e514551cb6 spec(access-control-prover): the checker gains an opt-in premise and the unguarded_path label
Codex stopped on a real conflict: with path records and no clause or sibling norm the checker returns no finding
by design. The prover's premise (a recognised entry is protected unless declared public) is now an opt-in keyword
with its own label and evidence, default off, existing behaviour and tests unchanged.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 15:54:29 +02:00
Marius CiepluchandClaude Fable 5.1 74a529825d spec: access-control prover (requirements, gap analysis, design, tasks)
A deterministic check that a protected operation is reachable from an entry point without a check dominating
the path, per framework, built on the existing obligations checker, caller index and entry mapper; scored as a
rule arm on the access-control training pool. Follows the maintainer's finding that the hunter's features
describe shape and cannot decide unsafety.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 15:51:25 +02:00
Marius CiepluchandClaude Fable 5.1 9feb8f1e33 fix(hunt): a row's entry points are the ones in its file or a caller's file, not the whole repository's list
The DSPy arm over the second pool failed with LMInvalidRequestError on every change with more than two rows, at no
cost: `source.facts_for` attached every entry point of the product tree to every row, 8190 records and 1.5 MB per
row on apache/seatunnel (the first pool's arm lost 11 changes the same way on trigger.dev and shopper), and the
rendered prompt was refused. The screen table of the second pool weighed 814 MB for the same reason.

A row now carries the entry points declared in its own file or in a file that calls the function, which is what the
input has described all along ("in-repository entry points that reach the file"). `source.entry_point_count`
follows that definition.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 14:47:08 +02:00
Marius CiepluchandClaude Fable 5.1 81ae206978 fix(hunt): build output gets no candidate rows, a minified line is not scanned once per function, the screen checkpoints every change
The second access-control screen spun for 2h20m on one ordinary mage-ai change: a Next.js build commit whose 3 MB
one-line bundles hold 12,355 functions each. `source.ranges_from_ir` ran two regex scans of the whole line once per
function, and the screen kept its 422 finished changes in memory only, so stopping it lost them.

- `source.ranges_from_ir`: a line over MINIFIED_LINE_CHARS (2000) is not checked per function; JavaScript names on it
  stay anonymous, other languages keep the parser's name.
- `source.generated_reason`: why a changed file is build output (a directory the product walk leaves out, a minified
  name, over MAX_FILE_BYTES, a line over the cap). `hunt.producers._candidates` leaves such files out and records the
  reason on the context; the fix site of a vulnerability is always kept. The DSPy arm shares the enumeration.
- The screen writes rows.jsonl and log.jsonl per change (rows first, entry last) and resumes by skipping logged ids.

Tests: the minified line never reaches the per-function scan; generated_reason on the four shapes and two source files;
build output in an ordinary change yields no rows while a vulnerability path in a one-line file is kept.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 13:24:45 +02:00
Marius CiepluchandClaude Fable 5.1 4cf9c85d22 perf(hunt): the caller search prepares each product file once per change
call_sites rescanned every line of every product file for declarations on each call; with one name per
candidate row that was the whole cost of the source producer. code_index prepares a file once (the names each
line declares), call_sites takes it, and callers_of keeps a cache of prepared files the producer context owns.
Same calls, tested against the unprepared scan. One Laravel change of 33 rows: 249 seconds before this pair of
commits, 20 now.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 09:46:46 +02:00
Marius CiepluchandClaude Fable 5.1 86d70831c8 perf(hunt): the source producer walks and reads the product tree once per change, not once per row
facts_for walked the whole product tree and re-read every product file for each candidate row; on a Laravel
application one change of 33 rows took four minutes, 96 percent of it there. The producer context already
holds the product file list and the texts it read for entry points, so facts_for and callers_of now accept
them. Same facts, tested by a call whose tree walk raises and whose file on disk is emptied after reading.

Co-Authored-By: Claude Fable 5.1 <[email protected]>
2026-10-14 09:35:16 +02:00