invariant-analysislisted

# Invariant Analysis ## Purpose Enumerate security claims made by a design, formalize them as invariants, check for hidden assumptions, assess verification feasibility, and propose a specification approach for proving or disproving the claims. ## Scope Constraints Reads system designs, security documentation, and existing formal specifications. Does not modify implementation code or execute verification tools. Does not access production systems for testing. ## Inputs - System design with stated or implied security claims - Threat model defining attacker capabilities - Architecture documentation describing components and interactions - Existing tests or verification results - Constraints on verification effort (time, tools, expertise) ## Input Sanitization No user-provided values are used in commands or file paths. All inputs are treated as read-only analysis targets. ## Procedure ### Step 1: Enumerate Security Claims Extract all security claims from the design, whether explicit or implicit: - **Explicit claims**: Stated in documentation ("the system ensures mutual exclusion") - **Implicit claims**: Assumed but not stated ("processes always terminate") - **Derived claims**: Inferred from the design ("if A holds and B holds, then C should hold") - For each claim, identify who makes it, what components it depends on, and what could violate it ### Step 2: Formalize as Invariants For each security claim, produce a formal invariant: - Express the claim as a precise predica