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.
• 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.

This proposal defines the path to the second level. It is not a claim that capOS currently satisfies it.

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.

U       set of user accounts / principals
S       set of subjects: processes, sessions, services
O       set of objects: files, namespaces, endpoints, process handles, secrets
C       set of containers: namespaces, directories, stores, service subtrees
E       entities = O union C
K       kernel object identities
Cap     capability handles / hold edges
Hold    relation S -> E with metadata
Own     subject-control or ownership relation
Ctrl    subject-control relation
Flow    observed information-flow relation
Rights  abstract rights: read, write, execute, own, control, transfer
Access  realized accesses: read, write, call, return, spawn, supervise

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.

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-transfer-design.md);
• user/session policy services (user-identity-and-policy-proposal.md);
• capability transfer and result-cap insertion (capability-model.md);
• DMA isolation before user drivers become part of the labeled model (dma-isolation-design.md);
• security verification tooling (security-and-verification-proposal.md).

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?

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