Invariant Artifact Specification

Definition#

An Invariant is the heart of CFSE security logic. Invariants are rules that must always hold true for a system to be considered secure. They codify security requirements as formal expressions using predicates, enabling systematic testing and verification.

Every security property in CFSE is expressed as an invariant. Concepts, interactions, flows, scenarios, explorations, and findings all reference invariants - they never inline security logic. This single-source-of-truth approach ensures consistency and maintainability.

Schema: invariant.schema.yaml

Required Fields#

Optional Fields#

Field Details#

rule#

The rule is a plain English statement that communicates the security requirement to stakeholders. It should be:

• Clear: Understandable without reading formal logic
• Unambiguous: One interpretation only
• Actionable: Developers know what to implement

Examples:

• Good: "Only resource owners can delete their own resources"
• Good: "All API endpoints require authentication"
• Bad: "Access control should be enforced" (Too vague)
• Bad: "Users without proper authorization tokens cannot access protected endpoints unless they have admin privileges or the endpoint is marked as public" (Too complex for one rule - split it)

logic#

The logic field contains the formal expression that can be mechanically verified. It uses:

• Quantifiers: FORALL, EXISTS
• Logical operators: AND, OR, NOT, IMPLIES, IFF
• Predicates: P-* references
• Actions: CREATE, READ, UPDATE, DELETE, ACCESS, EXECUTE

The logic must semantically match the rule - they express the same requirement in different forms.

criticality#

Criticality indicates the severity of violating this invariant:

tags#

Tags categorize invariants for filtering and organization:

Formal Logic Operators#

Quantifiers#

Actions#

Key Patterns#

• One invariant = one rule. If a security requirement has multiple independent conditions, split into multiple invariants. Compose them using dependencies.

• Rule and logic must match. The formal logic is the precise version of the English rule. If they say different things, fix the mismatch.

• List all predicates. Every P-* reference in the logic must appear in the predicates array. This enables dependency tracking and validation.

• Use appropriate criticality. Resist the urge to make everything P0. Reserve critical for actual critical issues - authentication bypass, authorization bypass, data breaches.

Common Mistakes#

Example: INV-SHOP-OWNER-DELETE#

id: INV-SHOP-OWNER-DELETE
rule: >
  Only the owner of an item can delete it. Users cannot delete items
  that belong to other users, preventing unauthorized data destruction.
 
logic: |
  FORALL user: C-SHOP-USER.
    FORALL item: C-SHOP-ITEM.
      DELETE(user, item) IMPLIES P-SHOP-IS-OWNER(user, item)
 
predicates:
  - P-SHOP-IS-OWNER
 
criticality: P1
 
tags:
  - authz
  - ownership
 
dependencies:
  - INV-SHOP-AUTH-REQUIRED
 
observability:
  logs:
    - event: "item.deleted"
      fields:
        - user_id
        - item_id
        - item_owner_id
      indicates: holds
    - event: "item.delete.unauthorized"
      fields:
        - user_id
        - item_id
        - item_owner_id
      indicates: violated
 
  metrics:
    - name: shop_delete_attempts_total
      type: counter
      labels:
        - authorized
        - item_type
    - name: shop_unauthorized_deletes_total
      type: counter
      labels:
        - endpoint
      threshold: 0
 
  alerts:
    - name: UnauthorizedDeleteAttempt
      condition: "shop_unauthorized_deletes_total > 0"
      severity: warning
      runbook: "https://wiki.example.com/runbooks/unauthorized-delete"
 
status: ACTIVE

Validation Criteria#

A valid invariant artifact MUST:

1. Have a unique ID matching pattern INV-<SYSTEM>-<NAME>
2. Have a non-empty rule that describes the security requirement in plain English
3. Have valid logic using proper CFSE predicate notation
4. List all predicates used in the logic expression
5. Have a criticality level (P0, P1, P2, or P3)
6. Have at least one tag from the allowed enum
7. Have semantic equivalence between rule and logic (they express the same thing)
8. Reference only existing predicates (predicate IDs should be defined)

Logic Validation#

The logic expression must be syntactically valid:

Predicate Relationship#

Invariants are composed from predicates. Each predicate is an atomic boolean condition:

Predicate: P-SHOP-IS-OWNER
  Parameters: (user: C-SHOP-USER, item: C-SHOP-ITEM)
  Returns: boolean
  Definition: True if user.id equals item.owner_id

Invariant: INV-SHOP-OWNER-DELETE
  Uses: P-SHOP-IS-OWNER
  Logic: FORALL user, item. DELETE(user, item) IMPLIES P-SHOP-IS-OWNER(user, item)

Predicates answer simple yes/no questions. Invariants compose them into security rules.

Related Specifications#

• Grammar Schema - Shared type definitions
• Formal Logic - Complete logic specification
• Concept Artifact - Concepts that invariants govern
• Predicate Specification - Atomic boolean conditions
• Invariant Library Specification - Canonical packaging format for many invariants/predicates

Common Pitfalls#

• Writing invariants that aren’t decidable from evidence (no clear observable conditions).
• Referencing predicates in logic but not listing them in predicates[] (breaks traceability).
• Encoding policy logic in other artifacts (like PRJ); invariants are SSOT for logic.