From 7b6e981f936454f53fb8c57ff8ebb0bb9a33ceda Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Wed, 23 Sep 2026 07:32:52 +0200 Subject: [PATCH 1/2] docs: define IFC profile variability and publication rules --- docs/decisions/adrs/README.md | 1 + ...01-adversarial-participant-flow-control.md | 19 ++ ...articipant-control-and-governed-effects.md | 18 ++ ...ifc-profile-variability-and-publication.md | 97 ++++++ docs/decisions/adrs/adr-index.yaml | 13 +- ...-1354-ifc-profile-variability-preflight.md | 261 ++++++++++++++++ .../modular-participant-control-contracts.md | 12 + docs/governance/requirement-scopes/1354.json | 78 +++++ docs/migration/ifc-profile-variability.md | 91 ++++++ docs/requirements/SEM-233/requirement.md | 34 ++- docs/requirements/SEM-235/requirement.md | 34 ++- .../research/ifc-profile-variability/cases.md | 92 ++++++ .../tests/ifc_profile_variability_model.py | 132 +++++++++ .../tests/test_issue_1354_governance.py | 38 +++ ...test_issue_1354_ifc_profile_variability.py | 279 ++++++++++++++++++ specs/formal/participant-semantics/README.md | 6 + .../adversarial-flow-control.md | 6 + .../ifc-profile-variability.md | 190 ++++++++++++ .../modular-participant-control.md | 6 + tools/policy/historical_identity_records.json | 4 +- tools/policy/requirement_order.yaml | 16 + 21 files changed, 1421 insertions(+), 6 deletions(-) create mode 100644 docs/decisions/adrs/adr-113-ifc-profile-variability-and-publication.md create mode 100644 docs/decisions/issue-1354-ifc-profile-variability-preflight.md create mode 100644 docs/governance/requirement-scopes/1354.json create mode 100644 docs/migration/ifc-profile-variability.md create mode 100644 docs/research/ifc-profile-variability/cases.md create mode 100644 implementations/python/tests/ifc_profile_variability_model.py create mode 100644 implementations/python/tests/test_issue_1354_governance.py create mode 100644 implementations/python/tests/test_issue_1354_ifc_profile_variability.py create mode 100644 specs/formal/participant-semantics/ifc-profile-variability.md diff --git a/docs/decisions/adrs/README.md b/docs/decisions/adrs/README.md index 4cb2bbfca..a52387330 100644 --- a/docs/decisions/adrs/README.md +++ b/docs/decisions/adrs/README.md @@ -265,3 +265,4 @@ adr-108-modular-participant-control-and-governed-effects | [110](adr-110-reusable-mixed-control-policies-and-occurrences.md) | Reusable Mixed-Control Policies and Occurrences | accepted | 2026-09-22 | | [111](adr-111-control-applicability-and-effect-decisions.md) | Control Applicability and Effect Decisions | accepted | 2026-09-22 | | [112](adr-112-external-inject-triggering-and-execution.md) | External Inject Triggering and Execution | accepted | 2026-09-22 | +| [113](adr-113-ifc-profile-variability-and-publication.md) | IFC Profile Variability and Publication | accepted | 2026-09-23 | diff --git a/docs/decisions/adrs/adr-101-adversarial-participant-flow-control.md b/docs/decisions/adrs/adr-101-adversarial-participant-flow-control.md index 4fc05fdae..5ad63bc4a 100644 --- a/docs/decisions/adrs/adr-101-adversarial-participant-flow-control.md +++ b/docs/decisions/adrs/adr-101-adversarial-participant-flow-control.md @@ -65,6 +65,23 @@ with participant-neutral authority. ## Decision +### Amendment: IFC profile variability and publication (#1354) + +[ADR-113](adr-113-ifc-profile-variability-and-publication.md) and +[IFC-01–IFC-07](../../../specs/formal/participant-semantics/ifc-profile-variability.md) +separate authored owner/guarantee requirements, published profile meaning and +backend realization. Governed finite publication remains the extension route; +no new owner syntax, policy interpreter or plugin facility is introduced. +Independent obligations, conservative propagation, per-obligation release +authority and immutable provenance remain mandatory. CA-04 governs admission; +losing an admitted guarantee blocks the affected release. The published v1 +vocabulary and non-exact-support rejection remain unchanged. + +The amendment's [migration contract](../../migration/ifc-profile-variability.md) +preserves historical profile/release interpretation and requires explicit +consumer support before owner-aware or revised bounded-support claims. This +semantic publication does not implement those consumers or certify a backend. + ### 1. Add two DRAFT owners SEM-233, **Adversarial Participant Boundary Information-Flow Control**, @@ -287,6 +304,8 @@ evidence records retain their own dates and scope. | Date | Commit/PR | Summary | | --- | --- | --- | | 2026-09-06 | #1068 | Clarify modular composition, governed effects and the declared-world boundary under ADR-108 while preserving the security profile and runtime interpreter non-goal. | +| 2026-09-23 | #1354 | Define IFC profile variability, requirement-relative support, per-obligation release and immutable migration under ADR-113. | + ## References diff --git a/docs/decisions/adrs/adr-108-modular-participant-control-and-governed-effects.md b/docs/decisions/adrs/adr-108-modular-participant-control-and-governed-effects.md index 0e907a1c7..c4c12746e 100644 --- a/docs/decisions/adrs/adr-108-modular-participant-control-and-governed-effects.md +++ b/docs/decisions/adrs/adr-108-modular-participant-control-and-governed-effects.md @@ -55,6 +55,23 @@ They do not all have information-flow labels. ## Decision +### Amendment: IFC profile variability and publication (#1354) + +[ADR-113](adr-113-ifc-profile-variability-and-publication.md) and +[IFC-01–IFC-07](../../../specs/formal/participant-semantics/ifc-profile-variability.md) +separate authored owner/guarantee requirements, published profile meaning and +backend realization. Governed finite publication remains the extension route; +no new owner syntax, policy interpreter or plugin facility is introduced. +Independent obligations, conservative propagation, per-obligation release +authority and immutable provenance remain mandatory. CA-04 governs admission; +losing an admitted guarantee blocks the affected release. The published v1 +vocabulary and non-exact-support rejection remain unchanged. + +The amendment's [migration contract](../../migration/ifc-profile-variability.md) +preserves historical profile/release interpretation and requires explicit +consumer support before owner-aware or revised bounded-support claims. This +semantic publication does not implement those consumers or certify a backend. + ### Amendment: exact-cut applicability and effect decisions (#1352) [ADR-111](adr-111-control-applicability-and-effect-decisions.md) and @@ -254,3 +271,4 @@ backend equivalence, or protection of opaque internals and undeclared channels. | Date | Reference | Change | | --- | --- | --- | | 2026-09-22 | #1352 | Clarify apparatus versus applicability, obligation coverage, typed dependency invocation, optional failure, required strength, atomic state and phase-independent parent decisions through ADR-111. | +| 2026-09-23 | #1354 | Define IFC profile variability, requirement-relative support, per-obligation release and immutable migration under ADR-113. | diff --git a/docs/decisions/adrs/adr-113-ifc-profile-variability-and-publication.md b/docs/decisions/adrs/adr-113-ifc-profile-variability-and-publication.md new file mode 100644 index 000000000..bfa76723e --- /dev/null +++ b/docs/decisions/adrs/adr-113-ifc-profile-variability-and-publication.md @@ -0,0 +1,97 @@ +# ADR-113: IFC Profile Variability and Publication + +## Status + +accepted + +Acceptance takes effect when the delivery PR for +[#1354](https://github.com/OpenRAE/rae/issues/1354) merges. An unmerged copy is +proposed delivery state. This is a semantic decision, not new portable profile +support or runtime adoption. + +## Date + +2026-09-23 + +## Classification + +Classification: FM3 + +Required artifacts: [IFC-01–IFC-07](../../../specs/formal/participant-semantics/ifc-profile-variability.md), +[worked cases and bounded evidence](../../research/ifc-profile-variability/cases.md), +[finite interpretation](../../../implementations/python/tests/ifc_profile_variability_model.py), +[behavioral witnesses](../../../implementations/python/tests/test_issue_1354_ifc_profile_variability.py), +[migration obligations](../../migration/ifc-profile-variability.md), and +SEM-233/SEM-235 amendments. + +Waivers: the finite interpretation assumes trusted context and comparable +synthetic guarantee facts. It is not an installed engine, public negotiator, +wire reader, instrumentation proof or backend conformance result. No schema, +profile bytes, provider protocol or runtime implementation changes here. + +## Context + +The [preflight](../issue-1354-ifc-profile-variability-preflight.md) confirms that +SEM-233's product-powerset algebra already supports finite independent owner +obligations. The published digest-pinned security profile has a much smaller +fixed vocabulary. Shape-valid token additions do not pass publication +validation, and modular consumers recognize a closed profile/fact union. +Finiteness is not the problem; losing independent release distinctions is. + +ADR-108 permits governed domains without a general interpreter. CA-04 already +defines requirement-relative support, while current v1 composition rejects +non-exact support. Neither a declaration nor acceptance of weaker capability +proves that the authored requirement is satisfied. + +## Decision + +Adopt `ifc-profile-variability/rev1` under SEM-233 and SEM-235. Authors specify +required owner/release distinctions, scope and guarantees, directly or through +exact governed references. Profiles publish their meaning; backend configuration +binds realizations without changing that meaning. + +Use governed closed finite publication for additional justified distinctions. +Independent owners retain independent confidentiality and integrity obligations, +even with equal current audiences. Conservative joins, trusted authority for +every discharged obligation, fresh derived identities and immutable provenance +remain mandatory. Extensibility uses exact profile bindings and the existing +trusted source/sink/authority resolver seam. No owner-parameter syntax, policy +language or plugin facility is justified by these finite cases. + +Require separate evidence for expressibility and realization, then apply CA-04 +to the actual authored coverage and constraints. An admitted bounded guarantee +is legitimate where the requirement permits it; losing an admitted promise +during execution blocks the affected mandatory release and requires an explicit +new admission to change the promise. Authority to downgrade does not establish +satisfaction or remove another owner's obligation. + +Publish exact current limits and migration obligations. Independent-owner +examples are semantic witnesses, not new registered profiles. Adding tokens +requires coherent release correspondence, contracts, readers, capability, +runtime and backend evidence before any operational claim. Preserve ADR-101's +security meanings, ADR-108's declared-world boundary and CA-01–CA-09. + +## Alternatives Considered + +- Collapse every owner into `restricted`: conservative blocking can be a + disclosed limit, but cannot supply independently authorized selective sharing. +- Encode new meaning in backend configuration or audit names: cannot establish + portable profile semantics, complete propagation or per-obligation authority. +- Add arbitrary labels, callbacks or a policy/plugin language: the finite cases + need none; they would introduce interpretation and executable authority. +- Adopt owner parameters immediately: potentially useful for repeated finite + deployments, but needs a concrete unmet case and a separate closed binding + contract. This decision leaves that justified extension possible. +- Treat all bounded support as success, or every bounded guarantee as runtime + failure: both ignore the requirement and the guarantee actually admitted. + +## Consequences + +The support boundary becomes reviewable: a valid requirement can be refused +because no profile expresses it, because no backend realizes it, or because +an admitted guarantee was lost. Supported policy denial remains a different +outcome. Historical records retain their original evidence and limitations. + +The cost of new variability is governed publication and coordinated consumer +adoption. This decision neither certifies a contextual encoding of independent +owners under the legacy vocabulary nor broadens existing implementation claims. diff --git a/docs/decisions/adrs/adr-index.yaml b/docs/decisions/adrs/adr-index.yaml index 4bff78905..339213a83 100644 --- a/docs/decisions/adrs/adr-index.yaml +++ b/docs/decisions/adrs/adr-index.yaml @@ -566,11 +566,14 @@ adrs: pin: b7e17e58fc01e8f07a972ee5abc65e6a8470e2a6d51c2480334a3777df079e98 - id: ADR-101 path: docs/decisions/adrs/adr-101-adversarial-participant-flow-control.md - pin: 7d613beae8ae50e3232a07be1eedd5db422f252a728f34597d0c5dac65086164 + pin: f2482abc411d1ac00e22e97310a979e8c4f0e5d2536a970636dda6db9e0d4016 amendments: - date: 2026-09-06 ref: "#1068" summary: "Clarify modular composition, governed effects and the declared-world boundary under ADR-108 while preserving the security profile and runtime interpreter non-goal." + - date: 2026-09-23 + ref: "#1354" + summary: "Define IFC profile variability, requirement-relative support, per-obligation release and immutable migration under ADR-113." - id: ADR-102 path: docs/decisions/adrs/adr-102-mixed-cross-backend-participant-control.md pin: cfcb0f5b7291b47fe6ff6096bb18dd9063b83ee5d4f7f6a9cafbdd06f21bf716 @@ -622,11 +625,14 @@ adrs: summary: "Narrowed the scope to connected single-maintainer OSS development and ordinary release recovery; retained the original design as history." - id: ADR-108 path: docs/decisions/adrs/adr-108-modular-participant-control-and-governed-effects.md - pin: 7df063f96f2732f10ba7a6129ea21ad40caa7fb5dfd2f3bbd9f9245cf05b3fff + pin: 590dbfba1b7e47b0f46271f38af4e2c56bb82d1265d193dbee6e532928e0a833 amendments: - date: 2026-09-22 ref: "#1352" summary: "Clarify applicability, dependency invocation, support and phase-independent parent decisions through ADR-111." + - date: 2026-09-23 + ref: "#1354" + summary: "Define IFC profile variability, requirement-relative support, per-obligation release and immutable migration under ADR-113." - id: ADR-109 path: docs/decisions/adrs/adr-109-participant-identity-and-objective-assignment.md pin: 859172f6b8791577059a3215af639210e86267455c8a059f71168e621c0f9c61 @@ -643,3 +649,6 @@ adrs: - id: ADR-112 path: docs/decisions/adrs/adr-112-external-inject-triggering-and-execution.md pin: 65e54addfb3a2dba74941f3c8030dec8c7a39661cc5aebb456e59c03af120ea3 + - id: ADR-113 + path: docs/decisions/adrs/adr-113-ifc-profile-variability-and-publication.md + pin: d5597eaad5df23dd012904fdd2454b13d051ee90c983bcc694342d21ba3e36b2 diff --git a/docs/decisions/issue-1354-ifc-profile-variability-preflight.md b/docs/decisions/issue-1354-ifc-profile-variability-preflight.md new file mode 100644 index 000000000..dc9a69a3c --- /dev/null +++ b/docs/decisions/issue-1354-ifc-profile-variability-preflight.md @@ -0,0 +1,261 @@ +# Issue #1354 — IFC profile variability and publication preflight + +Date: 2026-09-23. Inspection baseline: `ddba5049`. +Scope: architecture guidance for the issue contract; not an accepted semantic +decision, implementation plan, new profile or fulfillment claim. The supplied +issue assigns SEM-233 and SEM-235; the supplied SEM-235 payload is sufficient +requirement context. + +## Observed boundary + +The issue's diagnosis was read from this repository's Git object +`077f7d04:docs/research/runtime-refactor/diagnosis.md`, section 5; it is absent +from the working tree. Its narrow finding agrees with current sources: +the general algebra is more expressive than the published security vocabulary. +It does **not** establish that independently resolved policy/provenance cannot +enforce any owner distinctions outside the label vocabulary. + +Paths beginning with package names below are relative to +`implementations/python/packages/`. + +| Incumbent | Actual limit that the decision must account for | +| --- | --- | +| [SEM-233](../../specs/formal/participant-semantics/adversarial-flow-control.md), exact revision-1 algebra | `P(C) × P(I)`, independent obligations and union propagation already permit finite owner-relative clauses. Finiteness is not the expressiveness defect; collapsing independently releasable obligations is. | +| [Published security artifact](../../contracts/profiles/participant-boundary-flow-policy/participant-boundary-flow-policy-v1.json) | Confidentiality has exactly `restricted`, `unknown`; integrity has exactly `endorsed`, `unknown`, `untrusted` (each with its coordinate prefix). There are no independent owner tokens. `unknown` is unresolved, not a spare owner slot; `endorsed` is not an owner identity or a global trust rank. | +| `raes_contracts/contracts/participant_flow_control_semantics.py` and `raes_contracts/participant_flow_policy_profiles.py` | Profile ID, revision and authority are fixed; the model checks the exact published digest and the loader resolves an allowlisted ID/revision/digest tuple. The schema's 128-token array limits do not authorize new tokens. There is no latest-version fallback. | +| `raes_contracts/contracts/participant_control_profiles.py`, `participant_control_results.py`, `participant_control_composition.py` | Modular validation recognizes only the security and teaching revision-1 profiles. IFC facts are a closed union of the SEM-233 relation reference and teaching tokens; domain-to-profile dispatch is specialized. A generic artifact reference does not grant new domain support. | +| API-407/API-424 `raes_backend_protocols/participant_feature_admission.py` and `participant_control_admission.py`; `ControlEffectiveSupportModel` and `_support_blockers` in `raes_contracts/contracts/participant_control_results.py` and `participant_control_composition.py` | Strength/evidence negotiation already exists. Current v1 composition nevertheless blocks every non-exact effective support record. [CA-04](../../specs/formal/participant-semantics/control-applicability-and-evaluation.md#ca-04--support-is-relative-to-the-requirement) defines requirement-relative bounded satisfaction, but publication of that amendment did not implement it. | + +Profile support therefore spans the loader, literal identity/revision fields, +relation/context validators, modular selection and fact dispatch, capability +admission, runtime binding and history readers. A new artifact or relaxed digest +check alone cannot extend this chain. API-407's existing strength rank is a +declaration check, not proof of CA-04 coverage or comparable loss constraints. +Name any needed API-424/RUN-320 adoption separately from this issue's semantic +publication; do not repair their reducers incidentally under SEM-235. + +A read-only probe at this baseline confirmed that the original security +artifact passes model validation, adding `confidentiality:owner-a` passes its +JSON Schema but fails the profile model, and an unknown modular profile is +rejected. Shape validity is not publication or semantic admission. The finite +SEM-233 test model uses richer synthetic universes under revision-1 names; +those witnesses are algebra evidence, not additional published profiles. + +`ParticipantFlowReleaseAuthorityCoordinate` currently identifies release kind, +authority/revision and sink/destination/audience, without an owner-token scope. +A multi-owner support claim must establish where trusted resolution proves +authority over each discharged obligation. Adding tokens alone cannot establish +that authorization relation. + +There is also a semantic/wire distinction to resolve explicitly: SEM-233's +algebra describes endorsement as removing named integrity obligations, while +`ParticipantFlowEndorsementModel` requires nonempty source-to-result token +replacements and `validate_release` checks that exact delta. The accepted +decision must explain how its endorsement cases map to that carrier, or name +the separate contract change needed. Do not reinterpret historical +`integrity:endorsed` as proof of every owner's endorsement. + +## Decision constraints and separating cases + +Keep three owners explicit in the eventual decision: + +| Boundary | Information it must retain | +| --- | --- | +| Authored intent | Whose independent obligations apply, protected sources, permitted readers/destinations/sinks, relevant possible writers and endorsement requirements, release authority, memory scope, required coverage/guarantee and admissible loss. Selecting a profile may supply these through an exact governed reference; authors need not write a policy language. An author assertion alone grants no release authority. | +| Published semantic profile | Meaning of its carrier/tokens or any explicitly justified parameters; canonical encoding, order/join, source/default and sink relations, release/non-influence rules, memory scope, unknown behavior and exact support limits. Keep semantic identity distinct from schema version, selected policy, provider identity and configuration. | +| Backend/operator configuration | Installed mechanism, concrete source/principal/sink bindings, instrumentation and covered flow classes, resources, implementation/configuration pins and realization evidence. Configuration realizes published meaning; it cannot silently supply a different owner algebra or weaken authored obligations. | + +The decision must resolve the following cases, with expected refusal/release +and retained provenance. These are semantic examples, not proposed syntax: + +- **Independent confidentiality owners:** A permits readers Alice and Bob; + B permits Bob and Carol. A derived value influenced by both retains both + clauses; its audience must satisfy both, so only Bob is common. A's release + may relax A's clause, never B's. Equal current reader sets do not make two + owners equivalent: their release authorities can still differ. Union of + obligations must not become union of allowed readers. +- **Independent integrity obligations:** a proposal influenced by A's + approved publisher and B's unreviewed feed retains both possible influences. + An action sink requiring each origin's review cannot be satisfied by A's + endorsement of A's contribution alone. An intentionally permissive + observation sink may admit B's known untrusted contribution without + endorsement; a later action keeps that influence and checks its own policy. + Endorsement never changes confidentiality or erases writer provenance. +- **Opaque combination and selective release:** summary, parse, redaction, + trusted edit, shared state, handoff and retained memory carry every possible + input obligation. Excluding an input needs the published non-influence + relation and evidence. Release binds exactly the discharged obligations, + coordinate, source/result, authority, sink/destination, revision and cut; + naming an authority is not proof that it controls all owners' clauses. +- **Expressible but unrealizable:** distinguish a profile that cannot encode + the required owner/release distinction from a profile that can, but whose + installed backend misses a required source, native/control flow or final + sink. Both prevent a claim of support; neither becomes an ordinary policy + denial or a successful downgraded execution merely by changing its label. + +For each case, establish whether the existing profile plus independently +trusted contextual policy preserves the distinction, a new governed finite +profile is needed, or the requirement remains unsupported. If an encoding +coarsens labels, demonstrate preservation through derivation, independent +release and every required sink; retaining owner names only in audit text is +insufficient. Conservative over-restriction can be an explicitly admitted +limit, but is not exact expressiveness or permission to ignore functional +requirements. Lost owner information cannot be reconstructed from `restricted`. + +The natural extension seam is the **exact published profile binding and its +trusted source/sink/authority resolver**, consumed by the existing API-424 +selection and backend protocol. A new governed finite publication remains a +valid outcome. If the next independent owner would require duplicating an +otherwise identical profile, evaluate a bounded, typed parameter binding at +that seam; require demonstrated need, admitted principal scope, canonical +identity, complete validation and explicit consumer support before adopting +it. Do not preselect a new parameter syntax or replace publication with dynamic +discovery. Unknown IDs, tokens, revisions and comparisons remain unsupported. +Any owner parameter must resolve to an admitted principal identity, never an +unchecked display name, HTTP role or token prefix. Its finite scope and bindings +are semantic inputs: changing them requires a new admitted binding and cut, +not an unrecorded backend configuration edit. + +Preserve MPC-04's general domain contract: a closed carrier with canonical +encoding, partial order and a total, associative, commutative, idempotent, +monotone conservative join. SEM-233's powerset union is its security +specialization; do not require every domain to use sets or a least upper bound. +Failure status remains outside the carrier; unresolved source coverage is +never an empty known input or permission to produce bottom. + +Reuse CA-01–04's obligation coverage and support relation. Keep required, +declared, installed, effective and observed guarantees separate. An admitted +bounded requirement can accept evidenced support within those exact bounds; +a weaker result than the admitted guarantee is an execution failure/weakening +that blocks the affected mandatory release. A downgrade authorization does +not prove satisfaction. A changed requirement/profile needs a separately +authorized binding at a new cut and disclosed claim limits, preserving every +other owner's obligation. Optional advice is not a mandatory IFC guarantee. +There is no universal loss scale that makes two unrelated limitations comparable. + +The same profile decision must preserve the rest of CA-01–CA-09: + +- Keep the admitted apparatus distinct from profile obligations and the + exact-cut invocation subset. Required coverage is derived independently of + provider responses; omission, failure and `None` never prove inapplicability. + Shared results retain every selecting owner's conjunction. +- Use the finite typed slot/stage DAG and immutable predecessor results, not + one call per provider or ambient shared results. Close mandatory work over + required inputs without giving negative advisory content veto authority. + Optional rejection discards its state/effects at that invocation boundary; + it cannot hide failed mandatory coverage. A false trigger needs evidence. +- Scope provider state by the admitted instance, configuration, authority and + sharing domain. A profile id alone is not a cache/state key. Coverage, + decisions, accepted state, effect intents and consumed budgets share one + atomic commit; unsupported shared-scope atomicity prevents admission. +- Parent deny/withhold has the same meaning in every phase. Prerequisites, + success-dependent effects and independent consequences have separate + targets, authorities and outcomes; their combined event graph must be acyclic. + An independent audit may follow denial without releasing the parent. + Transforms/injects retain fresh identity, visibility, provenance, ordinary + downstream admission and finite causal budgets across retries and resets. + +## Cross-cutting gates and canonical owners + +This preflight creates no executable surface. The publication decision must +identify applicability of each layer below; later consumers cannot claim +support by modifying only a profile file or one validator. + +| Layer / incumbent | Required treatment | +| --- | --- | +| Ingress and shape: `raes_contracts/json_ingress.py::parse_bounded_json_object`, `ContractModel`, flow-profile loader, `parse_participant_control_evaluation`; HTTP `RequestSizeLimitMiddleware` | Reuse bounded reads, duplicate-member/non-finite rejection, closed models and `raes_contracts/canonical.py` digests. Bound any new owner/token/graph cardinality and decoding depth explicitly; the profile loader currently bounds bytes, while the evaluation parser also passes depth 32. Resolve packaged artifacts through `raes_contracts/corpus.py::corpus_family_root`, retaining exact-ID/path allowlists; no participant-selected file/URL, second JSON parser or open label/config map. | +| Semantic and contextual validation: `participant_flow_control_validation.py`, `participant_flow_control_profile_validation.py`, `participant_control_resolution.py` in `raes_contracts/contracts` | Resolve the exact published artifact, trusted source labels, policy cuts, per-obligation release authority, safe refs and sinks independently of provider/caller claims. Retain structural, algebra and contextual checks as distinct layers. Reuse API-409/API-423 occurrence validation and ordinary action admission. Schema-only acceptance cannot replace any of them. | +| Authentication and policy: `raes_runtime/control_plane_api/_auth.py`, `control_plane_security.py`, participant crossing policy/state-cut validators | Preserve verified principal/role/target and audience binding. HTTP/operator authority, declared-world owner identity, controller authority, declassification and endorsement are different relations. Profiles grant no credentials or runtime rights. Recheck all applicable gates at the exact cut; profile selection cannot suppress another owner's constraint. | +| Capability/configuration: API-407/API-424 resolvers above; `raes_contracts/contracts/experiment_bindings.py`, participant manifests, `raes_contracts/participant_configuration.py::realize_participant_configuration` | Reuse governed feature terms, required contract sets, installed bindings, evidence and limitations. Use existing target registries, aliases, value types, defaults and complete same-type normalization where configuration is required. A configuration digest or generic modular-control feature does not prove exact domain/owner/sink coverage. No second strength ranking or per-profile admission workflow. | +| Secrets and environment: `raes_contracts/secret_references.py`, experiment binding models, `raes/runtime_environment.py`, `runtime_values.py`, `raes_runtime/runtime_fact_dispatch.py` | Carry only authorized logical secret references at their owning boundary; secret configuration targets permit neither raw literals nor portable defaults. Environment bindings retain literal/`value_from` exclusivity, generated-artifact ownership and observed-value redaction; an in-band generated value cannot claim `operator_secret`. Keep resolved credentials/private state out of profiles, examples, portable evidence and digests. Hashing a low-entropy secret is not redaction. IFC tokens are not runtime sensitivity classifications. | +| Runtime and host: `ParticipantControlProvider` in `raes_backend_protocols/protocols.py`; `raes_runtime/participant_control_binding.py`, `participant_control_orchestration.py`, `participant_flow_sink.py`, `RuntimeTarget` and backend call contracts | Providers remain operator-constructed and effect-free during resolution. Reuse exact admitted-selection/cut checks, re-entry fences and final checks before external calls, serialization, stream chunks, writes, callbacks and errors. No scenario imports, URLs, commands or executable policy. Any later backend binding must protect credentials from argv, environment dumps, filenames and stdout/stderr. Host/process/tenant isolation is backend responsibility outside the declared world; finite graph bounds and re-entry protection are not timeouts or a sandbox. | +| Errors and observability: `StrictJsonIngressError`, bounded resolver `ValueError`, `Diagnostic`/`DiagnosticModel`, `AuditEvent`, `participant_control_diagnostics.py`, conformance `sanitized_failure_message`, HTTP `_operation_routes.py` | Preserve coarse value-safe refusal reasons and safe evidence refs through existing envelopes/loggers, including redacted 422/500 paths. Never return raw Pydantic inputs or provider exceptions. Even owner names, refusal existence and provenance refs may disclose information; project them through SEM-230 audience rules and disclose timing/undeclared-channel limits. Logs are not experimental evidence, and a denied disclosure must not retain a successful durable outcome. | +| Persistence and replay: ADR-104 `ControlPlaneStore`/`AtomicControlPlaneStore`, `commit_participant_transition`, runtime snapshots and `participant_control_evaluation_history.py` | Retain one expected-head/revision commit authority for evaluation, state and intents before dispatch. Preserve source labels, bindings, releases, effect identities, receipts and consumed budgets. No profile-specific repository, side journal or mutable cache as authority. Uncertain external effects stay indeterminate; commit does not prove application or exactly-once execution. | + +Do not conflate this profile family with GOV-920 interoperability profiles in +`specs/concept-authority/semantic-profiles.md`, private `DomainProfileBindingModel` +selections, validation profiles, or plan-realization profiles. Those incumbents +offer publication/binding patterns, not authorization to admit arbitrary IFC +domains through their extension points. Package ownership stays contracts/data +in `raes_contracts`, protocol in `raes_backend_protocols`, orchestration in +`raes_runtime`, and concrete instrumentation in each backend. + +## Publication, migration and evidence obligations + +When #1354's decision is accepted, publish it in the existing authorities. +Amend SEM-233 and SEM-235 where it changes or clarifies their obligations; +retain their separate authority and historical scope. ADR-101 remains the +security decision; ADR-108 remains the modular publication/declared-world +boundary. Reconcile CA-04 rather than publishing a competing support relation. +Under ADR-059, changes to accepted ADRs require an in-band amendment plus +matching `docs/decisions/adrs/adr-index.yaml` entry/pin, or explicit supersession. +This preflight does not amend those accepted artifacts. + +The accepted publication must enumerate expressible cases, unsupported cases, +supported source/flow/sink/release coverage, finite bounds and evidence limits. +Separate semantic publication, portable reader support, installed mechanism, +effective realization and assurance; no ACTIVE status or conformance promotion +from prose or a finite model alone. + +Preserve old profile bytes/digests and historical interpretations. New readers +must select exact supported interpretations; old readers reject unfamiliar +ones. Conversion records source/target pins, authority, mapping, loss and +unrecoverable distinctions. Never retag old `restricted` values as owner-aware, +rerun historical releases under new rules, or replay old effects as new work. +Explicitly cover pending work, retained memory, provider state, snapshots, +mixed-revision histories and cross-profile comparison; absent a published +authorized mapping, comparison or conversion remains unsupported. Reuse the +[applicability migration boundary](../migration/control-applicability-and-evaluation.md) +for new-cut admission, reconciliation and preservation of effect keys/budgets. + +If contracts are actually required by the accepted decision, reuse ADR-009/061: +hand-governed schemas, `contracts/schema-publication-manifest.json` and its +per-contract entries/`last_change`, fixtures, exports, `schema_bundle()` parity +and the `implementations/python/pyproject.toml` packaged-corpus configuration. +Draft schema stability does not authorize silent reinterpretation. Use +`contracts/concept-authority/`, existing governed +vocabularies and `contracts/provenance/sdl-lineage-ledger-v2.json` for actual +concept/lineage changes, without speculative catalogs or a second registry. + +Evidence should build on `sem233_boundary_flow_model.py`, +`test_sem_233_adversarial_boundary_flow.py`, `test_sem_233_flow_control_contracts.py`, +the SEM-235/CA finite witnesses, `test_api_424_capability_admission.py`, and the +existing #1003/#1004 sink/capability tests. Distinguish algebra witnesses from +real parser/context/admission checks and from backend realization. Required +counterexamples include selective owner release, independent endorsement, +schema-valid unsupported profiles, bounds exceeded, missing context, stale +cuts, memory/replay laundering and unexpected weakening. Denied live paths +need zero prohibited calls/disclosures and consistent durable outcomes before +they support runtime claims. + +Workflow incumbents are `.ground-control.yaml`, `.gc/plan-rules.md`, +`tools/check_repo_policy.py`, `tools/check_requirement_governance.py`, +`tools/requirement_context.py`, `tools/policy/requirement_scope.py`, +`tools/policy/requirement_order.yaml`, `noxfile.py`, `.pre-commit-config.yaml` +and `.github/workflows/ci.yml`. Reuse `tools/check_adr_immutability.py`, +`tools/check_schema_publication.py`, `tools/check_generated_schemas.py`, +`tools/check_concept_authority_governance.py` and `tools/check_sdl_lineage.py` +when their artifacts change; do not create a profile-specific workflow. +Set `RAES_REQUIREMENT_UID=SEM-235` for this supplied requirement context. +Publication spanning SEM-233/235 must use the existing exact-path issue-scope +mechanism and phase ownership rules, not infer ownership from a title or bypass +the gate. + +Preflight verification: the file-local repo-policy check passes; 12 selected +existing contract/admission tests pass, including trusted-context rejection, +release deltas, sanitized resolver errors and non-exact support refusal. The +read-only schema/profile probes above confirm the vocabulary boundary. These +checks establish current behavior, not #1354 fulfillment. The explicit +SEM-235 requirement-governance check fails with +`requirement-ownership-mismatch`: this note is outside the mapped +`modular-control-semantics` ownership roots. That is a publication blocker to resolve +through the existing ownership/scope workflow; this guidance-only preflight +does not change policy allowlists or claim that gate passed. Local checks +remain file-targeted; full suites belong to CI. + +Non-goals: implementing #1354 here; choosing its final variability repertoire; +a general policy language, plugin host, new engine, duplicate schema/validator, +exception hierarchy, logger, state store or workflow; retroactive guarantee +upgrades; and claims of universal noninterference, covert-channel protection, +model trust or backend equivalence. New syntax requires a concrete unmet case +that existing governed publication and bindings cannot adequately express. diff --git a/docs/explain/reference/modular-participant-control-contracts.md b/docs/explain/reference/modular-participant-control-contracts.md index bb360175d..30e2eff04 100644 --- a/docs/explain/reference/modular-participant-control-contracts.md +++ b/docs/explain/reference/modular-participant-control-contracts.md @@ -28,6 +28,18 @@ effects. Its [worked cases](../../research/control-applicability/cases.md) and define the required interpretation and adoption checks. Existing schemas, provider/v1 and retained history keep their original meaning. +## IFC variability amendment (#1354) + +[ADR-113](../../decisions/adrs/adr-113-ifc-profile-variability-and-publication.md) +and [IFC-01–IFC-07](../../../specs/formal/participant-semantics/ifc-profile-variability.md) +define authored/profile/backend separation, per-obligation owner release and +requirement-relative support. The exact present support table identifies the +fixed security vocabulary, closed modular profile/fact union and current +non-exact-support rejection. This amendment registers no profile and changes +none of those consumers. Follow the +[migration contract](../../migration/ifc-profile-variability.md) before claiming +owner-aware interpretation or revised bounded-support adoption. + ## Published boundaries | Contract | Meaning | diff --git a/docs/governance/requirement-scopes/1354.json b/docs/governance/requirement-scopes/1354.json new file mode 100644 index 000000000..66643a0f1 --- /dev/null +++ b/docs/governance/requirement-scopes/1354.json @@ -0,0 +1,78 @@ +{ + "schema_version": "requirement-scope/v1", + "issue_number": 1354, + "primary_requirement_uid": "SEM-235", + "requirement_uids": [ + "SEM-235", + "SEM-233" + ], + "bindings": { + "docs/decisions/adrs/README.md": [ + "SEM-235" + ], + "docs/decisions/adrs/adr-101-adversarial-participant-flow-control.md": [ + "SEM-233" + ], + "docs/decisions/adrs/adr-108-modular-participant-control-and-governed-effects.md": [ + "SEM-235" + ], + "docs/decisions/adrs/adr-113-ifc-profile-variability-and-publication.md": [ + "SEM-235" + ], + "docs/decisions/adrs/adr-index.yaml": [ + "SEM-235" + ], + "docs/decisions/issue-1354-ifc-profile-variability-preflight.md": [ + "SEM-235" + ], + "docs/explain/reference/modular-participant-control-contracts.md": [ + "SEM-235" + ], + "docs/governance/requirement-scopes/1354.json": [ + "SEM-235" + ], + "docs/migration/ifc-profile-variability.md": [ + "SEM-235" + ], + "docs/requirements/SEM-233/requirement.md": [ + "SEM-233" + ], + "docs/requirements/SEM-235/requirement.md": [ + "SEM-235" + ], + "docs/research/ifc-profile-variability/cases.md": [ + "SEM-235" + ], + "implementations/python/tests/ifc_profile_variability_model.py": [ + "SEM-235", + "SEM-233" + ], + "implementations/python/tests/test_issue_1354_governance.py": [ + "SEM-235", + "SEM-233" + ], + "implementations/python/tests/test_issue_1354_ifc_profile_variability.py": [ + "SEM-235", + "SEM-233" + ], + "specs/formal/participant-semantics/README.md": [ + "SEM-235" + ], + "specs/formal/participant-semantics/adversarial-flow-control.md": [ + "SEM-233" + ], + "specs/formal/participant-semantics/ifc-profile-variability.md": [ + "SEM-235", + "SEM-233" + ], + "specs/formal/participant-semantics/modular-participant-control.md": [ + "SEM-235" + ], + "tools/policy/historical_identity_records.json": [ + "SEM-235" + ], + "tools/policy/requirement_order.yaml": [ + "SEM-235" + ] + } +} diff --git a/docs/migration/ifc-profile-variability.md b/docs/migration/ifc-profile-variability.md new file mode 100644 index 000000000..b674cffb0 --- /dev/null +++ b/docs/migration/ifc-profile-variability.md @@ -0,0 +1,91 @@ +# IFC profile variability migration + +This is the adoption contract for [ADR-113](../decisions/adrs/adr-113-ifc-profile-variability-and-publication.md) +and [IFC-01–IFC-07](../../specs/formal/participant-semantics/ifc-profile-variability.md). +It publishes no converter, schema, profile artifact or deprecation window. + +## Interpretation and historical data + +Keep the amendment identity `ifc-profile-variability/rev1` distinct from +`sem-233/rev1`, `sem-235/rev1`, profile revisions/digests and wire/protocol +versions. Do not infer adoption from new prose, a backend name or a generic +modular-control capability. Negotiate exact supported interpretations across +producer, resolver, provider, runtime, store, snapshot and downstream readers. + +| Input | Required treatment | +| --- | --- | +| Legacy security profile and relation | Retain exact original bytes, digest, token meaning, source context and release interpretation. Use the legacy reader with its stated limitations. | +| New owner-aware publication | Old readers reject it. New readers require exact publication, schema/content and semantic support, independently trusted bindings and per-obligation release authority. | +| Mixed-revision archive | Route each record through its exact supported reader; retain order and evidence. Unknown or ambiguous interpretation is unsupported/unverifiable, not latest-version fallback. | +| Coarse `restricted` value without owner evidence | Preserve it. Do not invent A/B obligations, map it to public/bottom or claim an owner-aware conversion. | +| Pending effect or retained memory under a replaced profile | Preserve the original identity, labels, provenance, cut, release and outcome records; apply the new-cut rules below before any new action. | + +Source and possible-writer provenance never disappears when an obligation is +discharged. Historical `integrity:endorsed` is interpreted by its original +profile and release record; it cannot become universal or per-owner endorsement. +Do not recompute historical permits, mutate labels or replay effects to make +an archive appear newly conforming. + +## Explicit conversion + +A future published mapping must name source and target profile/semantic/schema +pins, exact source/result identities, transformation authority, affected +coordinates, scope, losses and evidence. Establish that order and conservative +propagation, every required sink and independent release remain sound. Preserve +functional distinctions the author required, not only prohibition safety. +Cross-profile joins/comparisons are unsupported without that relation. + +Independent historical owner evidence may support a new derived value through +an authorized mapping; it does not authorize rewriting the source. If evidence +is incomplete, retain unsupported/unverifiable status. An explicit new author +decision may choose a different requirement, but it is a semantic change with +disclosed limits, not a lossless migration. Authorization cannot waive another +owner's unresolved obligation implicitly. + +For endorsement, reconcile the semantic discharge relation with the current +wire requirement for source-to-result token replacements. A future carrier or +mapping must preserve the unreleased owners and immutable writer provenance, +and prove exact authority over each changed obligation. Renaming `endorsed` +or adding a token to the legacy artifact does not provide that correspondence. + +## Live bindings, memory and pending work + +Reuse the [applicability migration contract](control-applicability-and-evaluation.md) +and existing operation lifecycle. Quiesce affected admission, finish or +explicitly reconcile pending claims, then admit a supported binding at a new +cut. Never swap profile interpretation inside a live evaluation. Revalidate +required coverage and guarantees before effects and disclosure; current v1's +non-exact support rejection cannot be bypassed by a migration flag. + +Retained participant memory and shared/provider state retain every possible +input obligation. Migration needs exact old/new state scopes, versions, +configuration/authority bindings and supported atomicity. Episode/controller +change and provider replacement do not erase dependencies. Unknown migration +coverage prevents affected release, even if a new profile would otherwise +accept its known tokens. + +Preserve effect identities, receipts, history heads, causal roots and consumed +budgets. A new profile is not a new retry key. A prior permit/release is not +authority at a new sink or cut. Indeterminate external effects remain +indeterminate until the existing owner/readback and recovery policy resolve +them; admission or commit is not evidence of application. Retaining a record +does not authorize automatic resumption or repeated dispatch. + +## Publication owners and adoption evidence + +SEM-233 owns the security invariant and owner-specific release meaning; +SEM-235 owns governed domain publication and composition. API-424 and the +incumbent flow-contract owners must coordinate closed carriers and protocol +consumers, using API-407 support evidence. RUN-320 owns modular orchestration +adoption; concrete backend instrumentation and assurance remain separately +evidenced. This issue changes none of those runtime fulfillment statuses. + +Use ADR-009/061 publication records, fixtures, generated-schema parity and +packaged resources. Preserve stable-contract compatibility; record permitted +draft changes without silently changing historical interpretation. Required +real-consumer evidence includes unknown profile/token rejection, shape-valid +but unpublished artifacts, two-owner selective declassification and endorsement, +missing source/sink/control-flow coverage, bounds exceeded, stale cuts, +unexpected weakening, mixed-revision replay and pending-effect reconciliation. +Denied live paths must show zero prohibited calls/disclosures and truthful +durable outcomes. The finite #1354 witnesses do not establish those live claims. diff --git a/docs/requirements/SEM-233/requirement.md b/docs/requirements/SEM-233/requirement.md index 2636a28f9..4d78216a7 100644 --- a/docs/requirements/SEM-233/requirement.md +++ b/docs/requirements/SEM-233/requirement.md @@ -6,7 +6,7 @@ type: FUNCTIONAL priority: MUST wave: 4 created_at: 2026-07-30T18:36:51.139346Z -updated_at: 2026-09-20T00:00:00Z +updated_at: 2026-09-23T00:00:00Z --- # SEM-233 — Adversarial Participant Boundary Information-Flow Control @@ -15,12 +15,44 @@ updated_at: 2026-09-20T00:00:00Z The ecosystem shall define revisioned participant-neutral boundary information-flow semantics with independent confidentiality and integrity coordinates, conservative provenance-preserving propagation across observations, retained memory, proposals, transformations, action arguments, control handoffs, participant crossings, outputs, and sinks; it shall keep authentication, authorization, admission, approval, declassification, integrity endorsement, redaction, and transformation distinct, and require fail-closed exact-cut mediation immediately before every RAES-controlled external effect or disclosure, including cross-participant and cross-episode flows. +Profile support shall distinguish authored obligations and admitted guarantees +from published profile expressibility and backend realization. Independent +owner-qualified confidentiality and integrity requirements shall retain every +required propagation and selective-release distinction; trusted authority +shall cover each discharged obligation. Unsupported expression or realization +shall prevent the affected mandatory release, and unexpected loss of an +admitted guarantee shall not silently weaken the effective binding. Governed +finite publication and exact historical interpretation shall follow +`ifc-profile-variability/rev1`; new syntax or executable extensibility requires +separate justification and supported consumers. + ## Rationale SEM-230 and the current action, control, crossing, and runtime authorities define participant-relative mediation but do not yet carry independent confidentiality and source-integrity coordinates transitively to the final enforceable sink or distinguish intentionally adversarial influence from ordinary invalid behavior. Issue #812 adopts that missing boundary while preserving participant neutrality and explicit nonclaims for opaque internals and covert channels. +## IFC publication amendment and evidence boundary + +[ADR-113](../../decisions/adrs/adr-113-ifc-profile-variability-and-publication.md) +and [IFC-01–IFC-07](../../../specs/formal/participant-semantics/ifc-profile-variability.md) +publish the #1354 semantic amendment, authoritative on merge. Existing ACTIVE +status and implementation/test links retain their original fulfillment scope. +The new finite witnesses are bounded design evidence, not new portable profile, +owner-aware runtime, installed backend or revised support-negotiation adoption. +The [migration obligations](../../migration/ifc-profile-variability.md) must be +met before claiming those meanings across contracts, live state or history. + ## Traceability +- IMPLEMENTS → GITHUB_ISSUE `1354` (IFC variability semantic decision; no runtime adoption) +- IMPLEMENTS → SPEC `specs/formal/participant-semantics/ifc-profile-variability.md` (IFC-01–IFC-07 semantic publication) +- IMPLEMENTS → ADR `docs/decisions/adrs/adr-113-ifc-profile-variability-and-publication.md` (Accepted-on-merge publication decision) +- DOCUMENTS → DOCUMENTATION `docs/decisions/issue-1354-ifc-profile-variability-preflight.md` (Architecture constraints and current support limits) +- DOCUMENTS → DOCUMENTATION `docs/research/ifc-profile-variability/cases.md` (Worked cases and bounded evidence) +- IMPLEMENTS → DOCUMENTATION `docs/migration/ifc-profile-variability.md` (Interpretation, conversion and adoption obligations) +- TESTS → TEST `implementations/python/tests/ifc_profile_variability_model.py` (Finite design interpretation; not runtime enforcement) +- TESTS → TEST `implementations/python/tests/test_issue_1354_ifc_profile_variability.py` (Owner, support and publication witnesses) +- TESTS → TEST `implementations/python/tests/test_issue_1354_governance.py` (Real requirement ownership and scope evaluator) + - DOCUMENTS → ADR `docs/decisions/adrs/adr-108-modular-participant-control-and-governed-effects.md` (Preserves SEM-233 security semantics within modular control) - DOCUMENTS → DOCUMENTATION `docs/research/modular-participant-control/requirements.md` (Issue #1068 reuse disposition; statement and ACTIVE status unchanged) diff --git a/docs/requirements/SEM-235/requirement.md b/docs/requirements/SEM-235/requirement.md index 8e5fe3887..21385e0c5 100644 --- a/docs/requirements/SEM-235/requirement.md +++ b/docs/requirements/SEM-235/requirement.md @@ -6,7 +6,7 @@ type: FUNCTIONAL priority: MUST wave: 4 created_at: 2026-09-06T00:00:00Z -updated_at: 2026-09-22T00:00:00Z +updated_at: 2026-09-23T00:00:00Z --- # SEM-235 — Modular Participant Control and Extensible Dynamic IFC Semantics @@ -38,6 +38,17 @@ constraints. Parent deny/withhold shall retain the same meaning in every phase; prerequisites and independent or success-dependent consequences shall have separate target, authority, outcome and ordering relations under CA-01–CA-09. +Profile support shall distinguish authored obligations and admitted guarantees +from published profile expressibility and backend realization. Independent +owner-qualified confidentiality and integrity requirements shall retain every +required propagation and selective-release distinction; trusted authority +shall cover each discharged obligation. Unsupported expression or realization +shall prevent the affected mandatory release, and unexpected loss of an +admitted guarantee shall not silently weaken the effective binding. Governed +finite publication and exact historical interpretation shall follow +`ifc-profile-variability/rev1`; new syntax or executable extensibility requires +separate justification and supported consumers. + ## Rationale SEM-230 supplies participant-relative flow and SEM-233 supplies its security @@ -65,8 +76,29 @@ model supplies bounded design evidence. Producers and historical readers must satisfy the [migration contract](../../migration/control-applicability-and-evaluation.md) before claiming the amended semantics. +## IFC publication amendment and evidence boundary + +[ADR-113](../../decisions/adrs/adr-113-ifc-profile-variability-and-publication.md) +and [IFC-01–IFC-07](../../../specs/formal/participant-semantics/ifc-profile-variability.md) +publish the #1354 semantic amendment, authoritative on merge. Existing ACTIVE +status and implementation/test links retain their original fulfillment scope. +The new finite witnesses are bounded design evidence, not new portable profile, +owner-aware runtime, installed backend or revised support-negotiation adoption. +The [migration obligations](../../migration/ifc-profile-variability.md) must be +met before claiming those meanings across contracts, live state or history. + ## Traceability +- IMPLEMENTS → GITHUB_ISSUE `1354` (IFC variability semantic decision; no runtime adoption) +- IMPLEMENTS → SPEC `specs/formal/participant-semantics/ifc-profile-variability.md` (IFC-01–IFC-07 semantic publication) +- IMPLEMENTS → ADR `docs/decisions/adrs/adr-113-ifc-profile-variability-and-publication.md` (Accepted-on-merge publication decision) +- DOCUMENTS → DOCUMENTATION `docs/decisions/issue-1354-ifc-profile-variability-preflight.md` (Architecture constraints and current support limits) +- DOCUMENTS → DOCUMENTATION `docs/research/ifc-profile-variability/cases.md` (Worked cases and bounded evidence) +- IMPLEMENTS → DOCUMENTATION `docs/migration/ifc-profile-variability.md` (Interpretation, conversion and adoption obligations) +- TESTS → TEST `implementations/python/tests/ifc_profile_variability_model.py` (Finite design interpretation; not runtime enforcement) +- TESTS → TEST `implementations/python/tests/test_issue_1354_ifc_profile_variability.py` (Owner, support and publication witnesses) +- TESTS → TEST `implementations/python/tests/test_issue_1354_governance.py` (Real requirement ownership and scope evaluator) + - IMPLEMENTS → GITHUB_ISSUE `1352` (Applicability, dependency and effect semantic amendment) - IMPLEMENTS → SPEC `specs/formal/participant-semantics/control-applicability-and-evaluation.md` (CA-01–CA-09 semantic contract; not runtime adoption) - IMPLEMENTS → DOCUMENTATION `docs/decisions/adrs/adr-111-control-applicability-and-effect-decisions.md` (Accepted-on-merge decision) diff --git a/docs/research/ifc-profile-variability/cases.md b/docs/research/ifc-profile-variability/cases.md new file mode 100644 index 000000000..b26e368fb --- /dev/null +++ b/docs/research/ifc-profile-variability/cases.md @@ -0,0 +1,92 @@ +# IFC profile variability: cases and evidence + +This is the bounded evidence record for [ADR-113](../../decisions/adrs/adr-113-ifc-profile-variability-and-publication.md) +and [IFC-01–IFC-07](../../../specs/formal/participant-semantics/ifc-profile-variability.md). +The examples use synthetic owners and references, not proposed SDL syntax or +new registered profile artifacts. + +## Independent owners + +A's confidentiality policy admits Alice/Bob; B's admits Bob/Carol. A derived +summary has both obligations. Its confidentiality outcomes are: + +| Reader | A's clause | B's clause | Joined summary | +| --- | --- | --- | --- | +| Alice | satisfied | unsatisfied | deny | +| Bob | satisfied | satisfied | permit if every other gate passes | +| Carol | unsatisfied | satisfied | deny | + +At an exact sink/cut, A may authorize a fresh derived result discharging A's +clause. B's remains, so Carol can then satisfy confidentiality while Alice +cannot. A cannot discharge B's clause. If both initially name the same reader +set, they still remain distinct because A and B may release independently. +Mapping both to one `restricted` token either loses that distinction or blocks +sharing the authored requirement demands. The current artifact does not +directly support this case; a new finite publication and coordinated consumers +are needed. This is not evidence that every contextual encoding is impossible. + +For integrity, independent possible influences create `{I_A, I_B}`. A's +endorsement of its contribution leaves `I_B`; an action requiring no unresolved +integrity obligations still denies. A deliberately permissive observation +policy can accept known B influence without endorsement, but that observation +does not delete B's influence from a later proposal. Confidentiality and writer +provenance remain unchanged. The model's discharge is semantic: the current +wire replacement carrier needs the explicit correspondence described by IFC-03 +before supporting an owner-aware publication. + +## Support and failure cases + +| Case | Expected decision and evidence | +| --- | --- | +| Two independent owners mapped to distinct known tokens in each coordinate | Expressible in the synthetic finite profile; still requires complete realization evidence. | +| Missing mapping, duplicate owner binding, collapsed owners, unknown token or unresolved token used as an owner | Unsupported expression. An unresolved token is not extra expressiveness. | +| Owner token added to the real v1 JSON | Shape-valid but rejected by exact published-profile validation. The original profile remains loadable and unchanged. | +| Complete encoding but missing source, memory path or required sink instrumentation | Unsupported realization. Profile membership cannot replace coverage. | +| Evidenced bounded explicit-boundary guarantee admitted by the requirement | Admissible semantic case; current v1 composition still rejects non-exact support. No runtime adoption is claimed. | +| Requirement demands an additional guarantee that the realization lacks | Refuse admission, regardless of downgrade authority. | +| Run admitted additional guarantees, then loses one while still meeting the earlier floor | Record weakened and block affected release; do not silently lower the promise. | +| Profile/configuration changes or evidence becomes unresolved | Unsupported current binding; independently admit a new binding at a new cut. | +| A's grant used for B, another source/profile, sink or cut | Refuse release; no obligation or history is rewritten. | +| Opaque combination, retained memory, handoff or episode change | Preserve both coordinates and provenance; unknown coverage never permits a sink. | + +The finite model uses independently trusted coverage and grants and a set of +comparable synthetic guarantee facts. It does not define a universal ordering +for arbitrary backend limitations or solve general contextual encodings. Its +singleton-token encoding fragment requires independent release, so mappings +must distinguish each required owner. Finiteness alone places no one-owner +limit on the SEM-233 algebra. + +## Verification and clause map + +`implementations/python/tests/ifc_profile_variability_model.py` reuses the +incumbent SEM-233 finite model for derivation, sink conjunction, coordinate +rewrites and immutable provenance. It adds a finite expression/admission check, +admitted-versus-observed comparison and scoped grants. The companion +`test_issue_1354_ifc_profile_variability.py` drives the separating cases above +and the actual published profile model/schema. These are behavioral checks, +not assertions that prose contains its own terminology. + +`test_issue_1354_governance.py` exercises the real requirement ownership and +issue-scope evaluators, including refusal to treat runtime implementation as +SEM-235 semantic-publication work. Its tests were observed failing before the +new exact-path ownership/scope data was added. The semantic tests were observed +failing before their finite interpretation existed; additional source/profile +grant cases exposed the missing grant binding before its repair. + +| Acceptance/requirement clause | Satisfying artifact and evidence | +| --- | --- | +| Issue: authored/profile/backend distinctions and owner-qualified cases | IFC-01–02; owner encoding, audience intersection and selective release tests. | +| Issue: unsupported expression/realization and admitted strength versus weakening | IFC-04–05 and support tests; CA-04 remains the canonical satisfaction relation. | +| Issue: conservative propagation, independent coordinates, release authority and provenance | IFC-02–03; scoped grant, endorsement, retained-memory tests and incumbent SEM-233 behavioral tests. | +| Issue: accepted decision, exact limits, requirement/ADR amendments and migration | ADR-113, IFC-06–07, SEM-233/235 and ADR-101/108 amendments; actual profile rejection, ownership/scope and ADR pin checks. | +| SEM-233: independent coordinates, propagation, authority distinctions and final-sink contract | Incumbent adversarial-flow-control.md and its existing contract/runtime links remain authoritative; IFC-01–07 clarify expressibility and publication without changing those implementations. | +| SEM-235: revisioned domains, joins, defaults, memory, release and finite composition | Incumbent MPC-01–MPC-15 remain; IFC-01–03/06 specialize publication limits and retain non-security domains. | +| SEM-235: coverage, dependencies, advice, bounded support, atomic state and effects | CA-01–CA-09 remain; IFC-04–05 explicitly compose with them. Existing #1352 finite witnesses exercise those retained clauses; no runtime fulfillment upgrade. | +| SEM-235: fresh transformations/injects, visibility, provenance, admission and budgets | Incumbent MPC-09–MPC-14 and CA-05–CA-09 remain; IFC-05/07 and migration preserve them across profile changes. | + +Local verification uses only the new focused modules, relevant existing +SEM-233/#1352 modules and changed-artifact policy checks. Full suites remain in +CI. New backend adoption still requires the real consumer evidence listed in +the migration contract: the finite model proves no live mediation, portable +owner-aware reader, arbitrary noninterference, durable atomicity, recovery, +intentional-subversion robustness or installed backend capability. diff --git a/implementations/python/tests/ifc_profile_variability_model.py b/implementations/python/tests/ifc_profile_variability_model.py new file mode 100644 index 000000000..d6864b01e --- /dev/null +++ b/implementations/python/tests/ifc_profile_variability_model.py @@ -0,0 +1,132 @@ +"""Finite IFC-01–IFC-07 design projection, not a provider or wire contract. + +The encoding fragment has independently releasable obligations and singleton +tokens. It is not a solver for arbitrary conservative contextual encodings. +Coverage, grants and guarantee facts are independently trusted inputs; set +inclusion represents only comparable guarantees in this synthetic experiment. +""" + +from dataclasses import dataclass + +from sem233_boundary_flow_model import FlowProfile, UnsupportedFlow, rewrite_coordinate + + +@dataclass(frozen=True) +class Requirement: + confidentiality: frozenset[str] + integrity: frozenset[str] + coverage: frozenset[str] + guarantees: frozenset[str] + + +@dataclass(frozen=True) +class Encoding: + profile: FlowProfile + confidentiality: tuple[tuple[str, str], ...] + integrity: tuple[tuple[str, str], ...] + digest: str = "digest:synthetic-owner-publication" + + @property + def pin(self): + return self.profile.profile_id, self.profile.profile_revision, self.digest + + +@dataclass(frozen=True) +class Support: + profile_pin: tuple[str, str, str] + configuration: str + coverage: frozenset[str] + guarantees: frozenset[str] + resolved: bool = True + + +def _expresses(required, pairs, universe, unresolved): + mapping = dict(pairs) + if len(mapping) != len(pairs) or not required <= mapping.keys(): + return False + targets = {mapping[item] for item in required} + return len(targets) == len(required) and targets <= universe - {unresolved} + + +def admit(requirement, encoding, support): + """Project expressibility then CA-04 realization; no effect is dispatched.""" + profile = encoding.profile + if not ( + _expresses( + requirement.confidentiality, + encoding.confidentiality, + profile.confidentiality_universe, + "conf:deny-unresolved", + ) + and _expresses(requirement.integrity, encoding.integrity, profile.integrity_universe, "int:deny-unresolved") + ): + raise UnsupportedFlow("expression unsupported") + if not ( + support.resolved + and support.profile_pin == encoding.pin + and support.configuration + and requirement.coverage <= support.coverage + and requirement.guarantees <= support.guarantees + ): + raise UnsupportedFlow("realization unsupported") + return support + + +def check_execution(admitted, observed): + if not observed.resolved or (observed.profile_pin, observed.configuration) != ( + admitted.profile_pin, + admitted.configuration, + ): + return "unsupported" + if not admitted.coverage <= observed.coverage or not admitted.guarantees <= observed.guarantees: + return "weakened" + return "resolved" + + +@dataclass(frozen=True) +class Grant: + authority: str + confidentiality: frozenset[str] + integrity: frozenset[str] + sink: str + cut: str + source: str + profile: tuple[str, str] + + +def release( + profile, + source, + grant, + *, + result_ref, + operation, + confidentiality=frozenset(), + integrity=frozenset(), + sink="sink:action", + cut="cut:1", +): + """A trusted exact-context grant must cover every discharged obligation. + + The reused algebra checks fresh identity, operation/coordinate separation, + membership and immutable provenance. Grant acquisition is outside this model. + """ + if not ( + (grant.sink, grant.cut) == (sink, cut) + and grant.source == source.value_ref + and grant.profile == (profile.profile_id, profile.profile_revision) + and confidentiality <= grant.confidentiality + and integrity <= grant.integrity + ): + raise UnsupportedFlow("release authority does not cover the exact obligation and cut") + return rewrite_coordinate( + profile, + source, + result_ref=result_ref, + operation=operation, + remove_confidentiality=confidentiality, + remove_integrity=integrity, + authority_ref=grant.authority, + sink_ref=sink, + state_cut_ref=cut, + ) diff --git a/implementations/python/tests/test_issue_1354_governance.py b/implementations/python/tests/test_issue_1354_governance.py new file mode 100644 index 000000000..902f5697f --- /dev/null +++ b/implementations/python/tests/test_issue_1354_governance.py @@ -0,0 +1,38 @@ +"""Exercise the real governance consumer for the IFC semantic publication.""" + +from paths import REPO_ROOT +from tools.policy.repository_requirements import RepositoryRequirementClient +from tools.policy.requirement_governance import evaluate_requirement_governance +from tools.policy.requirement_scope import evaluate_requirement_scope, load_requirement_scope + + +def test_ifc_publication_has_exact_semantic_ownership(): + client = RepositoryRequirementClient(REPO_ROOT) + paths = [ + "docs/decisions/issue-1354-ifc-profile-variability-preflight.md", + "specs/formal/participant-semantics/ifc-profile-variability.md", + "implementations/python/tests/ifc_profile_variability_model.py", + "implementations/python/tests/test_issue_1354_ifc_profile_variability.py", + ] + assert evaluate_requirement_governance(REPO_ROOT, paths, client=client, requirement_uid="SEM-235") == [] + failures = evaluate_requirement_governance( + REPO_ROOT, + ["implementations/python/packages/raes_runtime/participant_control_orchestration.py"], + client=client, + requirement_uid="SEM-235", + ) + assert any(f.rule_id == "requirement-ownership-mismatch" for f in failures) + + +def test_issue_scope_validates_both_owners_without_runtime_authority(): + scope = load_requirement_scope(REPO_ROOT, "1354-ifc-profile-variability") + assert scope is not None + client = RepositoryRequirementClient(REPO_ROOT) + assert evaluate_requirement_scope(REPO_ROOT, list(scope.bindings), client=client, scope=scope) == [] + failures = evaluate_requirement_scope( + REPO_ROOT, + ["implementations/python/packages/raes_runtime/participant_control_orchestration.py"], + client=client, + scope=scope, + ) + assert any(f.rule_id == "requirement-scope-unassigned" for f in failures) diff --git a/implementations/python/tests/test_issue_1354_ifc_profile_variability.py b/implementations/python/tests/test_issue_1354_ifc_profile_variability.py new file mode 100644 index 000000000..e413d94e5 --- /dev/null +++ b/implementations/python/tests/test_issue_1354_ifc_profile_variability.py @@ -0,0 +1,279 @@ +"""Bounded #1354 witnesses; synthetic owner profiles are not published support.""" + +from dataclasses import replace + +import pytest +from ifc_profile_variability_model import ( + Encoding, + Grant, + Requirement, + Support, + admit, + check_execution, + release, +) +from jsonschema import Draft202012Validator +from raes_contracts.contracts import ParticipantBoundaryFlowPolicyProfileModel, schema_bundle +from raes_contracts.participant_flow_policy_profiles import load_participant_boundary_flow_policy_profile +from sem233_boundary_flow_model import ( + FlowGateState, + FlowOperation, + FlowProfile, + FlowValue, + SinkPolicy, + UnsupportedFlow, + carry, + derive, + may_flow_at_sink, +) + +PROFILE = FlowProfile( + "example-owner-ifc", + "rev1", + "ifc-profile-variability/rev1", + frozenset({"conf:A", "conf:B", "conf:deny-unresolved"}), + frozenset({"int:A", "int:B", "int:deny-unresolved"}), +) +ENCODING = Encoding(PROFILE, (("A", "conf:A"), ("B", "conf:B")), (("A", "int:A"), ("B", "int:B"))) +REQUIREMENT = Requirement( + frozenset({"A", "B"}), + frozenset({"A", "B"}), + frozenset({"source:A", "source:B", "flow:memory", "sink:action"}), + frozenset({"explicit-boundary-flow"}), +) +SUPPORT = Support(ENCODING.pin, "configuration:1", REQUIREMENT.coverage, REQUIREMENT.guarantees) +GRANT_A = Grant( + "authority:A", + frozenset({"conf:A"}), + frozenset({"int:A"}), + "sink:action", + "cut:1", + "summary:AB", + (PROFILE.profile_id, PROFILE.profile_revision), +) + + +def value(owner): + return FlowValue( + f"value:{owner}", + PROFILE.label(confidentiality={f"conf:{owner}"}, integrity={f"int:{owner}"}), + frozenset({f"source:{owner}"}), + frozenset({f"writer:{owner}"}), + "participant:1", + "episode:1", + "policy:1", + "rev1", + "cut:1", + ) + + +def combined(): + return derive( + PROFILE, + result_ref="summary:AB", + inputs=(value("A"), value("B")), + participant_ref="participant:1", + episode_ref="episode:1", + policy_ref="policy:1", + policy_revision="rev1", + state_cut_ref="cut:1", + ) + + +def sink(confidentiality, integrity): + return SinkPolicy( + "sink:action", + "destination:1", + PROFILE.profile_id, + "rev1", + "policy:1", + "rev1", + "cut:1", + frozenset(confidentiality), + frozenset(integrity), + ) + + +def test_finite_owner_encoding_admits_only_evidenced_coverage(): + assert admit(REQUIREMENT, ENCODING, SUPPORT) == SUPPORT + for missing in REQUIREMENT.coverage: + with pytest.raises(UnsupportedFlow, match="realization"): + admit(REQUIREMENT, ENCODING, replace(SUPPORT, coverage=SUPPORT.coverage - {missing})) + with pytest.raises(UnsupportedFlow, match="realization"): + admit(REQUIREMENT, ENCODING, replace(SUPPORT, resolved=False)) + with pytest.raises(UnsupportedFlow, match="realization"): + admit(REQUIREMENT, ENCODING, replace(SUPPORT, guarantees=frozenset())) + + +@pytest.mark.parametrize("coordinate,prefix", [("confidentiality", "conf"), ("integrity", "int")]) +@pytest.mark.parametrize("bad_mapping", ["collapsed", "missing", "unknown", "unresolved", "duplicate"]) +def test_independent_obligations_cannot_be_collapsed_or_invented(coordinate, prefix, bad_mapping): + maps = { + "collapsed": (("A", f"{prefix}:A"), ("B", f"{prefix}:A")), + "missing": (("A", f"{prefix}:A"),), + "unknown": (("A", f"{prefix}:A"), ("B", f"{prefix}:C")), + "unresolved": (("A", f"{prefix}:A"), ("B", f"{prefix}:deny-unresolved")), + "duplicate": (("A", f"{prefix}:A"), ("A", f"{prefix}:B"), ("B", f"{prefix}:B")), + } + with pytest.raises(UnsupportedFlow, match="expression"): + admit(REQUIREMENT, replace(ENCODING, **{coordinate: maps[bad_mapping]}), SUPPORT) + + +def test_admitted_bounded_guarantee_is_distinct_from_unexpected_weakening(): + bounded = admit(REQUIREMENT, ENCODING, SUPPORT) + assert check_execution(bounded, SUPPORT) == "resolved" + stronger = replace(SUPPORT, guarantees=SUPPORT.guarantees | {"extra-instrumentation"}) + admitted_stronger = admit(REQUIREMENT, ENCODING, stronger) + # Still meeting the author's floor does not erase an admitted promise. + assert check_execution(admitted_stronger, SUPPORT) == "weakened" + assert check_execution(bounded, replace(SUPPORT, coverage=SUPPORT.coverage - {"flow:memory"})) == "weakened" + exact_required = replace(REQUIREMENT, guarantees=stronger.guarantees) + with pytest.raises(UnsupportedFlow, match="realization"): + admit(exact_required, ENCODING, SUPPORT) + + +@pytest.mark.parametrize( + "change", + [ + {"profile_pin": ("another-profile", "rev1", "digest:example")}, + {"configuration": "configuration:2"}, + {"resolved": False}, + ], +) +def test_changed_or_unresolved_binding_requires_new_admission(change): + assert check_execution(SUPPORT, replace(SUPPORT, **change)) == "unsupported" + if "profile_pin" in change: + with pytest.raises(UnsupportedFlow, match="realization"): + admit(REQUIREMENT, ENCODING, replace(SUPPORT, **change)) + + +@pytest.mark.parametrize( + "reader,obligations,expected", + [ + ("Alice", {"conf:A"}, False), + ("Bob", {"conf:A", "conf:B"}, True), + ("Carol", {"conf:B"}, False), + ], +) +def test_combination_intersects_permitted_readers(reader, obligations, expected): + destination = replace(sink(obligations, {"int:A", "int:B"}), destination_ref=reader) + assert may_flow_at_sink(PROFILE, combined(), destination, FlowGateState.allowing()) is expected + + +def test_selective_release_preserves_other_owner_coordinate_and_history(): + source = combined() + result = release( + PROFILE, + source, + GRANT_A, + result_ref="released:A", + operation=FlowOperation.DECLASSIFICATION, + confidentiality=frozenset({"conf:A"}), + ) + assert result.label.confidentiality == frozenset({"conf:B"}) + assert result.label.integrity == source.label.integrity + assert result.influence_refs == source.influence_refs + assert source.provenance_refs <= result.provenance_refs + assert source.label.confidentiality == frozenset({"conf:A", "conf:B"}) + assert may_flow_at_sink(PROFILE, result, sink({"conf:B"}, {"int:A", "int:B"}), FlowGateState.allowing()) + with pytest.raises(UnsupportedFlow, match="authority"): + release( + PROFILE, + source, + GRANT_A, + result_ref="release:B", + operation=FlowOperation.DECLASSIFICATION, + confidentiality=frozenset({"conf:B"}), + ) + + +def test_endorsement_is_owner_scoped_and_observation_does_not_clear_influence(): + source = combined() + result = release( + PROFILE, + source, + GRANT_A, + result_ref="endorsed:A", + operation=FlowOperation.ENDORSEMENT, + integrity=frozenset({"int:A"}), + ) + assert result.label.integrity == frozenset({"int:B"}) + assert result.label.confidentiality == source.label.confidentiality + assert result.influence_refs == source.influence_refs + assert not may_flow_at_sink(PROFILE, result, sink({"conf:A", "conf:B"}, set()), FlowGateState.allowing()) + assert may_flow_at_sink(PROFILE, result, sink({"conf:A", "conf:B"}, {"int:B"}), FlowGateState.allowing()) + assert result.label.integrity == frozenset({"int:B"}) + with pytest.raises(UnsupportedFlow, match="authority"): + release( + PROFILE, + source, + GRANT_A, + result_ref="endorse:B", + operation=FlowOperation.ENDORSEMENT, + integrity=frozenset({"int:B"}), + ) + + +@pytest.mark.parametrize("changes", [{"cut": "cut:2"}, {"sink": "sink:other"}]) +def test_release_authority_is_bound_to_exact_sink_and_cut(changes): + with pytest.raises(UnsupportedFlow, match="authority"): + release( + PROFILE, + combined(), + replace(GRANT_A, **changes), + result_ref="release:new", + operation=FlowOperation.DECLASSIFICATION, + confidentiality=frozenset({"conf:A"}), + ) + + +@pytest.mark.parametrize("changed", ["source", "profile"]) +def test_release_grant_cannot_be_reused_for_another_source_or_profile(changed): + source, profile = combined(), PROFILE + if changed == "source": + source = replace(source, value_ref="different:source") + else: + profile = replace(PROFILE, profile_id="different-profile") + source = replace(source, label=replace(source.label, profile_id=profile.profile_id)) + with pytest.raises(UnsupportedFlow, match="authority"): + release( + profile, + source, + GRANT_A, + result_ref="release:new", + operation=FlowOperation.DECLASSIFICATION, + confidentiality=frozenset({"conf:A"}), + ) + + +def test_retained_memory_and_unknown_inputs_cannot_launder_owner_obligations(): + source = combined() + retained = carry( + PROFILE, + source, + result_ref="memory:next", + participant_ref="participant:2", + episode_ref="episode:2", + policy_ref="policy:1", + policy_revision="rev1", + state_cut_ref="cut:1", + ) + assert retained.label == source.label + assert source.influence_refs <= retained.influence_refs + unknown = replace(retained, supported=False) + assert not may_flow_at_sink( + PROFILE, unknown, sink(PROFILE.confidentiality_universe, PROFILE.integrity_universe), FlowGateState.allowing() + ) + + +def test_schema_valid_owner_token_is_not_a_published_profile(): + original = load_participant_boundary_flow_policy_profile("participant-boundary-flow-policy-v1") + payload = original.model_dump(mode="json") + payload["confidentiality_obligation_refs"] = sorted( + [*payload["confidentiality_obligation_refs"], "confidentiality:owner-a"] + ) + schema = schema_bundle()["participant-boundary-flow-policy-v1"] + Draft202012Validator(schema).validate(payload) + with pytest.raises(ValueError, match="exact published"): + ParticipantBoundaryFlowPolicyProfileModel.model_validate(payload) + assert load_participant_boundary_flow_policy_profile(original.profile_id) == original diff --git a/specs/formal/participant-semantics/README.md b/specs/formal/participant-semantics/README.md index b0c19bedf..4a6d9b8b6 100644 --- a/specs/formal/participant-semantics/README.md +++ b/specs/formal/participant-semantics/README.md @@ -1,5 +1,11 @@ # Participant Semantics Formal Design +Issue #1354 and ADR-113 publish [IFC profile variability and publication](ifc-profile-variability.md). +The amendment separates authored requirements, exact profile expressibility +and evidenced realization, preserving this document's original revision and +implementation boundary. It adds no registered owner-aware profile or runtime +support; its migration contract governs future adoption. + Issue #1352 and ADR-111 publish the [control applicability and evaluation amendment](control-applicability-and-evaluation.md) for SEM-235/API-424. Its bounded model tests the semantic decision; the linked diff --git a/specs/formal/participant-semantics/adversarial-flow-control.md b/specs/formal/participant-semantics/adversarial-flow-control.md index f90980486..5c34454a3 100644 --- a/specs/formal/participant-semantics/adversarial-flow-control.md +++ b/specs/formal/participant-semantics/adversarial-flow-control.md @@ -1,5 +1,11 @@ # SEM-233 And ASR-536 Adversarial Participant Flow Control +Issue #1354 and ADR-113 publish [IFC profile variability and publication](ifc-profile-variability.md). +The amendment separates authored requirements, exact profile expressibility +and evidenced realization, preserving this document's original revision and +implementation boundary. It adds no registered owner-aware profile or runtime +support; its migration contract governs future adoption. + Status: SEM-233 definition and portable-contract authority are published; runtime, backend, and ASR-536 evaluation obligations remain DRAFT. diff --git a/specs/formal/participant-semantics/ifc-profile-variability.md b/specs/formal/participant-semantics/ifc-profile-variability.md new file mode 100644 index 000000000..24a7b05d3 --- /dev/null +++ b/specs/formal/participant-semantics/ifc-profile-variability.md @@ -0,0 +1,190 @@ +# IFC profile variability and publication + +Semantic amendment: `ifc-profile-variability/rev1`, owned by SEM-233 and +SEM-235, issue #1354 and [ADR-113](../../../docs/decisions/adrs/adr-113-ifc-profile-variability-and-publication.md). +This defines publication and support obligations. It registers no new portable +profile, authoring syntax, provider protocol or runtime behavior. The original +`sem-233/rev1`, `sem-235/rev1` and their published artifacts retain their meaning. + +## IFC-01 — Intent, meaning and realization + +| Boundary | Required information and authority | +| --- | --- | +| Authored requirement | Independent confidentiality owners/clauses, allowed audiences and destinations, possible writers and integrity obligations, required release distinctions, sources/flows/sinks, memory scope, minimum guarantees and admissible limitations. An exact governed profile/policy reference may supply these; an author assertion grants no release authority. | +| Published semantic profile | Exact carrier and encoding, token meaning, order, conservative join, source/default and sink relations, release and non-influence relations, memory scope, unknown behavior, finite bounds and claim limits. | +| Backend/operator configuration | Installed implementation and configuration identity, admitted principal/source/sink bindings, instrumentation, effective coverage, resources, willingness and independently resolved realization evidence. These instantiate published relations; they cannot redefine them. | + +Keep semantic identity, profile ID/revision/digest, policy, schema content, +provider protocol, implementation and configuration pins distinct. A role, +display name, credential, token prefix or participant identity alone does not +identify an obligation owner or prove its release authority. Resolve that +relation through admitted principal and policy context. + +The chosen variability is governed publication of closed finite profiles. +It is sufficient for a fixed finite set of owner-qualified obligations without +a new policy language. Backend bindings may vary concrete principals and sinks +only where the published relation already permits those bindings. They may not +silently turn a generic token into a new owner algebra. + +This amendment introduces no parameterized owner syntax. Repeated deployment +needs may justify bounded typed owner parameters in a later publication, but +that decision must specify admitted identity scope, canonical binding identity, +finite bounds, authority, validation and every consumer. Arbitrary/unbounded +runtime owners, scenario-selected code, plugin discovery and executable profile +content are unsupported. A new owner outside a published universe requires a +new governed publication or a separately justified parameter contract. + +## IFC-02 — Distinctions that an encoding must preserve + +For security, retain `P(C) × P(I)` and componentwise union. An obligation names +a revisioned clause, including its owner and independently scoped release +relation where applicable. Owner A's confidentiality clause permits Alice and +Bob; B's permits Bob and Carol. A combination retains `{C_A, C_B}`: only Bob +satisfies both clauses. Joining obligations intersects acceptable audiences; +it never unions them. Equal current reader sets do not make independently +releasable owners equivalent. + +Likewise, `{I_A, I_B}` records independent unresolved integrity obligations +from two possible influences. Endorsing A's contribution leaves `I_B` and +both influence histories. A permissive observation sink may accept known +untrusted B influence without endorsement; a later action sink still evaluates +that influence against its own requirements. Unknown source resolution is +never known untrusted input or a public/trusted bottom label. + +An encoding is adequate for an authored requirement only if it preserves the +required distinctions through source resolution, derivation, independent +release, memory and every required sink. All encoded permits must respect the +authored prohibitions, and all required functional distinctions must remain +realizable. A conservative refusal of every flow does not satisfy a requirement +that also requires selective authorized sharing. + +Collapsing `C_A` and `C_B` into `restricted` cannot directly represent independent +owner release. Independently trusted contextual policy/provenance can impose +additional restrictions, but an exact support claim must demonstrate the full +encoding and release relation. Owner names in audit text or a backend-private +convention are insufficient. Admitted over-restriction may satisfy a narrower +requirement; it is neither exact expressiveness nor a license to discard a +functional obligation. A token cannot be repurposed against its published meaning. + +SEM-235 domains in general keep MPC-04's partial order and total conservative +join. They need not be powersets or satisfy an additional least-upper-bound +theorem. This security specialization does not narrow those other domains. + +## IFC-03 — Propagation and release + +Every opaque summary, parse, redaction, trusted edit, argument/control choice, +retained memory, shared state, handoff and participant/episode crossing carries +the conservative join of every possible input. Missing coverage is unresolved, +not an empty input set. Exclusion needs the published non-influence relation +and its evidence. All historical labels and source/influence refs are immutable. + +Declassification discharges only named confidentiality obligations; +endorsement discharges only named integrity obligations. Independently trusted +resolution must establish authority over **each** discharged obligation, +including every affected owner's clause. A grant for A does not cover B. +Approval, authentication, admission, trusted editing and monitor advice imply +neither operation. Both operations bind source and fresh result identity, +unchanged coordinate, exact profile/policy revision, sink/destination/audience, +authority, state cut and evidence. Provenance remains after discharge. + +This is the semantic discharge relation. The current wire endorsement carrier +requires nonempty source-to-result token replacements. An owner-aware contract +must publish and verify how its replacements represent discharge while retaining +remaining obligations and writer provenance, or publish a distinct supported +carrier. The existing `integrity:endorsed` token does not mean that all owners +have endorsed every influence. This amendment does not change that carrier. + +## IFC-04 — Admission and negotiation + +Reuse [CA-01–CA-04](control-applicability-and-evaluation.md), API-407 effective +support and API-424 bindings; do not create a competing strength rank. + +At apparatus admission and the relevant exact cut, establish in order: + +1. Resolve the authored requirement and every mandatory obligation independently + of provider responses. Proven inapplicability, absence and unresolved + coverage retain their different meanings. +2. Resolve the exact published profile/encoding and all supported readers. + Establish IFC-02 expressibility, source/default semantics and IFC-03 release + authority. Unknown identities, tokens, revisions, mappings or ambiguous + interpretations are unsupported, regardless of schema validity. +3. Resolve installed and effective realization for the required sources, + explicit data/control paths, memory/crossing scope, sinks, release operations, + finite bounds and evidence. A declaration, configuration digest, method name + or generic modular-control feature is insufficient. +4. Apply CA-04 satisfaction to that coverage, guarantee, admissible loss and + evidence. Record required, declared, installed, effective and admitted + guarantees and limitations separately. Incomparable or unknown evidence + cannot satisfy an obligation. Bounded support is admissible only when the + authored requirement already permits those precise bounds. + +Failure to express a requirement and failure to realize an expressible one are +distinct unsupported reasons. Neither is an ordinary policy denial inside a +supported profile. All prevent the affected mandatory release. A supported +policy may separately deny a particular flow. Optional advice cannot authorize +a mandatory IFC operation or hide missing coverage. + +## IFC-05 — Admitted strength and execution weakening + +An admitted bounded guarantee is the guarantee the run promised, within its +authored constraints. It is not an unexpected downgrade from an implicitly +perfect implementation. Conversely, a later loss of promised coverage, +enforcement, authority, freshness or evidence is weakening/failure even if an +earlier minimum requirement would still have accepted the reduced capability. +It must be recorded; it cannot silently redefine the admitted binding. + +Before each affected external effect or disclosure, revalidate the exact +binding, current cut and effective guarantees with all incumbent gates. Missing +required evidence, unsupported binding, stale cut or unaccepted weakening +prevents release. Evaluate and commit through the existing atomic transition +before dispatch; committed intent is not proof of external application. + +A separately authorized new requirement/profile binding at a new cut may +accept different limits only if every remaining owner and mandatory obligation +is satisfied. Downgrade authorization alone is not satisfaction. Replacing a +provider, configuration or profile does not reinterpret old decisions, erase +memory or authorize replay. Preserve CA-01–CA-09's dependency closure, advice +limits, scoped state, phase-independent parent decisions, independent effect +authority and finite causal budgets. + +## IFC-06 — Governed publication and exact present limits + +A new finite profile publication must include its full IFC-01 contract, +separating cases and bounds, conservative propagation and release evidence, +semantic identity, compatibility/migration rules and claim limits. Portable +adoption additionally needs coherent closed models, schemas, fixtures, +allowlisted loaders, modular fact/selection dispatch, trusted context and +per-obligation authority validation, capability negotiation, runtime/history +readers and conformance. Use ADR-009/061's existing publication ledger, +`schema_bundle()` parity and packaged corpus. A new JSON file or relaxed digest +check alone is insufficient. Stable breaking contracts require a new contract +identity; draft mutability never permits silent semantic reinterpretation. + +| Surface at the #1354 design cut | Exact supported meaning and limit | +| --- | --- | +| General SEM-233 algebra | Finite owner-relative clauses are expressible in principle; synthetic models do not publish portable profiles. | +| `participant-boundary-flow-policy-v1@rev1` | Exactly `confidentiality:restricted`, `confidentiality:unknown`; and `integrity:endorsed`, `integrity:unknown`, `integrity:untrusted`. No independent owner tokens or owner parameters. Unknown is unresolved, never a spare owner slot. | +| Profile loader/model | Exact allowlisted ID/revision/digest and fixed semantic authority; no latest fallback. The schema's maximum 128 entries per coordinate is a shape bound, not extensibility authorization. | +| Modular profile/fact consumers | Closed security and teaching revision-1 cases. `teaching-influence/rev1` has coached-hint/worked-example tokens and no confidentiality, integrity or release claim. A generic reference cannot add a domain. | +| Release contracts | Scoped contextual release validation and token replacement; no published generic owner-token grant carrier. A new owner claim needs explicit per-obligation authority correspondence. | +| Support composition | Current v1 rejects non-exact effective support. CA-04 and IFC-04 define semantic obligations for future adoption; this delivery does not make v1 accept bounded support. | +| Runtime/backend claims | Depend on the exact implemented profile and independently evidenced coverage. No new owner-aware realization, universal noninterference, covert-channel, opaque-internal or backend-equivalence claim is established here. | + +Thus the worked independent-owner cases require a new governed finite profile +and corresponding consumers for direct portable representation; they remain +unsupported by the current security vocabulary. A concrete contextual encoding +may be assessed under IFC-02, but none is certified by this delivery. Arbitrary +cross-profile comparison and automatic conversion remain unsupported. + +## IFC-07 — Migration and evidence + +The [migration contract](../../../docs/migration/ifc-profile-variability.md) +governs source/target pins, mappings, authority, loss, retained memory, pending +work and mixed-revision readers. Unknown old owners cannot be reconstructed +from coarse labels. New-cut evaluation never rewrites a historical release. + +[Worked cases and verification](../../../docs/research/ifc-profile-variability/cases.md) +separate a finite design projection, real incumbent parser/governance checks +and required future consumer evidence. No finite model or ACTIVE semantic +requirement status certifies an installed provider, end-to-end mediation, +durable recovery, adversarial robustness or general formal proof. diff --git a/specs/formal/participant-semantics/modular-participant-control.md b/specs/formal/participant-semantics/modular-participant-control.md index 420fe1514..fd57299a7 100644 --- a/specs/formal/participant-semantics/modular-participant-control.md +++ b/specs/formal/participant-semantics/modular-participant-control.md @@ -1,5 +1,11 @@ # Modular Participant Control and Extensible Dynamic IFC +Issue #1354 and ADR-113 publish [IFC profile variability and publication](ifc-profile-variability.md). +The amendment separates authored requirements, exact profile expressibility +and evidenced realization, preserving this document's original revision and +implementation boundary. It adds no registered owner-aware profile or runtime +support; its migration contract governs future adoption. + Authority revision: `sem-235/rev1`. Publication owner: SEM-235, issue #1070. Incumbent authorities: SEM-230 and SEM-233. Classification: FM3. diff --git a/tools/policy/historical_identity_records.json b/tools/policy/historical_identity_records.json index cf93c235b..58dfe7cc6 100644 --- a/tools/policy/historical_identity_records.json +++ b/tools/policy/historical_identity_records.json @@ -47,7 +47,7 @@ "record_class": "historical-index", "rationale": "Indexes immutable pre-cutover ADR titles, paths, pins, and amendment summaries without making them current identity surfaces.", "occurrences": 4, - "content_sha256": "5dd455dc3052c4223162f505f25beb53d4c0f24d704b05dfeed08662c8091add" + "content_sha256": "dcc7292315a539cbd58123111483e8949b7409029806b706736749167515fedc" }, { "path": "docs/decisions/adrs/adr-000-use-adrs.md", @@ -495,7 +495,7 @@ "record_class": "historical-index", "rationale": "Indexes immutable pre-cutover ADR titles, paths, pins, and amendment summaries without making them current identity surfaces.", "occurrences": 4, - "content_sha256": "095069130a2b2c48ce336abb4729a3357b586bce4c4abaccf74e2ddb307d9c69" + "content_sha256": "5e41a7f227a942b761dd65fcebeada59d46d1c87a44b2fb38132d3322e0e9ef5" }, { "path": "docs/decisions/cage-2-replication-design.md", diff --git a/tools/policy/requirement_order.yaml b/tools/policy/requirement_order.yaml index 707cbd0b9..d696efd9f 100644 --- a/tools/policy/requirement_order.yaml +++ b/tools/policy/requirement_order.yaml @@ -614,6 +614,19 @@ ownership: - specs/sdl/materialization-attestation.md - specs/sdl/observability-and-evidence.md modular-control-semantics: + # Issue #1354 semantic publication and bounded evidence. + - docs/decisions/adrs/adr-113-ifc-profile-variability-and-publication.md + - docs/decisions/issue-1354-ifc-profile-variability-preflight.md + - docs/explain/reference/modular-participant-control-contracts.md + - docs/governance/requirement-scopes/1354.json + - docs/migration/ifc-profile-variability.md + - docs/research/ifc-profile-variability/cases.md + - implementations/python/tests/ifc_profile_variability_model.py + - implementations/python/tests/test_issue_1354_governance.py + - implementations/python/tests/test_issue_1354_ifc_profile_variability.py + - specs/formal/participant-semantics/ifc-profile-variability.md + - tools/policy/historical_identity_records.json + - tools/policy/requirement_order.yaml # Issue #1352 semantic-design publication; no expanded runtime ownership. - docs/decisions/adrs/README.md - docs/decisions/adrs/adr-108-modular-participant-control-and-governed-effects.md @@ -963,6 +976,9 @@ ownership: - implementations/python/packages/raes_runtime/participant_submission_options.py - implementations/python/tests/test_issue_1016_mixed_runtime_coordination.py semantics-expansion: + # Issue #1354 semantic publication; formal specs/tests already belong here. + - docs/decisions/adrs/adr-101-adversarial-participant-flow-control.md + - docs/requirements/SEM-233/requirement.md - contracts/schemas/sdl # Shared description semantics and existing evidence lifecycle owners (SEM-218). - contracts/schemas/experiment-core/experiment-evidence-record-v1.json From 95d2dabbefbe5988dfaaf185b33c3c1ddba95486 Mon Sep 17 00:00:00 2001 From: Brad Edwards Date: Wed, 23 Sep 2026 08:01:49 +0200 Subject: [PATCH 2/2] test: isolate IFC exception assertions --- ...test_issue_1354_ifc_profile_variability.py | 35 ++++++++++++------- 1 file changed, 23 insertions(+), 12 deletions(-) diff --git a/implementations/python/tests/test_issue_1354_ifc_profile_variability.py b/implementations/python/tests/test_issue_1354_ifc_profile_variability.py index e413d94e5..13fcc0b24 100644 --- a/implementations/python/tests/test_issue_1354_ifc_profile_variability.py +++ b/implementations/python/tests/test_issue_1354_ifc_profile_variability.py @@ -97,12 +97,15 @@ def sink(confidentiality, integrity): def test_finite_owner_encoding_admits_only_evidenced_coverage(): assert admit(REQUIREMENT, ENCODING, SUPPORT) == SUPPORT for missing in REQUIREMENT.coverage: + incomplete = replace(SUPPORT, coverage=SUPPORT.coverage - {missing}) with pytest.raises(UnsupportedFlow, match="realization"): - admit(REQUIREMENT, ENCODING, replace(SUPPORT, coverage=SUPPORT.coverage - {missing})) + admit(REQUIREMENT, ENCODING, incomplete) + unresolved = replace(SUPPORT, resolved=False) with pytest.raises(UnsupportedFlow, match="realization"): - admit(REQUIREMENT, ENCODING, replace(SUPPORT, resolved=False)) + admit(REQUIREMENT, ENCODING, unresolved) + no_guarantees = replace(SUPPORT, guarantees=frozenset()) with pytest.raises(UnsupportedFlow, match="realization"): - admit(REQUIREMENT, ENCODING, replace(SUPPORT, guarantees=frozenset())) + admit(REQUIREMENT, ENCODING, no_guarantees) @pytest.mark.parametrize("coordinate,prefix", [("confidentiality", "conf"), ("integrity", "int")]) @@ -115,8 +118,9 @@ def test_independent_obligations_cannot_be_collapsed_or_invented(coordinate, pre "unresolved": (("A", f"{prefix}:A"), ("B", f"{prefix}:deny-unresolved")), "duplicate": (("A", f"{prefix}:A"), ("A", f"{prefix}:B"), ("B", f"{prefix}:B")), } + invalid_encoding = replace(ENCODING, **{coordinate: maps[bad_mapping]}) with pytest.raises(UnsupportedFlow, match="expression"): - admit(REQUIREMENT, replace(ENCODING, **{coordinate: maps[bad_mapping]}), SUPPORT) + admit(REQUIREMENT, invalid_encoding, SUPPORT) def test_admitted_bounded_guarantee_is_distinct_from_unexpected_weakening(): @@ -141,10 +145,11 @@ def test_admitted_bounded_guarantee_is_distinct_from_unexpected_weakening(): ], ) def test_changed_or_unresolved_binding_requires_new_admission(change): - assert check_execution(SUPPORT, replace(SUPPORT, **change)) == "unsupported" + changed_support = replace(SUPPORT, **change) + assert check_execution(SUPPORT, changed_support) == "unsupported" if "profile_pin" in change: with pytest.raises(UnsupportedFlow, match="realization"): - admit(REQUIREMENT, ENCODING, replace(SUPPORT, **change)) + admit(REQUIREMENT, ENCODING, changed_support) @pytest.mark.parametrize( @@ -176,6 +181,7 @@ def test_selective_release_preserves_other_owner_coordinate_and_history(): assert source.provenance_refs <= result.provenance_refs assert source.label.confidentiality == frozenset({"conf:A", "conf:B"}) assert may_flow_at_sink(PROFILE, result, sink({"conf:B"}, {"int:A", "int:B"}), FlowGateState.allowing()) + other_owner = frozenset({"conf:B"}) with pytest.raises(UnsupportedFlow, match="authority"): release( PROFILE, @@ -183,7 +189,7 @@ def test_selective_release_preserves_other_owner_coordinate_and_history(): GRANT_A, result_ref="release:B", operation=FlowOperation.DECLASSIFICATION, - confidentiality=frozenset({"conf:B"}), + confidentiality=other_owner, ) @@ -203,6 +209,7 @@ def test_endorsement_is_owner_scoped_and_observation_does_not_clear_influence(): assert not may_flow_at_sink(PROFILE, result, sink({"conf:A", "conf:B"}, set()), FlowGateState.allowing()) assert may_flow_at_sink(PROFILE, result, sink({"conf:A", "conf:B"}, {"int:B"}), FlowGateState.allowing()) assert result.label.integrity == frozenset({"int:B"}) + other_influence = frozenset({"int:B"}) with pytest.raises(UnsupportedFlow, match="authority"): release( PROFILE, @@ -210,20 +217,23 @@ def test_endorsement_is_owner_scoped_and_observation_does_not_clear_influence(): GRANT_A, result_ref="endorse:B", operation=FlowOperation.ENDORSEMENT, - integrity=frozenset({"int:B"}), + integrity=other_influence, ) @pytest.mark.parametrize("changes", [{"cut": "cut:2"}, {"sink": "sink:other"}]) def test_release_authority_is_bound_to_exact_sink_and_cut(changes): + source = combined() + changed_grant = replace(GRANT_A, **changes) + discharged = frozenset({"conf:A"}) with pytest.raises(UnsupportedFlow, match="authority"): release( PROFILE, - combined(), - replace(GRANT_A, **changes), + source, + changed_grant, result_ref="release:new", operation=FlowOperation.DECLASSIFICATION, - confidentiality=frozenset({"conf:A"}), + confidentiality=discharged, ) @@ -235,6 +245,7 @@ def test_release_grant_cannot_be_reused_for_another_source_or_profile(changed): else: profile = replace(PROFILE, profile_id="different-profile") source = replace(source, label=replace(source.label, profile_id=profile.profile_id)) + discharged = frozenset({"conf:A"}) with pytest.raises(UnsupportedFlow, match="authority"): release( profile, @@ -242,7 +253,7 @@ def test_release_grant_cannot_be_reused_for_another_source_or_profile(changed): GRANT_A, result_ref="release:new", operation=FlowOperation.DECLASSIFICATION, - confidentiality=frozenset({"conf:A"}), + confidentiality=discharged, )