# 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-proposal.md](user-identity-and-policy-proposal.md);
  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-proposal.md](security-and-verification-proposal.md);
  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-register.md](../design-risks-register.md) 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:

```text
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.

| Symbol | Meaning |
| --- | --- |
| `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:

```text
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:

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

`dominates(a, b)` means:

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

Integrity should be separate:

```text
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:

```text
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:

```text
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:

```text
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:

```text
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:

```text
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:

```text
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:

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

Authority graph:

```text
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:

```text
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:

| Concern                    | Tool in capOS              |
|----------------------------|----------------------------|
| Global state transitions, invariants | TLA+ (primary) |
| Relational graph queries (hold edges, dominance) | Alloy |
| Per-service protocol state machines | Z.100 SDL (optional) |
| Canonical call/return sequences | Z.120 MSC (optional) |
| Durable machine-checked proof | Coq / Isabelle / Lean (later) |
| Implementation-level Rust obligations | Kani / Prusti / Creusot |

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-transfer-design.md](../authority-accounting-transfer-design.md));
- user/session policy services
  ([user-identity-and-policy-proposal.md](user-identity-and-policy-proposal.md));
  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.md](../capability-model.md));
- DMA isolation before user drivers become part of the labeled model
  ([dma-isolation-design.md](../dma-isolation-design.md));
- security verification tooling
  ([security-and-verification-proposal.md](security-and-verification-proposal.md));
  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-register.md](../design-risks-register.md)) 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-proposal.md](oidc-and-oauth2-proposal.md)). 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-proposal.md](oidc-and-oauth2-proposal.md) 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.