> ## Documentation Index
> Fetch the complete documentation index at: https://docs.alchemicalchef.io/llms.txt
> Use this file to discover all available pages before exploring further.

# TLA+ Specification

> Temporal logic specification for verifying AD tier model safety invariants and state transitions

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

<Info>
  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.
</Info>

## Core Type System

The specification defines the fundamental types and their relationships:

```tla theme={null}
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]}
```

<Info>
  `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.
</Info>

### 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:

```tla theme={null}
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:

```tla theme={null}
AccessAllowed(user, computer) ==
    LET userTier == tierAssignment[user]
        computerTier == tierAssignment[computer]
    IN userTier = computerTier
```

### All Group Memberships

Returns combined direct, nested, and primary group memberships:

```tla theme={null}
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:

```tla theme={null}
TierIsolation ==
    \A u \in Users :
        LET groups == AllGroupMemberships(u)
            adminTiers == {tierAssignment[g] : g \in groups
                          \intersect AdminGroups}
        IN Cardinality(adminTiers \ {"Unassigned"}) <= 1
```

<Tip>
  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.
</Tip>

### 2. Tier0InfrastructurePlacement

Critical infrastructure must remain assigned to Tier 0:

```tla theme={null}
Tier0InfrastructurePlacement ==
    \A c \in tier0Infrastructure :
        tierAssignment[c] = "Tier0"
```

### 3. GpoRestrictionsValid

Each tier must deny logon from other tiers via GPO:

```tla theme={null}
GpoRestrictionsValid ==
    /\ gpoRestrictions["Tier0"] = {"Tier1", "Tier2"}
    /\ gpoRestrictions["Tier1"] = {"Tier0", "Tier2"}
    /\ gpoRestrictions["Tier2"] = {"Tier0", "Tier1"}
```

### 4. ObjectTierConsistency

Admin group memberships must align with assigned tier levels:

```tla theme={null}
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:

```tla theme={null}
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:

```tla theme={null}
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:

```tla theme={null}
Tier1CredentialsProtected ==
    \A c \in Computers :
        tierAssignment[c] = "Tier2" =>
            \A u \in credentialCache[c] :
                tierAssignment[u] /= "Tier1"
```

### 8. NoCircularGroupNesting

Groups cannot transitively contain themselves:

```tla theme={null}
NoCircularGroupNesting ==
    \A g \in Groups :
        g \notin TransitiveGroupClosure(g)
```

### 9. PrimaryGroupConsistency

Primary group assignments must match object tier assignments:

```tla theme={null}
PrimaryGroupConsistency ==
    \A obj \in Objects :
        tierAssignment[primaryGroup[obj]] = tierAssignment[obj]
        \/ tierAssignment[obj] = "Unassigned"
```

### 10. ServiceAccountHardening

Privileged service accounts must be properly secured:

```tla theme={null}
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

```tla theme={null}
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:

<Info>
  Additional actions include `RemoveFromTierGroup`, `RemoveNestedGroupMembership`, `SetPrimaryGroup`, `DesignateTier0Infrastructure`, `RemoveTier0Infrastructure`, `DisableAccount`, `EnableAccount`, and `UpdateLastLogon`. See the [full specification](https://github.com/AlchemicalChef/ADTierModel-Rust/blob/main/specs/ADTierModel.tla) for details.
</Info>

### MoveObjectToTier

Moves an object to a different tier with hardening validation:

```tla theme={null}
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:

```tla theme={null}
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:

```tla theme={null}
AddNestedGroupMembership(childGroup, parentGroup) ==
    /\ childGroup \notin TransitiveGroupClosure(parentGroup)
    /\ nestedGroupMembership' = [nestedGroupMembership EXCEPT
        ![childGroup] = @ \union {parentGroup}]
```

### HardenServiceAccount

Marks a service account as sensitive and disables interactive logon:

```tla theme={null}
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:

```tla theme={null}
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

1. Download and install the [TLA+ Toolbox](https://lamport.azurewebsites.net/tla/toolbox.html)
2. Clone the [ADTierModel-Rust repository](https://github.com/AlchemicalChef/ADTierModel-Rust)

### Model Configuration

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

```text theme={null}
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:

```tla theme={null}
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

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.

<Info>
  The model with the default configuration typically explores several thousand states. Larger configurations exponentially increase the state space.
</Info>

## 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.