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]>
This commit is contained in:
Marius Ciepluch
2026-10-14 17:31:07 +02:00
co-authored by Claude Fable 5.1
parent 7f1b820d5a
commit 17e07b36c4
18 changed files with 1179 additions and 66 deletions
@@ -1,3 +1,5 @@
# Handler obligations: Jenkins form validation and list filling require permission checks.
# https://www.jenkins.io/doc/developer/security/form-validation/ (reference in the approved brief).
# Delivery A additionally checked actual calls in Git HEAD objects (2026-10-14):
# p4-plugin: CredentialsHelper.lookupCredentialsInItem, P4PasswordImpl and P4TicketImpl
# call ConnectionFactory.testConnection, ConnectionFactory calls connect, ReviewNotifier
@@ -79,3 +81,11 @@ id = "identity-from-context"
kind = "identity_constraint"
identity_sources = ["SecurityContextHolder.getContext().getAuthentication()", "Jenkins.getAuthentication()", "Jenkins.getAuthentication2()", "getUserPrincipal()"]
request_sources = ["getParameter(", "getHeader(", "getCookies(", "getQueryString("]
[[operation]]
id = "stapler-handler"
kind = "privileged_action"
handlers = ["^do(?:Check.*|Fill.*Items|Test.*|Validate.*|Verify.*)$"]
framework = "stapler"
requires = ["path_guard"]
sensitivity = "high"
@@ -1,3 +1,9 @@
# Delivery B enforcement sources: shopperlabs__shopper Git HEAD packages/admin/routes/web.php
# uses chained middleware and groups. kimai__kimai at the pool revision uses @Route(path=...)
# and @Security in src/Controller/InvoiceController.php (class and action docblocks).
# Recognised contract names from the approved spec and the references below: Laravel auth, can:,
# role and permission middleware, constructor middleware/authorizeResource; Symfony IsGranted,
# Security and security.yaml access_control. No PHP operation or discharger row was changed.
# Closed authorization facts for Laravel, WordPress and Symfony.
# Checked shopperlabs__shopper Git HEAD source objects in /home/mc/ousast-results/valid/train/hist/:
# CollectionProducts.authorize, SetupGuide.can, AssetController.abort_unless,
@@ -1,3 +1,6 @@
# Checked mage-ai__mage-ai Git HEAD and websocket fix 66440e4d3: no authenticated
# decorator or get_current_user definition found. authenticated is already an existing fact.
# Handler names follow the Tornado RequestHandler/WebSocketHandler contract in the approved spec.
# Obligated operations and dischargers for Python web code (authorization-obligations, Req 1). Closed data.
version = "1"
language = "python"
@@ -84,3 +87,11 @@ permissive_values = ["False"]
id = "validated-input"
kind = "validated_input"
calls = ["validate", "schema.load", "parse_obj", "model_validate", "clean", "is_valid", "secure_filename", "safe_join"]
[[operation]]
id = "tornado-handler"
kind = "privileged_action"
handlers = ["^(?:get|post|put|delete|patch|head|options|open)$"]
framework = "tornado"
requires = ["path_guard"]
sensitivity = "high"
@@ -1,3 +1,6 @@
# Checked triggerdotdev__trigger.dev Git HEAD: apps/webapp/app/services/session.server.ts
# defines requireUser and requireUserId; apiAuth.server.ts defines authenticateApiRequest;
# routes/resources.dashboard-agent.alerts.$channelId.unsubscribe.tsx defines and calls authorize.
# Obligated operations and dischargers for TypeScript web code (same surface as JavaScript) (authorization-obligations, Req 1). Closed data.
version = "1"
language = "typescript"
@@ -72,7 +75,7 @@ sensitivity = "medium"
[[discharger]]
id = "route-guard"
kind = "path_guard"
calls = ["authenticate", "requireAuth", "ensureAuthenticated", "isAuthenticated", "verifyToken", "checkAuth", "protect", "authorize", "requireUser", "getServerSession", "auth", "withAuth", "jwt.verify", "passport.authenticate"]
calls = ["authenticate", "requireAuth", "ensureAuthenticated", "isAuthenticated", "verifyToken", "checkAuth", "protect", "authorize", "requireUser", "requireUserId", "authenticateApiRequest", "getServerSession", "auth", "withAuth", "jwt.verify", "passport.authenticate"]
decorators = ["UseGuards", "Authorized", "Roles"]
# `req.session` is the authenticated context itself, and it is listed because a destructuring spells the
@@ -112,3 +115,11 @@ permissive_values = ["false"]
id = "validated-input"
kind = "validated_input"
calls = ["parse", "safeParse", "validate", "validateSync", "sanitize", "escape", "validationResult", "z.object", "assert"]
[[operation]]
id = "remix-handler"
kind = "privileged_action"
handlers = ["^action$"]
framework = "remix"
requires = ["path_guard", "ownership_check"]
sensitivity = "high"