Design participant-relative opacity and supervisor-observation security semantics

[Brad-Edwards]

Objective

Assess and design opacity as an explicit participant information-security relation for ACES, including what a participant or other governed observer can infer from observations, omissions, control decisions, timing/order, policy changes, and the behavior of the supervisor itself.

#794 and ADR-085 define participant-relative projection and policy noninterference, and reserve future epistemic relations. They do not currently define opacity, observer belief, secret predicates, or the information leaked by approval/denial and supervisory behavior. This issue must decide whether opacity becomes a governed ACES relation, how it composes with SEM-230, and what implementation and assurance work it requires.

This is design and program work. It must not report an opacity proof or runtime enforcement that has not been delivered.

Required design questions

Observer and secret model

Define or explicitly reject:

• observer identities, coalitions, audiences, and attacker capabilities;
• secret predicates over world, participant, controller, policy, backend, and evidence state;
• observation maps over visible content, visible event occurrence, absence/withholding, ordering, timing, delivery status, failures, and control decisions;
• initial-state, current-state, K-step, infinite-step, language-based, probabilistic, and epistemic opacity variants;
• passive observation versus active probing through participant inputs;
• knowledge accumulated across episodes, retries, replay, policy revisions, and controller handoffs.

Supervisor-policy visibility

Model the cases where the observer:

• knows the full policy/supervisor;
• knows only the public policy surface;
• learns policy behavior from approvals, denials, edits, deferrals, handoffs, or other online decisions;
• observes a delayed, redacted, or selectively disclosed control decision;
• can distinguish supervisor changes through behavior even when the change event is hidden.

Decide whether the policy revision, supervisor implementation, control authority, and decision rule are low, high, declassified, or observer-relative state.

Relation to existing ACES claims

Precisely relate opacity to:

• policy noninterference;
• participant projected-history equality;
• epistemic indistinguishability;
• trace inclusion/equivalence;
• strong/weak/branching bisimulation;
• disclosure and declassification;
• concealment/revocation and prior knowledge;
• bounded negative-leakage tests.

State implications and non-implications. Do not use opacity as a synonym for redaction, access control, noninterference, or an opaque implementation.

Enforcement and realization

Assess verification, runtime enforcement, information-release scheduling, transformation/edit functions, supervisor synthesis, and deliberately added nondeterminism. Determine:

• what can be authored in SDL versus fixed by semantic authority;
• which contracts and runtime records need observer/secret/relation coordinates;
• whether action admission or egress mediation can enforce the selected opacity property;
• how backend capabilities declare exact, bounded, weakened, or unsupported realization;
• how audit/evidence surfaces avoid becoming an ungoverned leakage channel;
• how counterexamples and belief/information-state witnesses are represented safely.

Deliverables

• Primary-source-grounded current-state and gap assessment.
• Relation-selection decision and ADR amendment/new ADR as required.
• Formal carrier, observation map, secret-predicate, quantifier, and policy-visibility design.
• Worked examples showing:
  • projected histories that pass a bounded equality check but violate a selected opacity property;
  • a supervisor decision that leaks a secret;
  • a case where noninterference and opacity differ;
  • declassification that is authorized but still changes observer knowledge.
• Requirement disposition covering reuse, amendment, or creation.
• An ordered implementation and assurance issue graph.

Acceptance criteria

• The selected opacity relation is mathematically defined and revisioned, or rejection is supported by a rigorous mapping to an existing relation that covers the same claims.
• Supervisor-policy knowledge and decision-channel leakage are explicit.
• Time, nondeterminism, probability, concurrency, and partial-order scope are stated rather than silently inherited.
• Runtime enforcement, bounded checking, model checking, proof, and backend realization are separate assurance states.
• The behavioral-relation catalog and claim bindings can represent the selected relation and evidence level.
• Required DRAFT Ground Control authority exists before requirement-backed implementation children are opened.
• Child issues have bounded outcomes, dependencies, negative cases, evidence requirements, and explicit nonclaims.

Non-goals

• Treating generic implementation opacity as an information-security property.
• Proving every opacity variant.
• Exposing participant internals, prompts, chain-of-thought, credentials, hidden policy bodies, or raw secret payloads.
• Replacing policy noninterference or bisimulation with one catch-all relation.

Dependencies and coordination

• Parent program and adopted boundary: Assess and design formal participant I/O control with information-flow and bisimulation semantics #794.
• SEM-230 semantic authority: SEM-230 — Participant Information-Flow And Control Semantics #796.
• Mixed control: Mixed-Control Participant Operation (ACT-617) #251, Participant External Input And Intervention Contracts (API-409) #252, and Intervention, Handoff, And Supervisory Lifecycle (RUN-310) #255.
• Runtime mediation: RUN-319 — Participant Information-Flow Policy Enforcement #799.
• Assurance: ASR-535 — Participant Information-Flow And Relation Assurance #800.
• Behavioral-relation taxonomy: Define behavioral-relation taxonomy and prevent conformance/equivalence conflation #747.
• The participant-control SOTA/novelty evidence gate should inform source selection and claim positioning.

Primary-source starting set

• Jacob et al., Opacity of Discrete Event Systems and its Applications.
• Yin and Lafortune, A Uniform Approach for Synthesizing Property-Enforcing Supervisors for Partially-Observed Discrete-Event Systems.
• Xie, Yin, and Li, Opacity Enforcing Supervisory Control using Non-deterministic Supervisors.
• Current work on opacity with known, unknown, and partially inferred supervisors.
• Fagin, Halpern, Moses, and Vardi, Reasoning About Knowledge.
• ACES ADR-022, ADR-081, ADR-085, SEM-230, and the behavioral-relation catalog.

Requirements

• SEM-231

[Brad-Edwards]

🛠️ Picked up by /implement - driver codex, branch 810-participant-opacity-semantics, 2026-07-29T04:07:45.327Z.

[Brad-Edwards]

gc workflow phase recorded: preflight (issue #810). Posted by the MCP server to enforce ordering between workflow steps (issue #794 MVP-2). Do not edit or delete — used by downstream tools to gate phase prerequisites.

[Brad-Edwards]

gc workflow phase recorded: plan (issue #810). Posted by the MCP server to enforce ordering between workflow steps (issue #794 MVP-2). Do not edit or delete — used by downstream tools to gate phase prerequisites.

Outcome

Define participant-relative, one-sided possibilistic predicate opacity as a revisioned epistemic relation and publish an executable delivery program without claiming that RAES, RUN-319, or any backend currently enforces or proves it. The external primary/security/adjacent literature review is already recorded in docs/research/participant-opacity/ and preceded architecture preflight as requested.

Implementation

1. Use TDD against the shared relation seam. First add failing tests that require taxonomy rev5, participant-predicate-opacity, its dedicated claim surface and primary-source references; require paired relation-parameter-profile ref/revision fields for opacity while preserving existing consumers; exercise independent assurance axes; reject finite evidence promoted to universal scope; and structurally validate the issue program, worked counterexamples, dependency DAG, evidence boundaries, and nonclaims.
2. Extend BehavioralClaimBindingModel, BehavioralRelationDefinitionModel, RelationAssuranceModel, and validate_behavioral_claim_binding() rather than creating an opacity-local binding or registry. The shared binding will reference one closed revisioned relation-parameter profile; the catalog will declare when it is mandatory. Keep the extension backward-compatible for existing non-opacity bindings while making opacity coordinates structurally unavoidable.
3. Advance contracts/concept-authority/behavioral-relations-v1.json and its canonical fixture to rev5. Add the unary epistemic opacity definition, observer/secret/possible-point/profile obligations, supervisor-visibility and active-strategy treatment, independent assurance/nonclaim states, exact implications and non-implications, and revision-pinned primary sources. Advance every live rev4 producer together.
4. Regenerate affected published schemas (behavioral-relations-v1, experiment-study-v1, and scientific-completeness-taxonomy-v1) from schema_bundle(), update each schema-publication entry with its new content hash/summary, and keep generated/publication parity. No hand-authored schema-only divergence.
5. Add ADR-099 and a focused SEM-231 formal specification. Define the possible-point carrier, information cell, one-sided and symmetric quantifiers, passive/active strategy order, observation alphabet including omissions/decisions/timing/order/policy changes, supervisor-visibility profiles, memory/declassification behavior, concurrency/nondeterminism/probability limits, coalition scope, and the four required worked examples. Update participant and behavioral-relation reader views plus lineage ledger/source audit to map the imported definitions to RAES-native carriers.
6. Publish the current-state assessment, requirement disposition, and machine-readable/human-readable implementation program. Create DRAFT SEM-231 before opening children and relate it to SEM-230. Then open five bounded milestone-67 children for bounded falsification, finite-state model checking, mathematical proof, reference-runtime enforcement, and backend realization/conformance. Give each explicit negative cases, evidence/reproduction requirements, nonclaims, and real GitHub blocked by dependencies; reuse ACTIVE ASR-535, RUN-319, and API-407 where they already own assurance, runtime, and backend concerns.

Acceptance mapping

• Mathematical definition/revision: ADR-099, SEM-231 spec, rev5 catalog, and shared typed profile reference.
• Supervisor knowledge/decision leakage: formal visibility profiles and observation-channel counterexamples include decisions, occurrence, delivery, omission, order, latency, retries, and changed behavior.
• Time/nondeterminism/probability/concurrency/partial order: independently selected dimensions; baseline is untimed, possibilistic support-set semantics and makes no quantitative/timed/partial-order claim.
• Relation boundaries: document the conditional SEM-230 implication, failed reverse implication, information-cell role of epistemic indistinguishability, and non-equivalence to projected histories, trace relations, simulation/refinement, and bisimulation.
• Assurance separation: definition, checker/bounded tests, model check, proof, runtime enforcement, backend declaration/realization, and bounded conformance remain independent catalog/binding/program states.
• Catalog/binding representation: opacity requires a revisioned relation-parameter profile and exact evidence/assurance scope; universal claims still require model-check or proof evidence.
• Governance: SEM-231 remains DRAFT in this design run; it exists before requirement-backed children. The parent design does not transition child authority ACTIVE.

Whole-repository design

• Security: preserve strict participant/audience subject separation; store safe ids/refs/digests rather than secret values, worlds, private memory, policy bodies, prompts, credentials, or raw evidence; model decision/error/timing channels explicitly; add no environment/argv secret path; retain bounded diagnostics and the redacted unexpected-error envelope.
• Maintainability: reuse ADR-081/085/095, SEM-230 state and projection, BehavioralClaimBindingModel, catalog validation, claim-policy tooling, schema generation/publication, Ground Control, and existing conformance/runtime authorities.
• Extensibility: one shared relation-profile reference supports later symmetric, K/infinite-step, coalition, active, timed, partial-order, and quantitative variants without editing every claim consumer; variants that change the property still require a separately governed relation.
• Whole-repo gates: contract fixtures, schemas/publication entries, corpus packaging, experiment/scientific-completeness consumers, behavioral-claim policy, lineage, ADR immutability, requirement governance, and documentation are all in scope. No SDL, API endpoint, policy engine, belief store, runtime monitor, backend capability, or conformance result is added here.

Verification

Run targeted behavioral-relation, claim-policy, SEM-231/program, schema, lineage, and corpus tests during red-green-refactor. Before completion set RAES_REQUIREMENT_UID=SEM-231 because the branch has no UID, then run:

• implementations/python/.venv/bin/python tools/check_repo_policy.py
• implementations/python/.venv/bin/python tools/check_requirement_governance.py
• implementations/python/.venv/bin/python tools/verify_all.py
• the configured full verify, make policy, and later the single required pre-commit gate.

This is not a documentation-only carveout: shared contract models, generated schemas, fixtures, and tests change.