TLA+ Specification - AlchemicalChef

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

AdminGroups == \* Subset of Groups designated as administrative
    {g \in Groups : isAdminGroup[g]}

AdminGroups represents the subset of groups that grant administrative privileges within a tier. The exact membership is defined by your organization’s tier model implementation.

State Variables

The model tracks the following state:

Variable	Type	Description
`tierAssignment`	Object → Tier	Current tier for each object
`groupMembership`	Object → Set(Group)	Direct group memberships
`nestedGroupMembership`	Group → Set(Group)	Parent groups that each group is a member of
`primaryGroup`	Object → Group	Primary group (for POSIX compatibility)
`activeSessions`	Computer → Set(User)	Currently logged-in users
`credentialCache`	Computer → Set(User)	Cached credentials on each computer
`gpoRestrictions`	Tier → Set(Tier)	Logon restrictions per tier
`tier0Infrastructure`	Set(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 limits blast radius, if an administrative account is compromised, the attacker only gains access to a single tier rather than the entire environment.

2. Tier0InfrastructurePlacement

Critical infrastructure must remain assigned to Tier 0:

Tier0InfrastructurePlacement ==
    \A c \in tier0Infrastructure :
        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

Violation	Severity Weight	Description
Cross-tier admin access	20	User in admin groups across multiple tiers
Misplaced Tier 0 infrastructure	25	Critical system not in Tier 0
Wrong tier placement	15	Object in incorrect tier
Unhardened service account	10	Service account not marked sensitive
Interactive service account	10	Service account allows interactive logon
Stale account	5	Account 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, primaryGroup,
                   activeSessions, credentialCache, gpoRestrictions>>

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) ==
    /\ childGroup \notin TransitiveGroupClosure(parentGroup)
    /\ nestedGroupMembership' = [nestedGroupMembership EXCEPT
        ![childGroup] = @ \union {parentGroup}]

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]

Complete Specification

The full specification combines the initial state, next-state relation, and fairness conditions:

vars == <<tierAssignment, groupMembership, nestedGroupMembership,
          primaryGroup, activeSessions, credentialCache,
          gpoRestrictions, tier0Infrastructure, isSensitive,
          interactiveLogonAllowed, lastLogon, accountEnabled>>

Next ==
    \/ \E obj \in Objects, tier \in Tiers : MoveObjectToTier(obj, tier)
    \/ \E obj \in Objects, g \in AdminGroups : AddToTierGroup(obj, g)
    \/ \E child, parent \in Groups : AddNestedGroupMembership(child, parent)
    \/ \E sa \in ServiceAccounts : HardenServiceAccount(sa)
    \* ... additional actions

Spec == Init /\ [][Next]_vars

Running the Model

Prerequisites

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

Model Configuration

The ADTierModel.cfg file configures the model checker. TLC configuration files use the following format:

CONSTANT Users = {u1, u2}
CONSTANT Computers = {c1, c2}
CONSTANT Groups = {g0a, g0b, g1a, g1b, g2a, g2b}
CONSTANT ServiceAccounts = {sa1}

CONSTRAINT StateConstraint

INVARIANT TierIsolation
INVARIANT Tier0InfrastructurePlacement
INVARIANT GpoRestrictionsValid
INVARIANT ObjectTierConsistency
INVARIANT NoCrossTierSessions
INVARIANT Tier0CredentialsProtected
INVARIANT Tier1CredentialsProtected
INVARIANT NoCircularGroupNesting
INVARIANT PrimaryGroupConsistency
INVARIANT ServiceAccountHardening

The StateConstraint operator bounds the state space for finite model checking:

StateConstraint ==
    /\ \A g \in Groups : Cardinality(nestedGroupMembership[g]) <= 2
    /\ \A c \in Computers : Cardinality(activeSessions[c]) <= 3
    /\ \A c \in Computers : Cardinality(credentialCache[c]) <= 2

Running TLC

Open ADTierModel.tla in the TLA+ Toolbox
Create a new model using the configuration
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:

The initial state
Each action taken
The state where the invariant was violated
Which invariant failed

Use this trace to identify gaps in your administrative procedures.

​Overview

​Core Type System

​State Variables

​Helper Functions

​Transitive Group Closure

​Access Validation

​All Group Memberships

​Safety Invariants

​1. TierIsolation

​2. Tier0InfrastructurePlacement

​3. GpoRestrictionsValid

​4. ObjectTierConsistency

​5. NoCrossTierSessions

​6. Tier0CredentialsProtected

​7. Tier1CredentialsProtected

​8. NoCircularGroupNesting

​9. PrimaryGroupConsistency

​10. ServiceAccountHardening

​Compliance Detection

​Violation Types

​Compliance Score

​Administrative Actions

​MoveObjectToTier

​AddToTierGroup

​AddNestedGroupMembership

​HardenServiceAccount

​Complete Specification

​Running the Model

​Prerequisites

​Model Configuration

​Running TLC

​Interpreting Results

​No Violations Found

​Violation Found

Overview

Core Type System

State Variables

Helper Functions

Transitive Group Closure

Access Validation

All Group Memberships

Safety Invariants

1. TierIsolation

2. Tier0InfrastructurePlacement

3. GpoRestrictionsValid

4. ObjectTierConsistency

5. NoCrossTierSessions

6. Tier0CredentialsProtected

7. Tier1CredentialsProtected

8. NoCircularGroupNesting

9. PrimaryGroupConsistency

10. ServiceAccountHardening

Compliance Detection

Violation Types

Compliance Score

Administrative Actions

MoveObjectToTier

AddToTierGroup

AddNestedGroupMembership

HardenServiceAccount

Complete Specification

Running the Model

Prerequisites

Model Configuration

Running TLC

Interpreting Results

No Violations Found

Violation Found