The Security Properties Methodology

Formal Foundations

Mipiti's methodology is grounded in established security science, not a proprietary invention:

These methods have been used for decades in high-assurance environments (defense, critical infrastructure, hardware security) but were impractical for product teams due to the manual effort required. Mipiti automates them with AI while preserving their formal guarantees.

What Mipiti adds

• Usage (U) — a security property for non-extractable assets (see below)
• Extensible property set — C, I, A, U are the defaults; domains can add Safety, Privacy, Authenticity, or others
• LLM-powered discovery — AI identifies assets, attackers, and boundaries from natural language
• Deterministic coverage — the CO matrix is computed, not generated, ensuring mathematical completeness
• Continuous refinement — versioned models that evolve with the product

The Security Property Set

Each asset is tagged with the security properties that matter for it. The default set ships with four properties:

The first three (C, I, A) come from the well-known CIA triad. Usage extends the set to capture a threat that CIA cannot express: when an asset's confidentiality is architecturally assured (non-extractable), an attacker can still use the asset — invoking operations through its interface — without compromising the asset itself. The asset remains perfectly confidential, yet the attacker leverages its functionality for an unauthorized purpose.

This is formally independent from C, I, and A. Confidentiality is intact (the asset was never disclosed). Integrity is intact (the asset was never modified). Availability is intact (the service is running). Yet the security posture is degraded because the asset's functionality was exercised for the wrong purpose.

The property set is not closed — the methodology works with any set of security properties. The completeness guarantee comes from the cross-product math (Asset x Attacker), not from any specific property vocabulary.

When does Usage apply?

Usage applies when two conditions are met simultaneously:

1. The asset's confidentiality is architecturally assured — the asset is non-extractable by design (hardware isolation, secure enclaves, etc.)
2. The asset exposes an operational interface — operations can be invoked on or with the asset without extracting it

If the asset is extractable (e.g., a key stored in a config file, model weights on a regular GPU), then misuse reduces to a Confidentiality failure — someone obtained access to the asset or the credentials that protect it. Usage does not apply.

If the asset is non-extractable but has no operational interface (e.g., encrypted data at rest with no query API), then there is nothing to use. Usage does not apply.

Examples

The pattern: hardware or architectural isolation creates the non-extractability that makes Usage independent from Confidentiality. Without that isolation, every "misuse" scenario traces back to a Confidentiality failure of some credential or access path.

Capability-Defined Attackers

Attackers are defined by position and capability — not by persona labels like "script kiddie" or attack scenarios like "SQL injection."

Each attacker is a concrete, verifiable capability statement:

"Attacker with ability to intercept network traffic between client and server"

This framing is reusable across models and directly maps to control objectives.

The Control Objective Matrix

Control Objectives (COs) are the cross-product of:

Asset x Attacker = Control Objective

Each CO bundles all of an asset's security properties into a single testable "SHALL" statement:

"Confidentiality, Integrity, and Availability of [User Session Tokens] shall be protected from an attacker with [ability to intercept network traffic]."

This condensed format produces one CO per asset-attacker pair. The asset's full set of security properties is included in the statement, ensuring every property is covered without generating separate COs per property.

Because COs are computed deterministically (not generated by the LLM), coverage is mathematically guaranteed — no gaps, no hallucinations.

Implementation Controls

Control objectives define what must be protected. Implementation controls define how. After the CO matrix is computed, Mipiti uses LLM reasoning to generate concrete controls that satisfy each CO:

CO: "Integrity of [User Session Tokens] shall be protected from an attacker with [ability to intercept network traffic]."

Controls: HMAC-sign session tokens (CTRL-01), enforce TLS 1.3 on all endpoints (CTRL-02)

A single control can cover multiple COs, and a single CO can be covered by multiple controls organized into mitigation groups — alternative paths to satisfy the same objective.

Controls are the actionable output of the threat model: they are what your team implements, tracks in Jira, and marks as implemented on the Assurance page. Every control traces back through a CO to a specific asset-attacker pairing, maintaining full traceability from risk to mitigation.

Risk Ratings: Impact, Likelihood, and Risk Tiers

Every control objective carries a risk tier (Critical / High / Medium / Low) that helps prioritize which COs to address first. Risk tiers are derived deterministically — no LLM call — from two composed ratings:

• Asset Impact (H / M / L) — composed from a seven-factor decomposition.
• Attacker Likelihood (H / M / L) — composed from a five-factor decomposition.

Both H/M/L ratings are themselves outputs, not inputs. The platform never asks the user (or the LLM) for an H/M/L directly — they're always composed by a fixed rule from the factors below. Two consequences:

1. The same factor decomposition always composes to the same rating. Two reviewers looking at the factors can disagree about the factors but cannot disagree about the rating — that step is mechanical.
2. A rating without factors is meaningless. Hovering any rating badge shows the factor decomposition the rating came from; the audit trail records the factors, not just the H/M/L.

Asset Impact factors (seven axes)

Impact is an intrinsic property of the asset — what happens if this asset is compromised. The LLM judges the asset along seven axes during generation; you (or a coding agent) can override any factor afterward with a documented reason.

Per declared security property (only the properties the asset declares contribute):

• confidentiality_subscore — None / Low / High. Severity if confidentiality is breached.
• integrity_subscore — None / Low / High. Severity if integrity is broken.
• availability_subscore — None / Low / High. Severity if availability is lost.
• usage_subscore — None / Low / High. Severity if the asset's purpose-binding (Usage property) is violated — applies to non-extractable assets that expose an operational interface.

System-wide modifiers (always contribute):

• blast_radius — Isolated / Multiplicative / Cascading. Whether compromise stays contained, multiplies across peers, or cascades into dependent systems.
• recoverability — Trivial / Manageable / Permanent. How recoverable the harm is — a token rotation is trivial; a leaked private key is permanent.
• regulatory_scope — None / Notification / Legal. Whether breach triggers regulatory notification (GDPR Art. 33 etc.) or hard legal exposure (PCI fines, HIPAA penalties).

Impact composition rule

Let max_subscore be the highest declared per-property subscore. The composed impact is:

• H — if max_subscore == High, OR if max_subscore == Low AND any modifier is amplified (blast non-Isolated, recoverability Permanent, or regulatory Legal).
• L — if max_subscore == None AND blast is Isolated AND recoverability is Trivial AND regulatory_scope is None (the "all dials at zero" case).
• M — otherwise.

The amplifier rule is what catches the often-missed case where individual subscores look modest but the asset participates in a multiplicative blast radius or carries unrecoverable harm — those cases compose to H even without a single High subscore.

Example: An asset with confidentiality_subscore: Low, integrity_subscore: None, blast_radius: Multiplicative, recoverability: Manageable, regulatory_scope: Legal composes to H — a Low subscore plus a Legal regulatory amplifier overrides the otherwise-Medium reading.

Attacker Likelihood factors (five axes)

Likelihood is an intrinsic property of the attacker — how probable it is that this attacker capability will be exercised against the system. Five axes:

• attack_vector — Network / Adjacent / Local / Physical. Where the attacker has to be to exercise the capability.
• privileges_required — None / Low / High. Account / authorization level needed.
• attack_complexity — Low / High. Whether the attack works on first try or needs specific conditions.
• user_interaction — None / Required. Whether a human victim has to do something for the attack to succeed.
• capability_prevalence — Commodity / Targeted / Rare. How widely available this attack capability is in the wild.

Likelihood composition rule

The composition is prevalence-dominant — capability prevalence is the strongest signal of whether an attack will land at all:

• Commodity prevalence (ambient against any reachable surface — credential stuffing, SQL injection scanning, SSL stripping) → H, unless both privileges_required: High AND attack_complexity: High (the friction-overcomes-commodity case → M).
• Rare prevalence (nation-state, novel exploit chain) → L, regardless of other axes.
• Targeted prevalence → friction-cumulative score across the access factors:
  • +2 if attack_vector is Local or Physical, +1 if Adjacent.
  • +2 if privileges_required is High, +1 if Low.
  • +1 if attack_complexity is High.
  • +1 if user_interaction is Required.
  • Friction ≥ 4 → L; otherwise → M.

The rule encodes the empirical observation that prevalence usually wins: a Commodity-class attack with even moderate friction is still High (it'll land somewhere on a fleet); a Rare-class attack with no friction is still Low (the attacker just isn't there). Targeted attackers are where the access factors actually move the rating.

Example: attack_vector: Network, privileges_required: None, attack_complexity: Low, user_interaction: None, capability_prevalence: Commodity composes to H — commodity scanner against a public surface.

Example: attack_vector: Physical, privileges_required: High, attack_complexity: High, user_interaction: Required, capability_prevalence: Targeted composes to L — friction = 2+2+1+1 = 6, well past the 4-threshold.

Risk Tier Matrix

Each CO's risk tier is computed from the composed Asset Impact × composed Attacker Likelihood using a 3×3 matrix:

Risk tiers appear as color-coded badges on each CO throughout the platform. Hovering a CO's risk badge shows the underlying Impact and Likelihood. Hovering an asset or attacker rating shows the full factor decomposition that produced it.

Editing risk ratings

The composed rating is read-only on the wire — the API rejects any attempt to PATCH impact or likelihood directly. To override the LLM's judgment:

1. Open the asset (or attacker) edit modal.
2. Change one or more factor values. The derived rating updates live in the modal as you edit, so you see what your factor change composes to before saving.
3. Provide a change reason (required when factors change). The reason is captured in the rating-revision audit trail alongside who edited and when.

The audit trail records every factor change as an append-only revision keyed by (model_id, asset_id) (or attacker_id). The model's version chain isn't bumped for factor edits — they're a separate audit channel. GET /api/models/{id}/versions/{N} returns factors as recorded at that version's creation; the live read (GET /api/models/{id}) applies the latest revisions as a read-time overlay. Each revision row carries an explicit model_version column so a reader can attribute every factor change to the threat-model version it was applied against — version is tracked, not inferred from timestamps. When a new version is created, the latest revisions for version K are folded forward into K+1's blob so each version's blob captures its own end-of-life state; subsequent overlay reads scoped to K+1 don't double-count K's revisions.

Per-CO factor history is exposed via GET /api/models/{id}/control-objectives/{co_id}/factor-history — a chronological per-version timeline carrying factor snapshots at each version's start and end, derived risk_tier at each boundary, and the per-revision delta sequence with editor / rationale / change_reason. Auditors use it to walk every factor transition and the operator decision behind each one.

When a manual asset/attacker is added through the UI or MCP, you supply only the identity-bearing fields (name, description, security properties for assets; capability, position, archetype for attackers). The platform LLM-reasons the factor decomposition using the same prompt the generation pipeline applies to LLM-introduced entities — so calibration is consistent regardless of who introduced the entity. You can override any factor afterward via the edit flow above.

Two surfaces, two purposes — platform starting point vs. operator override

The platform's LLM-judged factors are a calibrated starting point, not authoritative judgment. The judgment is grounded only in the feature description; many factor values are deployment-specific in ways the platform cannot see — your tenant's regulatory scope, your incident base rate, your actual network segmentation, your operational maturity for recovery. So there are two distinct override surfaces, and they live in the audit trail under different change_reason semantics:

Both surfaces write to the same append-only rating_revisions side-table, and change_reason is how a reviewer later distinguishes "this is what the LLM thought at this moment" from "this is what the operator decided based on context the LLM lacks." Neither surface bumps the model version — factor judgments live in a side-table that overlays at read time. The bulk re-eval is non-destructive: controls, assertions, components, sufficiency signatures, and compliance mappings are all unaffected.

Trust Boundaries

Trust boundaries define where security domains meet. Data crossing a trust boundary requires validation and protection. Mipiti identifies boundaries automatically and maps which assets and data flows cross them.

Each boundary carries a closed-vocabulary passes attribute — the set of attack vectors (Network / Adjacent / Local / Physical) that successfully traverse it. A boundary that passes only {Network} blocks Local and Physical attackers from crossing; one that passes everything is a soft demarcation rather than a security control. The passes attribute is the load-bearing input to computed reachability (below) — it turns boundary semantics into a structural set-membership test instead of NLP over a prose description. Operator overrides require a documented change_reason, captured in the model's audit trail alongside the factor-edit pattern.

Computed Reachability

Whether a control objective is reachable — whether the attacker can actually reach the asset for the property under consideration — is computed deterministically by the reachability composer: a pure function over the model's structural primitives (Asset.component_ids, Component.trust_boundary_ids, TrustBoundary.passes, Attacker.trust_boundary_ids + Attacker.attack_vector, Assumption.exclusion). Same inputs always produce the same verdict — no LLM judgment in the predicate, no I/O, no clock, no random. Two structural rules, evaluated in order:

1. Active exclusion-predicate match. An assumption with a structured exclusion predicate that is active and matches the CO (by attacker, asset, property, or explicit co_ids list) makes the CO unreachable. The operator's attestation owns the false-positive risk; the match itself is mechanical.
2. Boundary-vector path. For the boundaries the attacker is positioned at and the boundaries the asset's components reach, every shared boundary blocks the attacker's attack_vector → unreachable. If at least one shared boundary passes the vector → reachable.

These are the only narrowing rules. The composer never narrows reach via inference over loose vocabularies — see "Why no capability-property rule" below.

Verdicts are reachable, unreachable (with a structurally-cited reason — the boundary that blocked or the assumption that excluded), or indeterminate when the attacker isn't positioned, the asset isn't component-scoped, or the two boundary sets don't intersect. The auditor-facing narration is template-generated from the structural verdict — no LLM call to produce the explanation. Indeterminate verdicts default to reachable for CO-coverage purposes (conservative — the CO stays in scope until the operator addresses the gap).

Why no capability-property rule

It would seem natural to add a third rule — "this attacker's capability cannot compromise this property" — but the asymmetry of soundness vs. completeness rules it out. False-unreachable verdicts are dangerous: they silently drop COs that should have controls and produce false security. False-reachable verdicts are merely conservative: extra COs get controls, costing review effort but never missing attacks. The composer is calibrated to that asymmetry. It only narrows reach where the structural justification is mechanical and tight (boundary blocks vector, operator attested exclusion). Capability-property projection requires inference over loose vocabularies (capability classes × asset shapes × property sub-kinds); any wrong cell of such a cross-table silently filters real risk, and the silence makes the failure invisible.

The right mechanism for "this attacker can't compromise this property of this asset" is operator attestation via Assumption.exclusion — class-1 evidence backed by signoff, traceable in the audit trail. Mipiti is valuable even without the reachability filter at all; the two narrowing rules pay for themselves; adding more aggressive structural narrowing trades core correctness for marginal optimization in the wrong direction.

Indeterminate verdicts are model-quality signals, not gaps to silently fill. Each indeterminate CO surfaces as a structural-completeness finding tied to a specific operator action (scope the asset, position the attacker, document an exclusion). The platform never auto-decides what the model is structurally missing — visibility is the right behavior. An auditor reading "5 COs unverified due to missing boundary positioning" can act on it; an auditor reading 5 LLM-rationalized verdicts has no signal that the underlying model is incomplete.

The reachability composer is pure: same inputs always produce the same verdict. A formal TLA+ specification verifies the predicate against the implementation over the closed-vocabulary input space; CI gates on every commit.

Asset → Component scope

Assets carry component_ids — the deployable units that handle them. A multi-instance asset (e.g., a session token flowing through client + cache + DB) lists every component that handles an instance. Reachability flows through this link: the boundaries the asset is "behind" are the union of its components' boundaries. Asset position is derived from this graph, not declared on the asset directly — keeps the asset abstraction intrinsic-property-focused while still letting reachability compute structurally.

Two Evidence-Provenance Classes

A reach claim on a CO can come from two different kinds of evidence, and Mipiti keeps them visibly distinct. The distinction is what makes a Mipiti threat model auditor-verifiable — the auditor doesn't have to trust Mipiti's reasoning; they verify each class by its own mechanism.

The reachability composer is the deterministic-computation surface. Operator non-applicability claims — "attacker T-X cannot reach asset A-Y because [predicate]" — are modeled as Assumption with a structured exclusion predicate, fed back into the composer which then emits unreachable / reason: assumption_excludes. Both signals route through the same composer.

How an auditor verifies a reach claim

1. Hit GET /api/models/{id}/reachability (or GET /api/models/{id}/control-objectives/{co_id} for one CO) — returns the composer's verdict: kind (reachable / unreachable / indeterminate), reason (structural label), narration (template-generated explanation), and structural pointers (boundary_id / assumption_id).
2. If kind is reachable or unreachable, the structural primitives back the verdict. The narration cites which boundary, which exclusion assumption, which attack vector — every value is a field on the model JSON the auditor can re-read.
3. If kind is indeterminate, the composer didn't have enough structural primitives to decide. The coherence report names which (asset_unbounded, attacker_unpositioned, no_shared_boundary, missing_entity); the operator addresses the gap by adding components, positioning attackers, or authoring a structured Assumption.exclusion predicate before audit closure.
4. Re-derive the verdict independently. Pull the model JSON, run compute_co_reachability(model, co) against it locally — the function is short, the inputs are visible, the result is reproducible. Auditor doesn't need to trust Mipiti's runtime.
5. Trace exclusion assumptions through to their attestations. When the verdict is assumption_excludes, the matching assumption's structured exclusion predicate is the structural backing; its attestations are the operator-signoff backing.

The same pattern applies beyond reachability. Impact composition, attacker likelihood, and CO generation are all deterministic-computation surfaces with re-derivation paths. Assertions are machine-verifiable with re-run paths. The auditor's job is connecting the two; the platform's job is keeping them visibly distinct.

Forensic reconstruction across history

The audit chain is durable across time. Three Mipiti-internal mechanisms make any past version's reach state reconstructible without new schema:

• Versioned model JSON. Each model version is immutable and carries that version's assumption.exclusion predicates, assumption.status values, and structural primitives. Re-running the composer against version-N's JSON reproduces version-N's verdicts.
• Timestamped attestations. Filtering by attested_at against a past version's creation window reconstructs which attestations were live then.
• CI-recorded assertion verifications. Every verification persists the commit SHA, the verdict, and the sufficiency signature. The SHA is content-addressed; the codebase at that SHA is immutably referenceable. An auditor re-checkouts the historical SHA and re-runs the same check, getting the same verdict bit-for-bit.

For post-incident or "what did the operator know when?" reconstructions, the chain is: incident timestamp → live model version at that time → version's Assumption.exclusion predicates → attestations live in that window → assertion verifications signed at the relevant commit SHA → re-verifiable today against the same code. None of it depends on the Mipiti runtime being available — the data is content-addressed and signed end-to-end. Mipiti is auditor-verifiable history, not just an auditor-verifiable current state.

Assumptions

Every threat model rests on assumptions. Mipiti makes these explicit and trackable, with a status lifecycle and an attestation mechanism.

Status lifecycle:

• Active — currently accepted as true
• Violated — found to be false (triggers re-evaluation)
• Retired — no longer relevant

Kinds. The Assumption entity covers many semantic kinds, not all of which are reach-exclusions:

The entity is designed to grow more optional structured-claim attachments over time — currently only the exclusion predicate is structured; other kinds remain prose-rationale until the methodology benefits from structuring them. This isn't a backward-compat concession; it's a semantic distinction. Some assumptions are reach-exclusions, others are documentation of context that no graph algorithm would ever touch.