# ARM-B CARD LAYER — S1: Black Basta ransomware intrusion
> Doctrine reference. Maneuver space + control inventory + coverage relations for this environment. No incident content. Everything below is standing library knowledge: the maneuver family a mature MC shop keeps on hand, the deployed controls, and the coverage relations expressed as a function of control state — never as a record of what happened.

**How to read these cards (term key).**
- **Maneuver** — an atomic adversary behavior identified by its *observable effect*, written as a Hoare triple: **precondition → mechanism → postcondition**.
- **Invariant core** — the part of the mechanism the adversary cannot change without abandoning the goal (carries the maneuver's identity). Exactly one per maneuver. **Implementation variants** realize it different ways.
- **Primitive** — a purpose-neutral micro-behavior (MBC tier); the invariant is the primitive *intersection* across all variants.
- **Robustness (L1–L5, Summiting the Pyramid)** — how hard the *observable* is to evade: L1 ephemeral < L2 configurable < L3 tool-artifact < L4 core-behavior < L5 invariant/chokepoint. It is a **ceiling** on the analytic, and it is a property of the observable, **not** of whether a detection is currently firing.
- **Defensive control** — a sensor whose own state (`enforcing > impaired > killed`) flows through the graph; `impaired`/`killed` sever the telemetry a detection reads.
- **Detect-face** — the face a detection acts on. Four-valued health: **live** (trigger+enrichment intact) / **degraded** (enrichment severed, trigger still fires) / **blind** (trigger severed, no longer fires) / **uncertain**. A face **trigger-depends** on a source (lose it → *blind*) or **enrichment-depends** (lose it → *degraded*).
- **Coverage (covered / notCovered)** — *derived*, never asserted. A maneuver whose only detect-face is blind and that no prevent/react control breaks = **notCovered**. Robustness and coverage are orthogonal.

---

## A. Maneuver cards

### A1 — Exploit of a public-facing application `(bb:mExploit, T1190)`
- **Observable effect:** code execution obtained on the target host through a public-facing application (initial foothold).
- **Hoare triple:**
  - *Precondition* — the egress/target channel is reachable `(bb:pReachYes: rChannel.reachability ≥ reachable)`.
  - *Mechanism* — gain code execution on the target `(invariant core bb:coreExploit)`.
  - *Postcondition* — the adversary process holds ≥ user integrity `(bb:pIntegUser: rProc.integrity ≥ user)`.
- **Invariant core / variants:** core `coreExploit` ("gain code execution on target"); one authored variant, `varExploitCVE` ("public-facing app exploit"). No primitive decomposition is authored for this maneuver.
- **Robustness:** **no authored observable-robustness grade** in the library — no `RobustnessLevel` is set on any exploit observable. Evasion-resistance for this step is *not rankable from the cards* (see D-7).
- **Detect-face:** `dfExploit` ("exploit detection"), sourced directly from the EDR `(sourcedFrom bb:edr1, dependencyLogic required)`.
- **Coverage in one line:** covered while the EDR is enforcing; its sole source is the EDR, so an impaired/killed EDR severs its trigger → blind → notCovered. Full derivation in Part C.

### A2 — Credential access by process-memory read `(bb:mCred, T1003.001)` — *richest card*
- **Observable effect:** admin credential material is harvested by **one process reading the memory of another** (the credential-bearing process). The maneuver is named by this effect — *not* by any specific dump API or tool.
- **Hoare triple:**
  - *Precondition* — the adversary process holds ≥ user integrity `(bb:pIntegUserReq: rProc.integrity ≥ user)`.
  - *Mechanism* — harvest admin credential material `(invariant core bb:coreCred)`, realized by reading process memory.
  - *Postcondition* — the account holds the admin credential `(bb:pCredAdmin: rAccount.credentialHeld ⊇ {admin}, opSubsumes)`.
- **Invariant core / variants / primitives:** core `coreCred` ("harvest admin credential material"). **Two** authored variants realize the same core:
  - `varLsass` — LSASS memory dump; composes `pOpenProcess` (OpenProcess + PROCESS_VM_READ) **and** `pReadProcMem`.
  - `varHandleDup` — handle-duplication read; composes `pDupHandle` (DuplicateHandle + PROCESS_DUP_HANDLE, bypasses SeDebug) **and** `pReadProcMem`.
  - **Invariant primitive (derived intersection):** `pReadProcMem` — "read another process's virtual memory" (MBC **C0049**). This is the shared residue no variant can drop; it *is* the maneuver's discriminating content.
- **Robustness:** spanning observable `obsInvariant` ("process writes then executes remote memory") — **robustness L5 (invariant), role spanning.**
  - *Why L5:* the observable is grounded in the invariant core (the credential-bearing memory read), unavoidable without abandoning credential harvest; both variants compose `pReadProcMem`, so a face keyed here fires *regardless of variant*. Ceiling semantics: L5 caps the achievable analytic robustness. A **variant-grounded / discriminating** observable — e.g. a specific LSASS-dump API signature — sits lower (tool-artifact ≈ L3) and is evaded by swapping to handle-duplication. Pinning the alert to the specific API therefore *lowers* robustness.
- **Detect-face:** `dfCred` ("LSASS access detection"), **trigger-depends on** the EDR telemetry face `(triggerDependsOn bb:dfEdrTelemetry, dependencyLogic required)`.
- **Coverage in one line — the headline caveat:** covered at L5 **while the EDR is enforcing**; because `dfCred` *trigger*-depends on EDR telemetry, an impaired/killed EDR severs its trigger → **blind → notCovered**, and **the L5 rating does not save it** (robustness ≠ coverage). Full derivation in Part C.

### A3 — Impair defenses: disable the endpoint sensor `(bb:mEdrKill, T1562.001)`
- **Observable effect:** the endpoint sensor is set to a non-enforcing state (stops enforcing / reporting).
- **Hoare triple:**
  - *Precondition* — the account holds the admin credential `(bb:pCredAdminReq: rAccount.credentialHeld ⊇ {admin}, opSubsumes)`.
  - *Mechanism* — disable the endpoint sensor `(invariant core bb:coreImpair)`.
  - *Postcondition* — the control's status = **killed** `(bb:pEdrKilled: rEdr.controlStatus = killed)`, which carries `degradesTelemetry = true`.
- **Invariant core / variants:** core `coreImpair` ("disable endpoint sensor"); one authored variant, `varBYOVD` ("bring-your-own-vulnerable-driver"). No primitive decomposition is authored.
- **Robustness:** **no authored observable-robustness grade.**
- **Detect-face — structural blind spot:** the maneuver's own face **is the EDR telemetry face itself**, `dfEdrTelemetry` (sourced from `bb:edr1`). The behavior that this maneuver executes destroys the very telemetry its detection reads. Once the postcondition holds (`controlStatus = killed`), `dfEdrTelemetry` is severed → blind → the maneuver becomes **notCovered by its primary face**. The only authored confirmation path is **out-of-band investigation**: `qWasEdrKilled` ("what is the EDR control status?", DFIQ `MC.Q.controlStatus.edr`), answered by checking service-state via secondary telemetry — a single-scalar observation at **confidence 0.9**.
- **Unmodeled sub-path (see A7 / D-3):** the vulnerable-driver *load itself* is **not** a modeled detect-face or prevent target — the maneuver is carried only as `controlStatus = killed` plus the secondary service-state observation.
- **Coverage in one line:** covered while enforcing; self-severing on success → notCovered by primary telemetry; confirmable only via the secondary investigation (not a coverage relation). Full derivation in Part C.

### A4 — Exfiltration over the egress channel `(bb:mExfil, T1041)`
- **Observable effect:** data is moved off the host to an adversary-controlled location over an outbound channel.
- **Hoare triple:**
  - *Precondition (conjunction of two)* — the account holds the admin credential `(bb:pCredAdminReq)` **and** the egress channel is reachable `(bb:pReachReq: rChannel.reachability ≥ reachable)`.
  - *Mechanism* — move data to an adversary-controlled location `(invariant core bb:coreExfil)`.
  - *Postcondition* — the host's exfiltration state = exfiltrated `(bb:pExfilDone: rTarget.exfilState = exfiltrated)`.
- **Invariant core / variants:** core `coreExfil` ("move data to adversary-controlled location"); one authored variant, `varHttps` ("exfil over HTTPS"). No primitive decomposition is authored.
- **Robustness:** **no authored observable-robustness grade.**
- **Detect-face — split sourcing:** `dfExfil` ("exfil detection"). Its **trigger is a *separate* control**, the network egress monitor `(sourcedFrom bb:netmon1)`; it **enrichment-depends on** the EDR telemetry face `(enrichmentDependsOn bb:dfEdrTelemetry)`; combinator `triggerPlusEnrichment`. So: netmon severed → *blind*; EDR severed → *degraded* (trigger still fires).
- **Coverage in one line:** covered-and-live while both controls are up. Because its trigger rides on netmon (independent of the EDR), an impaired/killed EDR **degrades but does not blind** it — the flow still fires, minus EDR-sourced enrichment (process attribution, data classification). Full derivation in Part C.

### A5 — Data encrypted for impact `(bb:mEncrypt, T1486)`
- **Observable effect:** files on the host are bulk-encrypted / rendered inaccessible (extortion impact).
- **Hoare triple:**
  - *Precondition* — the adversary process holds ≥ user integrity `(bb:pIntegUserReq)` **and nothing else** — notably **not** the admin credential.
  - *Mechanism* — encrypt files for extortion `(invariant core bb:coreEncrypt)`.
  - *Postcondition* — the host's data state = encrypted `(bb:pImpact: rTarget.dataState = encrypted)`.
- **Invariant core / variants:** core `coreEncrypt` ("encrypt files for extortion"); one authored variant, `varRansom` ("symmetric bulk file encryption"). No primitive decomposition is authored.
- **Robustness:** **no authored observable-robustness grade.**
- **Detect-face:** `dfEncrypt` ("mass-encryption detection"), **trigger-depends on** the EDR telemetry face `(triggerDependsOn bb:dfEdrTelemetry, dependencyLogic required)`.
- **Coverage in one line:** covered while the EDR is enforcing; because `dfEncrypt` *trigger*-depends on EDR telemetry, an impaired/killed EDR severs its trigger → **blind → notCovered**; impact then surfaces only out-of-band. **Chokepoint note:** its only precondition is local process integrity, so neither credential-invalidation nor egress-block nor network isolation removes its precondition (see Part C precondition-structure). Full derivation in Part C.

### A6 — Unmodeled credential-access siblings (stubs — no authored coverage record)
A mature endpoint-credential-theft library would carry these neighbors of A2. **mc-core/0.2.1 does not model them at all** — no maneuver, no invariant core, no detect-face, no coverage verdict. They are listed so the responder does not mistake their absence for coverage; **do not infer any coverage for them.** Cross-reference D-8.

- **SAM / registry-hive dump (T1003.002)** — *unmodeled path. No authored coverage record.*
- **DCSync / directory-replication credential theft (T1003.006)** — *unmodeled path* (no domain controller, no replication modeling). *No authored coverage record.*
- **NTDS.dit extraction (T1003.003)** — *unmodeled path. No authored coverage record.*
- **Remote / network LSASS access** — only the **local** process-memory read (A2) is modeled; the network/remote path is *unmodeled*. *No authored coverage record for the remote path.*
- **Offline credential crack (off-environment)** — *unmodeled path* (no off-host computation in the model). *No authored coverage record.*
- **LSA secrets / cached-domain-credential harvest** — *unmodeled path. No authored coverage record.*

> Faithful verdict: of the credential-access family a real tool (e.g. an Impacket-style suite) exercises, this model can speak to roughly the **local process-memory read only**. Everything else in A6 is SILENT.

### A7 — Other unmodeled family members (stubs — no authored coverage record)
- **Vulnerable-driver *load* as a detect/prevent target (BYOVD itself)** — the impair maneuver (A3) is carried only as `controlStatus = killed`; the driver load has **no** modeled detect-face and **no** modeled prevent target. *No authored coverage record for the driver load itself.* Cross-reference D-3.
- **Inhibit-recovery / shadow-copy deletion (T1490)** — a standard ransomware precursor to A5; *unmodeled path. No authored coverage record.*

---

## B. Defensive control cards

### B1 — EDR `(bb:edr1)` — endpoint sensor on the target host
- **What it is:** the primary endpoint sensor; state variable `controlStatus ∈ {enforcing, impaired, killed}`; `impaired`/`killed` carry `degradesTelemetry = true`.
- **What it observes:** process creation, process-memory access (the credential read), driver loads, exploit behavior.
- **Detect-faces it sources:**
  - **As trigger (direct source):** `dfEdrTelemetry` (the raw endpoint-telemetry face) and `dfExploit`. `dfEdrTelemetry` is also the **root** face that `dfCred` and `dfEncrypt` *trigger*-depend on, and that the impair maneuver's own face *is*.
  - **As trigger (transitive, via `dfEdrTelemetry`):** `dfCred` (A2), `dfEncrypt` (A5).
  - **As enrichment only:** `dfExfil` (A4) *enrichment*-depends on it (process attribution / data classification for the network flow).
- **Failure mode (impaired/killed → `degradesTelemetry true`):** the blinding rule fires on the flag, not on a specific value.
  - Trigger-loss → **blind → notCovered:** `dfExploit`, `dfCred`, `dfEncrypt`, and `dfEdrTelemetry` itself.
  - Enrichment-loss → **degraded (still fires):** `dfExfil`.
  - The post-failure surviving detection surface is exactly the *degraded* exfil face.

### B2 — netmon `(bb:netmon1)` — perimeter network egress monitor
- **What it is:** a network egress monitor at the perimeter; **independent of EDR agent liveness** (no modeled dependency on `edr1`).
- **What it observes:** outbound connection destination / volume / protocol (flow metadata only).
- **Detect-faces it sources:** the **sole trigger** of `dfExfil` (A4). It supplies the *trigger* only; the *enrichment* for that face comes from the EDR.
- **Failure mode:** no `controlStatus` StateFact is authored for netmon (it is not modeled as degrading). Structurally, were it impaired/killed its `degradesTelemetry` flag would sever the `dfExfil` **trigger** → `dfExfil` **blind**. As standing posture, its trigger is intact and survives an EDR failure — which is precisely what keeps exfil *degraded* rather than *blind*.

### B3 — Service-control log — EDR service-state telemetry *(not a modeled control)*
- **What it is:** the Windows service-state log for the EDR service (running/stopped); host-local but independent of EDR-agent liveness. **It is NOT modeled as an `mc:Control`** — it appears only as the `observationSource` of the out-of-band EDR-status observation (`bb:obEdrKilled`, confidence 0.9) and the telemetry for the investigation `bb:invEdr`.
- **What it observes:** the EDR service's running/stopped state.
- **Detect-faces it sources:** **none.** Because it is not a first-class control, it can source no detect-face and yields no coverage verdict — only an **Investigation/Observation** answering `qWasEdrKilled`. It is the confirmation path for A3, not a coverage relation. Cross-reference D-9.
- **Failure mode:** survives the EDR kill (independent telemetry); its only output is a single-scalar-confidence observation with no decay/corroboration model (D-5).

### B4 — Environment tooling present but *not* modeled as controls
The environment also fields a **SIEM** (retains forwarded EDR alerts after the sensor dies) and **identity/auth logs** for the service account. **Neither is an `mc:Control`**; neither sources a modeled detect-face; neither yields a coverage verdict. In particular the SIEM's alert-retention (a pre-failure alert persisting after the face goes blind) has **no** vocabulary in the model — `faceStatus` is current-state only. Cross-reference D-10.

---

## C. Coverage relations

Coverage is **derived** from detect-face health + control state + any prevent/react control that breaks the maneuver — never asserted. It is stated here as a **function of control state** (the two regimes over the `controlStatus` domain), which is the doctrine form; it is not a claim about any particular control state obtaining.

### C.0 — Precondition-supply structure (standing maneuver graph, type-level)
This is library structure (`requiresPattern` / `yieldsPattern`, the derived `canUnlock`), the basis for chokepoint reasoning. It is **not** an incident chain.
- `mExploit` yields **≥ user integrity** → establishes the precondition of **`mCred`** *and* **`mEncrypt`**.
- `mCred` yields **admin credential** → establishes the precondition of **`mEdrKill`** *and* **`mExfil`** (the admin credential is the **shared** precondition of both).
- `mExfil` additionally requires **reachable egress** (`pReachReq`) — an environmental precondition not supplied by any maneuver's yield.
- `mEncrypt` requires **only** ≥ user integrity — it does **not** require the admin credential.
- **Chokepoint consequences (doctrine):** invalidating the admin-credential precondition removes a precondition of **both** `mEdrKill` and `mExfil`; invalidating reachable egress removes a precondition of `mExfil` only; **nothing about the credential or the network** removes `mEncrypt`'s precondition — only breaking the local process integrity would. No prevent/react DefenderManeuver instance is authored to carry any of these (D-1/D-2), so these are structural facts, not prescribable actions.

### C.1 — Coverage matrix

| Maneuver | Detect-face | Trigger source | Enrichment source | Robustness ceiling | Coverage — EDR **enforcing** | Coverage — EDR **impaired/killed** |
|---|---|---|---|---|---|---|
| A1 Exploit `mExploit` | `dfExploit` | EDR (direct) | — | none authored | **covered** (live) | trigger severed → **blind → notCovered** |
| A2 Credential read `mCred` | `dfCred` | EDR telemetry `dfEdrTelemetry` | — | **L5 (spanning)** | **covered @ L5** (live) | trigger severed → **blind → notCovered** *(L5 does not save it)* |
| A3 Impair EDR `mEdrKill` | `dfEdrTelemetry` (its own) | EDR (direct) | — | none authored | **covered** (live) | self-severing → **blind → notCovered** by primary; secondary service-state investigation only |
| A4 Exfil `mExfil` | `dfExfil` | **netmon** (independent) | EDR telemetry | none authored | **covered** (live, enriched) | trigger survives + enrichment severed → **degraded → covered-but-degraded** |
| A5 Encrypt `mEncrypt` | `dfEncrypt` | EDR telemetry `dfEdrTelemetry` | — | none authored | **covered** (live) | trigger severed → **blind → notCovered** |

### C.2 — Per-maneuver residual-gap notes
- **A1 Exploit:** single-sourced on the EDR; no independent trigger and no authored robustness ceiling. Under EDR loss the face is blind and the maneuver is uncovered.
- **A2 Credential read — the sharpest relation:** the **L5 rating and a `notCovered` verdict co-exist** once the EDR is down. Robustness measures how hard the *observable* is to evade by changing implementation; it says nothing about whether the face is *firing*. `dfCred` trigger-depends on EDR telemetry — a control-plane failure that severs that telemetry blinds even a maximally-robust observable. Residual under EDR loss: **credential access is uncovered**, L5 notwithstanding. Blind to: any credential read once the endpoint telemetry is gone.
- **A3 Impair EDR:** the maneuver's detection face is the telemetry it destroys → not coverable by its primary face on success. The secondary service-state path is an **investigation**, not a coverage relation, so it yields no `covered/notCovered` verdict — only a confidence-0.9 status observation. Blind to: the driver-load mechanism itself (unmodeled; A7/D-3).
- **A4 Exfil — degraded, not blind:** because the trigger is the **separate** netmon control, the flow still fires under EDR loss; only the EDR-sourced enrichment (process attribution, data classification) is severed. Doctrine: treat a triggered-but-unenriched exfil face as **trustworthy but under-enriched**, not as low-confidence noise. Prevent angle: invalidating `pReachReq` (block egress) or `pCredAdminReq` (revoke credential) would each independently remove a precondition — **but no prevent DefenderManeuver instance is authored** (D-2), so the cards flag the lever without prescribing the action.
- **A5 Encrypt:** `dfEncrypt` trigger-depends on the EDR → blind under EDR loss → impact uncovered by detection, surfacing only out-of-band. Its precondition structure (local integrity only) means the containment levers that cut A3/A4 (credential revocation) and the network levers (isolation, egress-block) **do not remove its precondition** — this is a coverage *and* precondition fact, both card-carriable; the response action to break local integrity is **not** authored (D-2).

### C.3 — Robustness-graded admission (policy overlay)
Under the reference policy, an edge counts as robustness-graded-covered only at observable robustness rank **≥ 4** (StP L4+; `pol:coverageAdmissionRank = 4`). **Only A2 carries an authored observable robustness** (L5 ≥ 4) and clears the bar. A1, A3, A4, A5 have **no authored robustness observable**, so the graded overlay is **underivable** for them — their coverage is asserted at face-health level only, with no robustness ceiling to grade against (D-7).

### C.4 — Where coverage is absent or underivable (SILENT / unmodeled)
- All A6 credential-access siblings (SAM-hive, DCSync, NTDS.dit, remote-LSASS, offline crack, LSA secrets) and A7 members (BYOVD driver-load-as-target, inhibit-recovery/shadow-copy deletion): **no maneuver, no face, no verdict — SILENT.** No coverage may be asserted or inferred for them.
- The EDR-kill maneuver's secondary confirmation: **no coverage verdict** derivable (investigation only, not a detect-face).

---

## D. Card-authorability report (framework-gap channel)

Points where the scenario needed something the current TBox cannot hold faithfully, and what a card-reliant responder would consequently get wrong.

**D-1. Prevent side is empty (slots exist, zero instances).** *Needed:* say what hardening would stop the credential read or the driver load (Credential Guard, RunAsPPL/LSA protection, ASR, WDAC, attack-surface reduction). *Why not:* the TBox has the machinery (`prevent` Function, `invalidates`, `hardeningAbsence` clauses) but **no prevent DefenderManeuver is instantiated**. *Consequence:* a responder asking "what deployment would have prevented A2/A3" gets nothing projectable; the cards can speak detection health, not prevention.

**D-2. Respond/react side is empty (slots exist, zero instances).** *Needed:* card-ground the containment choices (isolate host, disable/rotate the service account, block egress, kill the process). *Why not:* the TBox has the `respond` Function + `evicts` but **no respond DefenderManeuver is instantiated**. *Consequence:* the cards can flag the chokepoint (credential precondition shared by A3+A4; local-integrity precondition of A5) and the `notCovered` verdicts, but **cannot prescribe the response**. A responder can derive *which lever matters* from the precondition structure (C.0) yet finds no authored defender maneuver to enact it — the prescription lives outside the model.

**D-3. BYOVD mechanism is not a modeled maneuver-target.** *Needed:* detect or prevent the vulnerable-driver *load* itself. *Why not:* the impair maneuver is carried only as `controlStatus = killed` + a secondary observation; the driver load has no detect-face and no prevent target. *Consequence:* "catch or block the BYOVD" is not projectable beyond the killed-status observation; a responder over-reads the model as covering the *how* of the EDR kill.

**D-4. No wall-clock / latency granularity.** *Needed:* reason about how fast a face blinds, dwell time, MTTR, time-to-contain. *Why not:* state is integer step-indexed only (`stepIndex`, `atStep`); no duration or latency. *Consequence:* any timing/speed-of-response judgment is unsupported — only ordering exists.

**D-5. Single scalar confidence, no decay or corroboration.** *Needed:* reason about how the out-of-band EDR-killed confidence (0.9) ages or fuses with other evidence. *Why not:* one scalar, no aging or evidence-combination calculus. *Consequence:* a responder cannot model confidence decay or corroboration; the 0.9 is a flat, un-fusable number.

**D-6. No asset-criticality / blast-radius vocabulary.** *Needed:* prioritize by crown-jewel value or downstream reachability. *Why not:* single host, one channel; no data-valuation or reachability-beyond-the-channel modeling. *Consequence:* any prioritization-by-asset-value question is unanswerable from the cards.

**D-7. Robustness ceiling authored on only one of five maneuvers.** *Needed:* a robustness rank for exploit, EDR-kill, exfil, and encryption — "how hard to evade" per step. *Why not:* only `obsInvariant` (the credential read) carries a `RobustnessLevel`; the other four maneuvers have **no** observable with a robustness grade. *Consequence:* evasion-resistance is rankable for exactly one step; the robustness-graded coverage overlay (C.3) is underivable for the other four. A responder asking "is our exfil/encryption detection robust to a technique swap?" gets no card-grounded answer.

**D-8. The L5 spanning observable binds to its maneuver only through an occurrence-level evidence claim.** *Needed:* state, as standing library doctrine, that the credential-read invariant *manifests as* the L5 spanning observable. *Why not:* there is **no type-level `manifestsAs` / `groundedIn` / `primitiveManifestsAs` edge** from `coreCred` or `pReadProcMem` to `obsInvariant`; the only link is an occurrence-level evidence claim (`evidenceFor` an occurrence). *Consequence:* the doctrine "this maneuver's invariant shows up as this L5 observable" cannot be read off the standing library without leaning on incident evidence — an altitude mismatch. A responder consulting only the type-level library cannot recover the L5-spanning tie to the maneuver.

**D-9. The secondary confirmation telemetry is not a first-class control.** *Needed:* express coverage of the EDR-kill via the surviving service-state telemetry. *Why not:* the service-control log is only an `observationSource`/investigation input, not an `mc:Control`; it can source no detect-face and yields no coverage verdict. *Consequence:* the EDR-kill maneuver has **no derivable coverage** from the secondary source — only an investigation observation. A responder cannot get a `covered` verdict for A3 even though an independent signal exists.

**D-10. No alert-forwarding / retention vocabulary; `faceStatus` is current-state only.** *Needed:* express that an alert emitted while a face was live persists (e.g. forwarded to a SIEM) even after the face goes blind. *Why not:* the four-valued `faceStatus` describes the face's *current* firing ability; there is no entity or relation for alert forwarding/retention, and the SIEM is not modeled. *Consequence:* a responder reading a `blind → notCovered` verdict for the credential face would wrongly conclude *nothing is recoverable* post-failure, missing that a pre-failure alert may persist downstream. The model conflates "the face no longer fires" with "no evidence survives."

**D-11. Single-trigger dependency; no modeled telemetry redundancy for the endpoint faces.** *Needed:* reason about adding a second, independent telemetry source to keep the credential/encryption faces alive if the EDR dies. *Why not:* `dfCred` and `dfEncrypt` each carry a single `required` trigger dependency on `dfEdrTelemetry`; the `redundant`/`kOfN` combinators exist in the TBox but are unpopulated for these faces. *Consequence:* the cards cannot represent a telemetry-redundancy remediation; the responder cannot ask "what second sensor removes the single point of failure" and get a modeled answer.

---

*Validation self-check:* one invariant core per maneuver (`mc:via`, exactly one) — satisfied in every A-card. Robustness stated as a **ceiling on the observable** (A2 only; C.3), never as a realized analytic score. Coverage presented as **derived** from face-health + control state + prevent/react (C), never asserted; the two-regime rendering derives from the `controlStatus` domain and the `degradesTelemetry` flag, not from any asserted current state. Trigger-vs-enrichment health rollup (blind vs degraded) follows the `triggerDependsOn` / `enrichmentDependsOn` / `triggerPlusEnrichment` semantics. No retired constructs used (no AMC, ORTG, forcedness, chokepointCoupling, `transition`-as-unit, six-fork model, or `covers`-as-relation; `Detectability`/`DependencyLogic`/`respond`/`triggerPlusEnrichment`/`EvidenceClaim` used as the canonical names). No incident timeline, sequencing, or occurrence-level narrative appears in any card.