Skip to main content
The TLA+ specification models the AD tier model as a state machine, verifying that safety properties hold across all possible sequences of administrative operations. It uses the TLC model checker to exhaustively explore the state space.

​
Overview

TLA+ (Temporal Logic of Actions) is a formal specification language developed by Leslie Lamport. It excels at modeling concurrent and distributed systems where correctness depends on the order and interleaving of operations. For the AD tier model, TLA+ verifies that:
  • No administrative action can create cross-tier access
  • Credentials never leak from higher to lower tiers
  • Service accounts remain properly hardened
  • Group nesting never creates circular dependencies
The specification implements the equivalent of LDAP’s LDAP_MATCHING_RULE_IN_CHAIN (OID 1.2.840.113556.1.4.1941) for transitive group membership resolution.

​
Core Type System

The specification defines the fundamental types and their relationships: 
CONSTANTS
    Users,              \* Set of user objects
    Computers,          \* Set of computer objects
    Groups,             \* Set of group objects
    ServiceAccounts     \* Set of service account objects

Tiers == {"Tier0", "Tier1", "Tier2", "Unassigned"}

Objects == Users \union Computers \union Groups \union ServiceAccounts

​
State Variables

The model tracks the following state:
VariableTypeDescription
tierAssignmentObject → TierCurrent tier for each object
groupMembershipObject → Set(Group)Direct group memberships
nestedGroupMembershipGroup → Set(Group)Groups that are members of other groups
primaryGroupObject → GroupPrimary group (for POSIX compatibility)
activeSessionsComputer → Set(User)Currently logged-in users
credentialCacheComputer → Set(User)Cached credentials on each computer
gpoRestrictionsTier → Set(Tier)Logon restrictions per tier
tier0InfrastructureSet(Computer)Systems that must remain Tier 0

​
Helper Functions

​
Transitive Group Closure

Computes all groups a principal belongs to through nested membership: 
TransitiveGroupClosure(obj) ==
    LET
        DirectGroups == groupMembership[obj]

        RECURSIVE Expand(_)
        Expand(groups) ==
            LET newGroups == UNION {nestedGroupMembership[g] : g \in groups}
            IN IF newGroups \subseteq groups
               THEN groups
               ELSE Expand(groups \union newGroups)
    IN Expand(DirectGroups)

​
Access Validation

Determines if a user can access a resource based on tier assignment: 
AccessAllowed(user, computer) ==
    LET userTier == tierAssignment[user]
        computerTier == tierAssignment[computer]
    IN userTier = computerTier

​
All Group Memberships

Returns combined direct, nested, and primary group memberships: 
AllGroupMemberships(obj) ==
    TransitiveGroupClosure(obj) \union {primaryGroup[obj]}

​
Safety Invariants

The specification defines 10 core safety invariants that must hold in every reachable state.

​
1. TierIsolation

No user can hold administrative privileges across multiple tiers: 
TierIsolation ==
    \A u \in Users :
        LET groups == AllGroupMemberships(u)
            adminTiers == {tierAssignment[g] : g \in groups
                          \intersect AdminGroups}
        IN Cardinality(adminTiers \ {"Unassigned"}) <= 1
This invariant prevents the “Golden Ticket” scenario where a single compromised account can access all tiers.

​
2. Tier0InfrastructurePlacement

Critical infrastructure must remain assigned to Tier 0: 
Tier0InfrastructurePlacement ==
    \A c \in criticalInfrastructure :
        tierAssignment[c] = "Tier0"

​
3. GpoRestrictionsValid

Each tier must deny logon from other tiers via GPO: 
GpoRestrictionsValid ==
    /\ gpoRestrictions["Tier0"] = {"Tier1", "Tier2"}
    /\ gpoRestrictions["Tier1"] = {"Tier0", "Tier2"}
    /\ gpoRestrictions["Tier2"] = {"Tier0", "Tier1"}

​
4. ObjectTierConsistency

Admin group memberships must align with assigned tier levels: 
ObjectTierConsistency ==
    \A obj \in Objects :
        \A g \in groupMembership[obj] \intersect AdminGroups :
            tierAssignment[g] = tierAssignment[obj]
            \/ tierAssignment[obj] = "Unassigned"

​
5. NoCrossTierSessions

Active sessions must respect tier boundaries: 
NoCrossTierSessions ==
    \A c \in Computers :
        \A u \in activeSessions[c] :
            tierAssignment[u] = tierAssignment[c]

​
6. Tier0CredentialsProtected

Tier 0 credentials cannot be cached on lower-tier systems: 
Tier0CredentialsProtected ==
    \A c \in Computers :
        tierAssignment[c] /= "Tier0" =>
            \A u \in credentialCache[c] :
                tierAssignment[u] /= "Tier0"

​
7. Tier1CredentialsProtected

Tier 1 credentials cannot be cached on Tier 2 systems: 
Tier1CredentialsProtected ==
    \A c \in Computers :
        tierAssignment[c] = "Tier2" =>
            \A u \in credentialCache[c] :
                tierAssignment[u] /= "Tier1"

​
8. NoCircularGroupNesting

Groups cannot transitively contain themselves: 
NoCircularGroupNesting ==
    \A g \in Groups :
        g \notin TransitiveGroupClosure(g)

​
9. PrimaryGroupConsistency

Primary group assignments must match object tier assignments: 
PrimaryGroupConsistency ==
    \A obj \in Objects :
        tierAssignment[primaryGroup[obj]] = tierAssignment[obj]
        \/ tierAssignment[obj] = "Unassigned"

​
10. ServiceAccountHardening

Privileged service accounts must be properly secured: 
ServiceAccountHardening ==
    \A sa \in ServiceAccounts :
        tierAssignment[sa] \in {"Tier0", "Tier1"} =>
            /\ isSensitive[sa] = TRUE
            /\ interactiveLogonAllowed[sa] = FALSE

​
Compliance Detection

The specification identifies and quantifies violations:

​
Violation Types

ViolationSeverity WeightDescription
Cross-tier admin access20User in admin groups across multiple tiers
Misplaced Tier 0 infrastructure25Critical system not in Tier 0
Wrong tier placement15Object in incorrect tier
Unhardened service account10Service account not marked sensitive
Interactive service account10Service account allows interactive logon
Stale account5Account inactive for 90+ days

​
Compliance Score

ComplianceScore ==
    LET
        totalViolationPoints ==
            (CrossTierViolations * 20) +
            (MisplacedInfraViolations * 25) +
            (WrongTierViolations * 15) +
            (UnhardenedSAViolations * 10) +
            (InteractiveSAViolations * 10) +
            (StaleAccountViolations * 5)
        totalObjects == Cardinality(Objects)
    IN 100 - ((totalViolationPoints * 100) \div (totalObjects * 10))

​
Administrative Actions

The specification models 12 state transitions. The key actions are shown below:
Additional actions include RemoveFromTierGroup, RemoveNestedGroupMembership, SetPrimaryGroup, DesignateTier0Infrastructure, RemoveTier0Infrastructure, DisableAccount, EnableAccount, and UpdateLastLogon. See the full specification for details.

​
MoveObjectToTier

Moves an object to a different tier with hardening validation: 
MoveObjectToTier(obj, newTier) ==
    /\ newTier \in {"Tier0", "Tier1"} =>
        (obj \in ServiceAccounts => isSensitive[obj])
    /\ tierAssignment' = [tierAssignment EXCEPT ![obj] = newTier]
    /\ UNCHANGED <<groupMembership, nestedGroupMembership, ...>>

​
AddToTierGroup

Adds an object to a tier group, preventing cross-tier membership: 
AddToTierGroup(obj, group) ==
    /\ group \in AdminGroups
    /\ LET currentAdminTiers == {tierAssignment[g] :
           g \in AllGroupMemberships(obj) \intersect AdminGroups}
       IN currentAdminTiers = {} \/
          currentAdminTiers = {tierAssignment[group]}
    /\ groupMembership' = [groupMembership EXCEPT
        ![obj] = @ \union {group}]

​
AddNestedGroupMembership

Adds a group as a member of another group, preventing cycles: 
AddNestedGroupMembership(childGroup, parentGroup) ==
    /\ parentGroup \notin TransitiveGroupClosure(childGroup)
    /\ nestedGroupMembership' = [nestedGroupMembership EXCEPT
        ![parentGroup] = @ \union {childGroup}]

​
HardenServiceAccount

Marks a service account as sensitive and disables interactive logon: 
HardenServiceAccount(sa) ==
    /\ sa \in ServiceAccounts
    /\ isSensitive' = [isSensitive EXCEPT ![sa] = TRUE]
    /\ interactiveLogonAllowed' = [interactiveLogonAllowed EXCEPT
        ![sa] = FALSE]

​
Running the Model

​
Prerequisites

  1. Download and install the TLA+ Toolbox
  2. Clone the ADTierModel-Rust repository

​
Model Configuration

The ADTierModel.cfg file configures the model checker: 
CONSTANTS
    Users = {u1, u2}
    Computers = {c1, c2}
    Groups = {g0a, g0b, g1a, g1b, g2a, g2b}
    ServiceAccounts = {sa1}

CONSTRAINT
    \* Bound state space for finite model checking
    Cardinality(nestedGroupMembership[g]) <= 2
    Cardinality(activeSessions) <= 3
    Cardinality(credentialCache[c]) <= 2

INVARIANTS
    TierIsolation
    Tier0InfrastructurePlacement
    GpoRestrictionsValid
    ObjectTierConsistency
    NoCrossTierSessions
    Tier0CredentialsProtected
    Tier1CredentialsProtected
    NoCircularGroupNesting
    PrimaryGroupConsistency
    ServiceAccountHardening

​
Running TLC

  1. Open ADTierModel.tla in the TLA+ Toolbox
  2. Create a new model using the configuration
  3. Run the model checker
TLC will explore all reachable states and report any invariant violations with a counterexample trace showing the sequence of actions that led to the violation.
The model with the default configuration typically explores several thousand states. Larger configurations exponentially increase the state space.

​
Interpreting Results

​
No Violations Found

If TLC completes without errors, the tier model design is verified to maintain all safety invariants under the configured constraints.

​
Violation Found

TLC provides a trace showing:
  1. The initial state
  2. Each action taken
  3. The state where the invariant was violated
  4. Which invariant failed
Use this trace to identify gaps in your administrative procedures.