Research / AUTH-CONTRACT-1: scoped policy proofs + cross-stack enforcement conformance (Cedar / OwnIR / runtime witnesses) #453

Classification / relationship to existing work

Research / bounded feasibility pilot · P2–P3 backlog · no production feature or ownership-engine pivot authorized.

Investigate cross-stack, contract-driven authorization verification as a possible opt-in consumer of Own.NET's source facts, graph and witness infrastructure. The product question is not "can we make another authorization linter?" but:

Given a human-reviewed authorization policy, can we establish that every supported execution path to one protected effect enforces the correct actor–action–resource decision, and return source-backed counterexamples or honestly scoped proof results?

Parent / scope boundary: #448 already covers general requirements-to-code conformance. This issue is its security-authorization vertical and evaluation corpus, not a second general requirements framework. Reuse #447 for model extraction/witness design, #272 for obligations, and #382 for retaining canonical interprocedural call information. Related proof/soundness research: #445, #451. None is automatically a dependency or permission to rewrite production OwnIR.

Not an instruction to scan third-party systems, reveal internal vulnerabilities, change existing product security policies or deploy a new authorization engine. Research only in locally controlled fixtures/environments with synthetic data.

Distinguish three different claims

1. Policy correctness (PDP): a policy satisfies a formally stated property (e.g. an unprivileged principal is always denied an update on a protected resource). Cedar SymCC / SMT may prove policy properties under its schema, entities, context and assumptions.
2. Enforcement conformance (PEP): real C# application paths invoke the correct policy for the same authenticated actor, action and resource, consume its decision, and prevent the protected effect when denied. This cannot be inferred solely from a valid policy.
3. Cross-stack end-to-end conformance: C#, gateway/routing/HTTP, downstream Go/other services and persistence preserve authorization identity/operation/resource binding; there is no bypass path via another transport, entry point or backend writer. A partial call graph, mocked backend or policy solver result does not prove this.

Potential contract (illustrative, not a ready schema):

contract: profile-update
action: Profile.Update
requires:
  permission: "profile.update"
  resource_scope: target_profile
protected_effect:
  entity: Profile
  kind: persistent_mutation
properties:
  - denied_operation_has_no_effect
  - all_supported_paths_are_authorized
  - actor_action_resource_binding_preserved

The reviewer-approved policy is an external input, not extracted uncritically from current possibly-buggy implementation. Policy authors must also specify who may perform legitimate system/background actions, scope exceptions, entity identity, temporal validity, and trusted callers.

Gate 0 — state of the art and Own.NET capability inventory (read-only)

• Pin current Own.NET SHA, Roslyn facts / OwnIR representation, Rust/Python analysis surface, call/CFG summaries, effect reachability, source anchors, unknown propagation and SARIF/codeFlows. Read the actual implementations and open limitations, especially Canonical first-party call facts: preserve interprocedural calls instead of collapsing them into frontend release/use/escape guesses #382; do not assume a complete call graph or effect/alias analysis.
• Check which facilities already exist and whether an opt-in external verification consumer is more appropriate than enlarging ownership-specific diagnostics or changing the default CLI.
• Source-backed comparison with Cedar + cedar-policy-symcc, AWS IAM Access Analyzer/Zelkova, OpenFGA model tests, SpiceDB schema validation, CodeQL C# authorization queries, Semgrep, OWASP access-control matrix testing, and relevant formal approaches (NIST IR 8539, transition-system/temporal logic). Separate formal proofs of a policy from tests of example decisions and from whole-program claims.
• Identify unsupported semantic boundaries (reflection, virtual/interface dispatch, DI, dynamically constructed HTTP URLs, middleware, handlers, raw SQL/stored procedures, external processes, auth token forwarding, concurrent writes, unmodeled libraries).
• Define one specific opportunity missed by existing tools, or conclude NO-GO before writing a checker. Never conflate analyzer quality with number of findings.

Gate 1 — minimal independently reviewed contract and fixtures

Pick one synthetic/authorized C# domain operation (e.g. Profile.Update), with two entry points and one persistent effect. Keep sensitive company routes, permissions, incident details and tokens out of the public repository.

Freeze, before inspecting verifier output:

• Explicit actor/action/resource/decision truth table; permitted exceptions and which identities are trusted.
• What constitutes an effect (persisted state, not merely HTTP 200/403) and a denied operation.
• A clear policy schema with bounded entity/context assumptions.
• The actual code/symbol/effect mappings and their verified provenance.
• Control corpus: (a) correct implementation; (b) missing authorization on alternate entry; (c) Read checked before Update; (d) result of Authorize ignored; (e) a legitimate distinct privileged system path; (f) unresolved external call/unknown effect; optional wrong-resource binding and TOCTOU if representation supports them.

Require a positive reachability control so a never-executing mutation cannot produce a vacuous green test.

Gate 2 — separate policy proof and enforcement analysis

A. Policy layer: prototype with existing Cedar SymCC or another well-supported verifier if the chosen semantics fit. Check a useful universal property or equivalence/inclusion; collect counterexample and precise solver/schema assumptions. If the desired rule needs temporal state not expressible in the policy model, mark this limitation and evaluate a small transition model (Quint/TLA+ as a candidate), not a full new solver.

B. C# enforcement layer: start from code facts / CodeQL baseline and see if existing Own.NET extraction can trace supported entry points to an authorized protected effect. A successful authorization check must dominate the relevant effect on each feasible path and be bound to matching actor/action/resource/state; syntactic appearance of Authorize is insufficient. Account for false-positive paths, exceptions, async, unknown targets and alternate writers. Never silently interpret an unresolved call as safe.

C. Runtime witness: in isolated .NET fixtures, exercise negative/positive cases and verify before/after persisted state, not just status codes. Mutation controls must force expected red failures. Separate a candidate static trace from a reproduced executable witness.

D. Cross-stack extension only after A–C provide incremental value: use one small local C# → HTTP → Go (or alternate-language) fixture, with independent parsers/handlers and one protected write. Verify stable actor/action/resource binding and comparison of the operation authorized vs operation executed. A disconnected two-language model does not demonstrate cross-stack conformance. Reuse existing Go analyzers or contract/integration harness; do not build a full Go frontend as a prerequisite.

Evidence / proof vocabulary

Report each property with a coverage envelope: code SHA, entry points and effect sinks included, analyzed languages and component versions, closed-world assumptions, modeled entities/contexts, source-to-model mapping completeness, unresolved dispatches, runtime/environment assumptions, and exact verifier commands.

Allowed outcomes:

• POLICY-PROVEN (SCOPED): policy theorem proved under stated policy-model assumptions, not application correctness.
• ENFORCEMENT-PROVEN (SCOPED): only when implementation-to-model relation and all relevant paths/effects are themselves justified under an explicit bounded/closed-world model; otherwise do not use this label.
• VIOLATED / REPRODUCED: reviewed reachable counterexample, preferably runtime corroboration, with source-linked path and effect witness.
• TESTED-BOUNDED: negative/positive fixtures passed; not a proof of all executions.
• UNKNOWN / INCOMPLETE / NOT-APPLICABLE: incomplete graph, unsupported semantics, inconsistent or unspecified business rule, unresolved integration, etc. No false PASS under unknowns.

Explicitly distinguish:

• policy misunderstanding vs source extraction unsoundness vs genuine implementation defect;
• falsifiable safety claims vs unbounded liveness/availability claims;
• static path candidate vs feasible execution;
• test accuracy and negative controls vs theorem/proof obligation.

Evaluation / success and stop criteria

• Independent prior-art inventory and dedup map (Research: requirements-to-code conformance checking (BDD + reviewed formal contracts + OwnIR evidence) #448/Research: FeaVer/Ultimate-style property-guided model extraction and source-level witnesses (bounded spike) #447/P1: Add Obligation Protocols for project-specific barrier-sensitive rules #272/Canonical first-party call facts: preserve interprocedural calls instead of collapsing them into frontend release/use/escape guesses #382, Own.NET Rust/Python core); recorded pinned upstream versions/links.
• One small human-reviewed, frozen authorization contract and threat/assumption model.
• One positive fixture, ≥3 relevant violation mutants, ≥1 legitimate privileged-path near neighbor, ≥1 unsupported/unknown case; controls show non-vacuous failure.
• A policy-level property checked with an existing solver or documented NO-GO on semantics/tooling.
• Baseline CodeQL/Semgrep + ordinary integration tests run against the same fixtures; compare TP/FP/FN/UNKNOWN, setup/maintenance cost, and source-witness fidelity with any Own.NET-based prototype.
• No claimed end-to-end proof without faithful mapping of relevant operations and effects; explicit coverage assumptions.
• If warranted, one local cross-stack witness with synthetic data, authorizer decision + executed operation + persisted state.
• Outcome GO-EXTERNAL-AUTH-PILOT / DEFER-MISSING-FACTS / STOP-NO-INCREMENTAL-VALUE with reproducible commands, SHA, artifacts and honest scope.

Strong GO signal: a validated cross-entry authorization defect or meaningful proof/witness improvement not available from existing CodeQL + policy solver + integration baseline. A mere wrapper for Cedar or new YAML syntax is not enough.

Hard non-goals

• No broad "formally prove your entire app secure" or OWASP compliance certification claim.
• No generalized multi-stack CPG, full Go static analyzer, auto-synthesized policy treated as ground truth, custom SMT solver, or mandatory Cedar dependency.
• No new production security rule, scanning of non-owned infrastructure, or use of production credentials. No Git push, PR, deploy or production fix automatically authorized by this research issue.
• No silent changes to Own.NET ownership semantics, default CLI, core architecture, existing milestones or mandatory CI.
• No disclosure of private defect routes, exploit details, user data or internal repositories in this public issue.

Starting references

• Cedar language and analysis, Cedar SymCC, AWS: open-source Cedar Analysis
• CodeQL C# function-level access control
• OWASP Authorization Cheat Sheet, OWASP ASVS
• NIST IR 8539, OpenFGA, SpiceDB
• Own.NET #448, #447, #382

Conditional extension — infrastructure-to-code route semantics (after Gate 2D)

Status: optional Stage E / research-later, not a prerequisite for Gate 0–2, and not a mandate to extend OwnIR. The code path and the infrastructure routing/configuration together determine which protected operations may be reachable. Evaluate whether an external cross-stack semantic graph can connect infra-declared routes and trust boundaries to the C#/Go execution/effect graph, while keeping ownership-focused OwnIR and its existing guarantees unchanged.

Hypothesis and architecture seam

Use separate, independently auditable fact producers:

C# (Roslyn -> OwnIR/call/effect facts)    Go (AST/SSA or verified handler facts)
                   \\                        /
                    \\                      /
nginx/ingress/IaC (parsed + resolved effective routes)      Policy (reviewed actor/action/resource)
                         \\                /
             Cross-stack route/trust/effect graph
                      -> bounded property checker
                      -> candidate path + source/config evidence
                      -> local end-to-end witness / UNKNOWN

Candidate graph relations, with explicit semantics and provenance: exposes, routes_to, rewrites_to, calls, authenticates, authorizes, delegates_identity, trusts_header_from, mutates. Do not reduce an nginx proxy_pass to an ordinary OwnIR call: it has different semantics and failure modes. Graph edges need source/config location, resolved deployment/version, validation method, and whether their target is complete/unknown.

Stage E1 — one reproducible local nginx -> C# -> Go fixture

Only after the basic policy proof, C# enforcement pilot and C#->Go runtime witness demonstrate incremental value:

1. Construct a synthetic local route table with two public/private entry paths, one protected Profile.Update effect, known fake actors and permissions, and a local state store. Use no private production configs, live endpoints or credentials.
2. Parse a minimal nginx config using a mature existing parser (e.g. nginxinc/crossplane); independently verify actual behavior against the exact pinned nginx binary/config (e.g. nginx -T for rendered config, local HTTP traces). Parsing syntax alone is not semantic verification.
3. Model just the route rules needed by the fixture, including applicable location precedence, URI normalization, proxy_pass URI replacement, rewrite / internal redirects, auth_request failure behavior, and relevant forwarded/trust headers. Record supported variants and reject unsupported semantics as UNKNOWN. Do not guess target routes from unresolved templates, includes, variables or runtime modules.
4. Bind route transitions to explicit, reviewable C#/Go handler identities and authorization/effect witnesses; compare the authorized actor/action/resource with the executed operation + persisted mutation, not merely response status.
5. Controls: (a) safe baseline; (b) alternate exposed nginx route bypassing the intended auth boundary; (c) direct backend endpoint reachable contrary to a declared trust assumption; (d) deliberately ambiguous/unresolved route yielding UNKNOWN; (e) legitimate internal-only route with separately verified reachability policy, to measure false positives.
6. Distinguish the checker found a candidate path from the path was shown reachable in an isolated runtime. Require negative mutation controls and positive non-vacuity controls before reporting meaningful success.

Stage E2 — compare other infrastructure forms only if E1 passes

• Kubernetes Ingress / Gateway API / Terraform / Helm / environment-rendered config: consider existing structured parsers and scanners (e.g. Checkov, Conftest) as sources of infra facts, not as a substitute for effective routing/auth semantics.
• Serverless comparator (future): one equivalently scoped synthetic API Gateway -> Lambda -> datastore fixture. Model entry-point exposure, IAM/resource policies, direct Lambda function URLs where relevant, authorizer-cache identity/key, service roles and persisted effects. Serverless relocates trust boundaries to declared cloud configuration; it does not remove them. No AWS account needed or authorized for this pilot: start with offline configuration modeling and local fixtures, and mark unvalidated platform semantics UNKNOWN.
• Config vs deployment drift: distinguish repository templates from effective rendered configuration and actually deployed revision. Without trustworthy effective-config provenance, a "no reachable bypass" verdict cannot cover production. Specify version/environment/secret-free sanitized provenance and prevent claims spanning unobserved or stale deployments.
• Infrastructure managed outside the repo: explicitly label NOT COVERED unless supplied trustworthy facts. Never silently infer the absence of a bypass from an absent ingress config.

Property, proof boundary, and comparison

Target the same reviewed security invariant as Gates 1–2, without broadening policy scope:

For each supported path from an untrusted entry to Profile.Write:
  the matching actor/action/resource authorization decision must be valid
  and deny must prevent the protected persistent effect.

A candidate may be VIOLATED/REPRODUCED, TESTED-BOUNDED, or UNKNOWN/INCOMPLETE. ENFORCEMENT-PROVEN (SCOPED) is permitted only if the relevant routing semantics, trust model, backend mappings, call/effect coverage and model correspondence are justified as complete for the declared scope. No proof claim for arbitrary nginx extensions or arbitrary cloud platform behavior.

Measure incremental benefit versus: (i) native nginx config/runtime checks, (ii) Checkov/Conftest infra rules, (iii) CodeQL/C# baseline, and (iv) the current Gate 2 C#→Go end-to-end tests. Collect true/false positives, unknowns, concrete witnesses, setup cost and provenance precision. If a few local tests and existing tools already catch all controls with less maintenance, close Stage E as STOP-NO-INCREMENTAL-VALUE.

Decision / non-goals

• Gate 2D completed and approved as useful; otherwise Stage E remains parked.
• Effective nginx config and semantics scope pinned, plus a cross-layer edge provenance/unknown record.
• Reproduce at least one actual local infra-to-code auth mismatch and one correctly rejected benign near-neighbor, or clearly record NO-GO.
• Compare against existing infra/code scanners and E2E baseline; report GO-BOUNDED-GRAPH-PILOT / DEFER-EFFECTIVE-CONFIG / STOP-NO-INCREMENTAL-VALUE.
• If successful, propose a separate opt-in consumer / issue, not a default Own.NET production change.

Hard boundaries: no generic nginx emulator, no multi-cloud completeness claim, no mandatory new Go/frontend/parser stack, no production infrastructure changes, no scans or requests to non-owned hosts, no privileged cloud credentials or secret-bearing config dumps, no blind expansion into "OWASP correctness certification".

Relevant primary documentation: nginx request processing, nginx location/proxy_pass/rewrite, proxy_pass, auth_request, AWS Lambda function URLs.

Gate 0 addendum — Confirmate / Fraunhofer CPG donor-or-competitor check

Research update, 2026-11-04 · mandatory prior-art comparison before any new graph/evidence-store implementation. The earlier Cloud Property Graph / general multi-language graph novelty assumption is no longer viable as a unique product claim. In particular, re-evaluate the following independently maintained projects and their implemented (not merely advertised) behavior:

A. Confirmate: continuous assessment and evidence provenance

• confirmate/confirmate (Apache-2.0) is a newer platform in the Clouditor ecosystem; distinguish it from clouditor/cloud-property-graph, which is a research prototype tying static code analyses to cloud runtime assessments.
• The current Confirmate repository README labels the open-source release work in progress. It documents a Go orchestrator, CLI, in-memory local mode, evidence/assessment components, and collectors for AWS, Azure, OpenStack, IONOS, Kubernetes and CSAF. Some build/usage surfaces are still described as in-progress. Do not infer that production-grade source-to-policy proofs or cross-stack C#/Go+nginx semantics already exist.
• Check actual public implementation and component readiness (pinned SHA), data model for target of evaluation, evidence, assessment, collector identity, timestamps, version/provenance, API/export, auth boundaries and lifecycle. Examine whether a small Own.NET proof/witness can be represented as externally produced evidence without losing assumptions, complete/incomplete coverage, source/config SHA, negative-control results, status or source locations.
• Run only local/in-memory/synthetic exercises without cloud credentials. Prefer an existing evidence format/API if it preserves our proof honesty. If it conflates a tested observation with a proved property, do not integrate as-is.
• Compare the maintenance cost of reusing Confirmate vs a minimal file-backed ledger (JSON/SARIF + links). Do not build a new evidence store unless a concrete unmet requirement is demonstrated; equally, do not pull an orchestrator into the pilot for the sake of infrastructure.

Primary sources: Confirmate README, cloud collector documentation, CloudPG README, Fraunhofer Confirmate/CRA overview.

B. Fraunhofer-AISEC CPG: existing semantic graph and extensible passes

• Fraunhofer-AISEC/cpg provides a multi-language Code Property Graph with extensible passes, source/flow/evaluation-order facts and optional persistence. Its current README explicitly lists Go as maintained, while C# is absent from the main-branch language support matrix; verify any C# PR/branch separately before claiming support.
• Before extending OwnIR into a universal multi-stack IR, compare a minimal external graph adapter consuming existing Roslyn/OwnIR facts against CPG's graph model / existing passes. OwnIR remains focused on its existing ownership analysis, with no new default graph/database dependency.
• Evaluate, on a tiny reviewable C# + Go fixture: method identity/call-site mapping, CFG/DFG/EOG coverage, virtual/opaque calls, source spans, alias/effect mapping, error/unknown handling, and stable cross-language HTTP endpoint binding.
• Confirm that the adapter can retain proof-relevant distinctions: actor, action, resource, authorization decision used to guard a persistent effect, and unresolved paths. A plain graph edge authorizes or calls is not itself a verified authorization guard.
• Check whether an external CPG query/pass catches the same seeded missing-authorization case as the proposed Own.NET approach. Prefer reuse if equivalent; do not introduce a second whole-program solver or custom multi-language CPG.

Primary sources: CPG README and supported-language table, CPG documentation, CloudPG architecture.

Compare against the actual AUTH-CONTRACT-1 objective, not marketing labels

The decision is whether we have a distinct capability linking reviewed authorization contract → source/config execution path → matched actor/action/resource → denied write effect → independently reproducible witness under explicit completeness assumptions.

Evaluation questions (record explicit answers):

1. Can existing CPG/CloudPG abstractions express the needed cross-layer semantic facts, or is a narrow external relation adapter sufficient?
2. Can Confirmate store/present evidence with the needed PROVEN (SCOPED) vs TESTED vs UNKNOWN distinctions without misleading compliance conclusions?
3. Does the proposed Own.NET consumer find a confirmed defect, give a better source-level witness, or reduce setup/review cost over CPG/Codyze + CodeQL + Cedar + conventional tests?
4. If not, should the result be DONOR-REUSE / STOP-NO-INCREMENTAL-VALUE rather than a new verification framework?

Acceptance / stop:

• Pin exact upstream SHAs, public implementation surfaces, license and reproducible local commands; record functionality missing or only planned.
• One tiny donor comparison (no production integration) for CPG and one minimal evidence export/read assessment for Confirmate; if these cannot run, document specific blockers rather than invent results.
• Report semantics and model-coverage differences, maintenance and deployment burden; keep separate POLICY-PROVEN, TESTED-BOUNDED, VIOLATED, UNKNOWN outcomes.
• Explicit verdict: REUSE-DONORS, GO-NARROW-EXTERNAL-CONSUMER, DEFER-DONOR-MATURITY, or STOP-NO-INCREMENTAL-VALUE.
• No production OWN.NET rewrite, automatic CI gate, distributed evidence infrastructure, or claim of formally proving arbitrary C#/Go/nginx systems by default.

Out of scope: LumberChunker is a document semantic-chunking / retrieval experiment, not an authorization-verification or OCR component; track it separately in the AI Assistant repository when that repository is identified. Do not add it to the OWN.NET security implementation plan.