Skip to main content
Formal verification uses mathematical methods to prove that a system satisfies specific security properties. Unlike testing, which can only show the presence of bugs, formal methods can prove their absence within a defined model. All of my software that I publish includes some degree of formal validation alongside the code. Here is the formal model of the AD Tier Model platform so you can see how it works.

​
Why Formal Verification?

Traditional security testing has limitations:
ApproachStrengthsLimitations
Penetration TestingFinds real exploitsPoint-in-time, incomplete coverage
Code ReviewCatches implementation bugsMisses design flaws, doesn’t scale
Static AnalysisAutomated, fastHigh false positive rate, limited depth
Formal VerificationMathematical proof of propertiesRequires modeling effort
Formal verification provides guarantees that the tier model design, when properly implemented, prevents entire classes of attacks rather than just specific vulnerabilities.
The formal models serve as executable specifications. They define what the tier model should do and can be checked automatically by model checkers to verify correctness.

​
The Two Specifications

The AD Tier Model uses two complementary formal methods:

TLA+ Specification

Verifies temporal properties and state transitions. Ensures the system maintains safety invariants as administrators perform operations over time.

Alloy Specification

Analyzes ACL structure for privilege escalation paths. Detects attack chains like DCSync, RBCD abuse, and cross-tier compromise.

​
TLA+ for Temporal Verification

TLA+ (Temporal Logic of Actions) models the system as a state machine. It verifies that:
  • Safety properties hold in all reachable states (e.g., no user ever has cross-tier admin access)
  • Liveness properties ensure progress (e.g., unhardened service accounts eventually get hardened)
  • State transitions preserve tier isolation during administrative operations
The TLA+ specification defines 10 core safety invariants covering tier isolation, credential protection, and service account hardening.

​
Alloy for Structural Analysis

Alloy uses relational logic and constraint solving to analyze the structure of Active Directory permissions. It verifies that:
  • No attack paths exist from lower tiers to higher tiers
  • ACL configurations don’t allow privilege escalation
  • Protected groups remain secure from unauthorized modification
The Alloy specification includes 11 attack predicates covering DCSync exploitation, Shadow Credentials, Resource-Based Constrained Delegation abuse, and more.

​
How They Complement Each Other

AspectTLA+Alloy
FocusBehavior over timeStatic structure
Question Answered”Does the system stay safe during operations?""Are there any attack paths in this configuration?”
Verification TypeModel checking (exhaustive state exploration)SAT solving (constraint satisfaction)
FindsUnsafe state transitions, missing guardsPrivilege escalation paths, ACL misconfigurations
Together, the specifications ensure that:
  1. The tier model design is sound (TLA+)
  2. Specific AD configurations don’t have exploitable weaknesses (Alloy)
Use the TLA+ model to verify your tier model procedures are correct. Use the Alloy model to analyze your actual AD configuration for attack paths.

​
Getting the Specifications

The formal specifications are available in the ADTierModel-Rust repository: 
specs/
├── ADTierModel.tla      # TLA+ temporal specification
├── ADTierModel.cfg      # TLC model checker configuration
└── ADTierModel_ACL.als  # Alloy structural specification

​
Next Steps

TLA+ Deep Dive

Explore the 10 safety invariants and how to run the TLC model checker

Alloy Deep Dive

Learn about attack path detection and running the Alloy Analyzer