Proposal: Formal MAC/MIC Model and Proof Track

How capOS could move from pragmatic label checks to a formal mandatory access control and mandatory integrity control story suitable for a GOST-style claim.

Problem

Adding a label field to capabilities is not enough to claim formal mandatory access control. ГОСТ Р 59453.1-2021 frames access control through a formal model of an abstract automaton: the model describes states, subjects, objects, containers, rights, accesses, information flows, safety conditions, and proofs that unsafe accesses or flows cannot arise.

capOS should therefore separate two levels:

• Pragmatic label policy. Userspace brokers and wrapper capabilities enforce labels at trusted grant paths and selected method calls. The user/session side of this level is tracked in User Identity and Policy; this proposal does not redefine the broker, session, or local-account surface, only the formal model that would sit underneath it.
• Formal MAC/MIC. A documented abstract state machine, safety predicates, transition rules, proof obligations, and an implementation mapping. Only this second level can support a GOST-style claim. The verification tooling budget (TLA+/Alloy/Kani/Loom/Prusti/Creusot tracks) is owned by Security and Verification; this proposal feeds new obligations into that plan, it does not duplicate the tier definitions.

This proposal defines the path to the second level. It is not a claim that capOS currently satisfies it. The Design Risks and Open Questions entry Q13 – Formal properties to prove treats the current bounded-proof set (cap-table non-forgery, frame-bitmap invariants, transfer rollback, ring producer-consumer invariants) as the baseline that this proposal extends toward an abstract automaton – it is not a step toward seL4-style full functional refinement.

Scope

The first formal target should be narrow:

Confidentiality:
  No transition creates an unauthorized information flow from an object at a
  higher or incomparable confidentiality label to an object at a lower label,
  except through an explicit trusted declassifier transition.

Integrity:
  No low-integrity or incomparable subject can control a higher-integrity
  subject, and no low-integrity subject can write or transfer influence into a
  higher-integrity object, except through an explicit trusted upgrader or
  sanitizer transition.

The proof should cover capability authority creation and transfer before it covers every device, filesystem, or POSIX compatibility corner. For capOS, capability transfer is the dangerous boundary.

Terminology

The Russian GOST terms to keep straight:

• мандатное управление доступом: mandatory access control for confidentiality.
• мандатный контроль целостности: mandatory integrity control.
• целостность: integrity.
• уровень целостности: integrity level.
• уровень конфиденциальности: confidentiality level.
• субъект доступа: access subject.
• объект доступа: access object.

The standards separate confidentiality MAC from integrity control. capOS should not merge them into one vague label field.

Abstract State

The formal model should be intentionally smaller than the implementation. It models only the security-relevant state.

Hold is central. In capOS, authority is represented by capability table entries and transfer records, not by global paths. A formal model that does not model capability hold edges will miss the main authority channel.

Suggested hold-edge metadata:

HoldEdge {
  subject
  entity
  interface_id
  badge
  transfer_mode
  origin
  confidentiality_label
  integrity_label
}

Label Lattices

Use deployment-defined partial orders, not hardcoded government categories.

Example confidentiality lattice:

public < internal < confidential < secret
compartments = {project-a, project-b, ops, crypto}

dominates(a, b) means:

level(a) >= level(b)
and compartments(a) includes compartments(b)

Integrity should be separate:

untrusted < user < service < trusted
domains = {boot, storage, network, auth}

The model must specify how labels compose across containers:

• contained entity confidentiality cannot exceed what the container policy permits unless the container explicitly supports mixed labels;
• contained entity integrity cannot exceed the container’s integrity policy;
• a subject-associated object such as a process ring, endpoint queue, or process handle needs labels derived from the subject it controls or exposes.

Capability Method Flow Classes

capOS cannot rely on syscall names such as read and write. Each interface method needs a flow class.

Initial categories:

ReadLike       data flows object -> subject
WriteLike      data flows subject -> object
Bidirectional  data flows both ways
ControlLike    subject controls another subject/object lifecycle
TransferLike   authority or future data path is transferred
ObserveLike    metadata/log/status observation
Declassify     trusted downgrade of confidentiality
Sanitize       trusted upgrade of integrity after validation
NoFlow         lifecycle release or local bookkeeping only

Examples:

File.read                 ReadLike
File.write                WriteLike
Namespace.bind            WriteLike + ControlLike
LogReader.read            ReadLike
ManifestUpdater.apply     WriteLike + ControlLike
ProcessSpawner.spawn      ControlLike + TransferLike
ProcessHandle.wait        ObserveLike
ServiceSupervisor.restart ControlLike
Endpoint.call             depends on endpoint declaration
Endpoint.return           depends on endpoint declaration
CAP_OP_RELEASE            NoFlow
CAP_OP_CALL transfers     TransferLike
CAP_OP_RETURN transfers   TransferLike

The flow table is part of the trusted model. Adding a new capability method without classifying its flow should fail review.

Transitions

The abstract automaton should include at least these transitions:

create_session(principal, profile)
spawn(parent, child, grants)
copy_cap(sender, receiver, cap)
move_cap(sender, receiver, cap)
insert_result_cap(sender, receiver, cap)
call(subject, endpoint, payload)
return(server, client, result, result_caps)
read(subject, object)
write(subject, object)
bind(subject, namespace, name, object)
supervise(controller, target, operation)
release(subject, cap)
revoke(authority, object)
declassify(trusted_subject, source, target)
sanitize(trusted_subject, source, target)
relabel(trusted_subject, object, new_label)

Each transition needs preconditions and effects. Example:

copy_cap(sender, receiver, cap):
  pre:
    Hold(sender, cap.entity)
    cap.transfer_mode allows copy
    confidentiality_flow_allowed(cap.entity, receiver)
    integrity_flow_allowed(sender, cap.entity, receiver)
    receiver quota has free cap slot
  effect:
    Hold(receiver, cap.entity) is added
    Flow(cap.entity, receiver, transfer) is recorded when relevant

Move is not a shortcut. It has different authority effects but can still create an information/control flow into the receiver.

Safety Predicates

Confidentiality:

read_allowed(s, e):
  clearance(s) dominates classification(e)

write_allowed(s, e):
  classification(e) dominates current_confidentiality(s)

flow_allowed(src, dst):
  classification(dst) dominates classification(src)

No write down follows from classification(dst) dominates classification(src).

Integrity:

integrity_write_allowed(s, e):
  integrity(s) >= integrity(e)

control_allowed(controller, target):
  integrity(controller) >= integrity(target)

integrity_flow_allowed(src, dst):
  integrity(src) >= integrity(dst)

The exact inequality direction must be validated against the chosen integrity semantics. The intent is that low-integrity subjects cannot modify or control high-integrity subjects or objects.

Subject control:

supervise_allowed(controller, target):
  confidentiality/control labels are compatible
  and integrity(controller) >= integrity(target)
  and Hold(controller, ServiceSupervisor(target)) exists

Authority graph:

all live authority is represented by Hold
every Hold edge has a live cap table slot or trusted kernel root
no transition creates Hold without passing transfer/spawn/broker preconditions

Proof Shape

The proof is an invariant proof over the abstract automaton:

Base:
  initial_state satisfies Safety

Step:
  for every transition T:
    if Safety(state) and Precondition(T, state),
    then Safety(apply(T, state))

The transition proof must explicitly cover:

• spawn grants,
• copy transfer,
• move transfer,
• result-cap insertion,
• endpoint call and return,
• namespace bind,
• supervisor operations,
• declassification,
• sanitization,
• relabel,
• revocation and release preserving consistency.

The proof must also state what it does not cover:

• physical side channels,
• timing channels not modeled by Flow,
• bugs below the abstraction boundary,
• device DMA until DMAPool/IOMMU boundaries are modeled,
• persistence/replay until persistent object identity is modeled.

Tooling Plan

Start with lightweight formal tools, then deepen only if the model stabilizes.

TLA+

Best first tool for capOS because capability transfer, spawn, endpoint delivery, and revocation are state transitions. Use TLA+ to model:

• sets of subjects, objects, labels, and hold edges,
• bounded transfer/spawn/call transitions,
• invariants for confidentiality, integrity, and hold-edge consistency.

TLC can find counterexamples early. Apalache is worth evaluating later for symbolic checking if TLC state explosion becomes painful.

Alloy

Useful for relational counterexample search:

• label lattice dominance,
• container hierarchy invariants,
• hold-edge graph consistency,
• “can a path of transfers create forbidden flow?” queries.

Alloy complements TLA+; it does not replace transition modeling.

Coq, Isabelle, or Lean

Only after the model stops moving. These tools are appropriate for a durable machine-checked proof artifact. They are expensive if the policy surface is still changing.

Kani / Prusti / Creusot

Use these for implementation-level Rust obligations after the abstract model exists:

• cap table generation/index invariants,
• transfer transaction rollback,
• label dominance helper correctness,
• quota reservation/release balance,
• wrapper cap narrowing properties.

They do not replace the abstract automaton proof.

ITU-T Z-series specification languages

ITU-T publishes a family of formal specification languages for protocols and behavioural systems. They are complements to TLA+/Alloy, not replacements; each targets a different part of the specification-to-code pipeline.

• Z.100 SDL — Specification and Description Language. State machines with structured data, signals, and composition. SDL models communicating extended finite-state machines, which is a natural fit for the capability ring protocol, endpoint call/return, and supervisor quiesce/resume state. SDL-RT (SDL real-time) adds timers explicitly, which matters for cap_enter wait/timeout semantics.
• Z.120 MSC — Message Sequence Charts. A UML-sequence-diagram predecessor with formal semantics (ITU-T Z.120 Annex B). MSC is useful for documenting what a correct capability-transfer sequence looks like — CALL issuing hold edge, server RECV, server RETURN with result caps, caller CQE — in a form that can be model-checked against the SDL state machine. tools/ccs-style session dumps already produce sequence-shaped records; converting a subset to MSC form would let invariants be checked as sequence-diagram properties (e.g. “no RETURN without a matching CALL hold edge”).
• Z.151 URN — User Requirements Notation (Goal-oriented Requirement Language + Use Case Maps). Worth tracking for later capOS security-requirement traceability — linking proof obligations to threat-model goals — but overkill for the first formal artifact.

Relative to the TLA+/Alloy track:

SDL/MSC should be considered for the protocol layer (capability transfer sequences, endpoint handshakes, supervisor lifecycle) where TLA+ specifications tend to become cluttered with message-passing boilerplate. They should not replace the abstract automaton that covers hold-edge safety invariants — that work stays in TLA+/Alloy.

Other ITU-T security frameworks

Relevant security frameworks from the X-series that this proposal cross-references rather than re-derives:

• X.800 / X.805 — Security architecture for Open Systems Interconnection and Security architecture for systems providing end-to-end communications. Taxonomy of security services (authentication, access control, data confidentiality, data integrity, non-repudiation, availability, privacy) × layers. Used in security-and-verification-proposal.md as a completeness checklist.
• X.810 — Overview of security frameworks.
• X.811 — Authentication framework.
• X.812 — Access control framework. Referenced from user-identity-and-policy-proposal.md for ADF/AEF decomposition.
• X.813 — Non-repudiation framework. Relevant for signed audit records and signed manifest updates.
• X.814 — Confidentiality framework.
• X.815 — Integrity framework. Directly relevant to the MIC half of this proposal; X.815 terminology on integrity “verification”, “recovery”, and “protection” clarifies which obligations apply at which boundary.
• X.816 — Security audit and alarms framework. The monitoring proposal adopts its audit taxonomy.

Implementation Mapping

The proof track must produce implementation obligations that code review and tests can check.

Required implementation hooks:

• every kernel object that participates in policy has stable ObjectId;
• every labeled object has MandatoryLabel;
• every hold edge or capability entry records enough label metadata for transfer checks;
• every capability method has a flow class;
• every transfer path calls one shared label/flow checker;
• every spawn grant uses the same checker as transfer;
• every endpoint has declared flow policy;
• every declassifier/sanitizer is an explicit capability and audited;
• every relabel operation is explicit and audited;
• every wrapper cap preserves or narrows authority and labels;
• process exit and release remove hold edges without leaving ghost authority.

The current pragmatic userspace broker model is allowed as an earlier stage, but the implementation mapping must identify where it is bypassable. Any path that lets untrusted code transfer labeled authority without the broker must move into the kernel-visible checked path before a formal MAC/MIC claim.

Testing and Review Gates

Before implementing kernel-visible labels:

• write the TLA+ or Alloy model;
• include at least one counterexample-driven test showing a rejected unsafe transfer in the model;
• document every transition that is intentionally out of scope.

Before claiming pragmatic MAC/MIC:

• broker and wrapper caps enforce labels at grant paths;
• audit records every grant, denial, and relabel/declassify operation;
• QEMU demo shows a denied high-to-low transfer and a permitted trusted declassification.

Before claiming GOST-style MAC/MIC:

• abstract automaton is written;
• safety predicates are explicit;
• all modeled transitions preserve safety;
• implementation obligations are mapped to code paths;
• transfer/spawn/result-cap insertion cannot bypass label checks;
• limitations and non-modeled channels are documented.

Integration With Existing Plans

This proposal depends on:

• authority graph and resource accounting (Authority Accounting);
• user/session policy services (User Identity and Policy); the pragmatic broker, session metadata, local-account, and stale-cap enforcement work lives there. The formal model in this file treats the pragmatic level as the implementation surface that any abstract subject / hold-edge transition must be mapped back onto;
• capability transfer and result-cap insertion (Capability Model);
• DMA isolation before user drivers become part of the labeled model (DMA Isolation);
• security verification tooling (Security and Verification); the TLA+/Alloy/Kani/Loom/Prusti/Creusot tier descriptions and obligation budget belong there. New obligations introduced here (label dominance helpers, transfer-time flow checks, declassifier/sanitizer audit) feed into that proposal’s tier tables rather than redefining them in this file;
• the consolidated design-risks-register entry Q13 – Formal properties to prove (Design Risks and Open Questions) tracks this proposal as the route from the current bounded-proof baseline to a documented abstract automaton; R14 – User identity / policy is proposal-shaped records why the pragmatic level still cannot make a GOST-style claim today.

Consumers that carry additional proof obligations onto this track:

• OIDC/OAuth2 federated authentication and token-typed capabilities (OIDC and OAuth2). That proposal enumerates a 10-item proof-obligation checklist and a tool-assignment table (TLA+/Alloy/SDL/MSC/Kani/Prusti) for OIDC-specific transitions. The obligations are additive to the ones here: they extend flow classes onto token caps, add session- creation and broker-outbound MAC/MIC predicates, and model verify_id_token as a trusted total function.

Non-Goals

• No certification claim.
• No claim that current capOS implements GOST-style MAC/MIC.
• No attempt to model all side channels in the first version.
• No kernel policy language interpreter.
• No POSIX uid/gid authorization.
• No label field without transition rules and proof obligations.

Open Questions

• What is the smallest useful label lattice for the first demo?
• Should labels live on objects, hold edges, or both?
• Should endpoint flow policy be static per endpoint, per method, or per transferred cap?
• How should declassifier and sanitizer capabilities be scoped and audited?
• Which channels must be modeled as memory flows versus time flows?
• Is TLA+ sufficient for the first formal artifact, or should the relational parts start in Alloy?
• Which parts of ГОСТ Р 59453.1-2021 should be treated as direct goals versus inspiration for a capOS-native formal model?
• How should OIDC/OAuth2 federation fit the first formal artifact? The proof-obligation checklist in OIDC and OAuth2 is already sized for the same TLA+/Alloy/SDL/MSC/Kani tool assignment used here, but the first MAC/MIC model may be cleaner if it lands before federated subjects are added. Decide whether OIDC joins the initial TLA+ module or follows as a second artifact that extends the subject-creation transition.

References

• ГОСТ Р 59383-2021, access-control foundations: https://lepton.ru/GOST/Data/752/75200.pdf
• ГОСТ Р 59453.1-2021, formal access-control model: https://meganorm.ru/Data/750/75046.pdf
• ITU-T Rec. X.800 (03/91) — Security architecture for OSI.
• ITU-T Rec. X.805 (10/03) — Security architecture for systems providing end-to-end communications.
• ITU-T Rec. X.810 (11/95) — Security frameworks: Overview.
• ITU-T Rec. X.811 (04/95) — Authentication framework.
• ITU-T Rec. X.812 (11/95) — Access control framework.
• ITU-T Rec. X.813 (10/96) — Non-repudiation framework.
• ITU-T Rec. X.815 (11/95) — Integrity framework.
• ITU-T Rec. X.816 (11/95) — Security audit and alarms framework.
• ITU-T Rec. Z.100 (04/21) — Specification and Description Language overview.
• ITU-T Rec. Z.120 (02/11) — Message Sequence Charts.
• ITU-T Rec. Z.151 (10/18) — User Requirements Notation.