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

# Alloy Specification

> Constraint-based ACL analysis for detecting privilege escalation attack paths across the AD tier model

<Note>
  This page assumes familiarity with Alloy. If you're new to the language, start with [Alloy Basics](/formal-methods/alloy-basics) and the [Alloy Syntax Guide](/formal-methods/alloy-syntax-guide).
</Note>

The Alloy specification performs structural analysis of Active Directory access control lists to detect privilege escalation paths. It uses constraint solving to find configurations where lower-tier principals can compromise higher-tier resources.

## Overview

Alloy is a declarative modeling language based on first-order relational logic. Unlike TLA+ which focuses on temporal behavior, Alloy excels at analyzing static structural properties and finding counterexamples to security assertions.

For the AD tier model, Alloy verifies that:

* No attack paths exist from Tier 2 to Tier 0
* DCSync rights are restricted to Tier 0
* Protected groups cannot be modified by lower tiers
* Resource-Based Constrained Delegation cannot be abused for escalation

<Info>
  The Alloy model performs analysis similar to BloodHound but with formal guarantees. It finds all possible attack paths within the modeled permissions, not just known patterns.
</Info>

## Data Model

### Principal Hierarchy

```alloy theme={null}
abstract sig ADObject {
    securityDescriptor: one SecurityDescriptor
}

abstract sig Principal extends ADObject {
    memberOf: set Group,
    tier: one Tier
}

sig User extends Principal {
    sessions: set Computer
}

sig Computer extends Principal {
    allowedToActOnBehalf: set Principal  // RBCD
}

sig Group extends Principal {
    members: set Principal
}

sig ServiceAccount extends Principal {
    spn: lone SPN,
    constrainedDelegationTargets: set Principal
}

sig SPN {}
```

### Container Structure

```alloy theme={null}
sig OrganizationalUnit extends ADObject {
    contains: set ADObject,
    parentOU: lone OrganizationalUnit
}

sig Domain extends ADObject {
    rootOU: one OrganizationalUnit,
    domainAdmins: one Group,
    enterpriseAdmins: one Group,
    schemaAdmins: one Group
}
```

### Tier Model

```alloy theme={null}
abstract sig Tier {}
one sig Tier0, Tier1, Tier2, Unassigned extends Tier {}

fun tierLevel[t: Tier]: Int {
    t = Tier0 => 0 else
    t = Tier1 => 1 else
    t = Tier2 => 2 else 3
}

pred higherPrivilege[t1, t2: Tier] {
    tierLevel[t1] < tierLevel[t2]
}
```

## Security Descriptors and ACLs

### ACL Structure

```alloy theme={null}
sig SecurityDescriptor {
    owner: one Principal,
    dacl: one DACL,
    sacl: lone SACL
}

sig DACL {
    aces: set ACE
}

sig SACL {
    aces: set ACE
}

sig ACE {
    trustee: one Principal,
    rights: set Right,
    extendedRights: set ExtendedRightGUID,
    propertyRights: set PropertyGUID,
    aceType: one ACEType,
    inherited: Bool,
    objectType: lone ObjectTypeGUID,
    inheritedObjectType: lone ObjectTypeGUID
}

abstract sig ACEType {}
one sig Allow, Deny extends ACEType {}

abstract sig Bool {}
one sig True, False extends Bool {}

sig ObjectTypeGUID {}
```

### Permission Rights

The specification models the full range of AD permissions:

**Control Rights**

```alloy theme={null}
abstract sig Right {}

// Generic rights
one sig GenericAll, GenericRead, GenericWrite extends Right {}

// ACL modification rights
one sig WriteDacl, WriteOwner extends Right {}
```

**Object Rights**

```alloy theme={null}
one sig CreateChild, DeleteChild, Delete extends Right {}
one sig ListChildren, ListObject extends Right {}
```

**Property Rights**

```alloy theme={null}
one sig WriteProperty, ReadProperty extends Right {}
one sig Self_, ExtendedRight extends Right {}
```

**Extended Rights (by GUID)**

```alloy theme={null}
abstract sig ExtendedRightGUID {}

one sig UserForceChangePassword extends ExtendedRightGUID {}
one sig DS_Replication_Get_Changes extends ExtendedRightGUID {}
one sig DS_Replication_Get_Changes_All extends ExtendedRightGUID {}
one sig WriteMember extends ExtendedRightGUID {}
```

**Security-Sensitive Properties**

```alloy theme={null}
abstract sig PropertyGUID {}

one sig ServicePrincipalNameProperty extends PropertyGUID {}      // Kerberoasting
one sig MsDS_AllowedToActOnBehalfProperty extends PropertyGUID {} // RBCD
one sig UserPasswordProperty extends PropertyGUID {}
one sig MsDS_KeyCredentialLink extends PropertyGUID {}            // Shadow Credentials
```

## Protected Groups

Well-known privileged groups are automatically assigned to Tier 0:

```alloy theme={null}
sig ProtectedGroup in Group {}

fact ProtectedGroupsAreTier0 {
    all g: ProtectedGroup | g.tier = Tier0
}

fact WellKnownProtectedGroups {
    Domain.domainAdmins in ProtectedGroup
    Domain.enterpriseAdmins in ProtectedGroup
    Domain.schemaAdmins in ProtectedGroup
}
```

## Attack Path Detection

The specification includes 11 predicates for discovering attack paths. The examples below show the conceptual approach; see the [full specification](https://github.com/AlchemicalChef/ADTierModel-Rust/blob/main/specs/ADTierModel_ACL.als) for exact implementation.

### Effective Trustee Resolution

Determines if a principal matches an ACE trustee (directly or through group membership):

```alloy theme={null}
pred effectiveTrustee[ace: ACE, p: Principal] {
    p = ace.trustee or ace.trustee in p.^memberOf
}
```

### Core Compromise Predicate

Determines if a principal can compromise a target:

```alloy theme={null}
pred canCompromise[attacker: Principal, target: Principal] {
    attacker != target and (
        canModifyDACL[attacker, target] or
        canForcePasswordChange[attacker, target] or
        canAddToGroup[attacker, target] or
        hasDCSyncRights[attacker] or
        canConfigureRBCD[attacker, target] or
        canSetSPN[attacker, target] or
        canWriteShadowCredentials[attacker, target] or
        canAbuseDelegation[attacker, target]
    )
}
```

### Attack Scenarios

#### 1. WriteDACL/WriteOwner Abuse

```alloy theme={null}
pred canModifyDACL[attacker: Principal, target: Principal] {
    let sd = target.securityDescriptor |
    some ace: sd.dacl.aces |
        ace.aceType = Allow and
        effectiveTrustee[ace, attacker] and
        (WriteDacl in ace.rights or WriteOwner in ace.rights or
         GenericAll in ace.rights)
}
```

Attackers with WriteDACL can grant themselves any permission. WriteOwner allows taking ownership and then modifying the DACL.

#### 2. Group Membership Manipulation

```alloy theme={null}
pred canAddToGroup[attacker: Principal, targetGroup: Group] {
    some ace: targetGroup.securityDescriptor.dacl.aces |
        ace.aceType = Allow and
        effectiveTrustee[ace, attacker] and
        (WriteMember in ace.extendedRights or
         GenericAll in ace.rights or
         GenericWrite in ace.rights)
}
```

Adding oneself to Domain Admins provides immediate Tier 0 access.

#### 3. Password Reset Attacks

```alloy theme={null}
pred canForcePasswordChange[attacker: Principal, target: User] {
    some ace: target.securityDescriptor.dacl.aces |
        ace.aceType = Allow and
        effectiveTrustee[ace, attacker] and
        (UserForceChangePassword in ace.extendedRights or
         GenericAll in ace.rights)
}
```

<Tip>
  Password reset attacks are particularly dangerous when targeting service accounts, as these accounts often have elevated privileges and run critical services. Accounts with SPNs are especially valuable since resetting their password grants immediate access to the services they operate.
</Tip>

#### 4. DCSync Exploitation

```alloy theme={null}
pred hasDCSyncRights[attacker: Principal] {
    some ace: Domain.securityDescriptor.dacl.aces |
        ace.aceType = Allow and
        effectiveTrustee[ace, attacker] and
        DS_Replication_Get_Changes in ace.extendedRights and
        DS_Replication_Get_Changes_All in ace.extendedRights
}
```

DCSync allows extracting all password hashes from AD, equivalent to full domain compromise.

#### 5. Resource-Based Constrained Delegation (RBCD)

```alloy theme={null}
pred canConfigureRBCD[attacker: Principal, target: Computer] {
    some ace: target.securityDescriptor.dacl.aces |
        ace.aceType = Allow and
        effectiveTrustee[ace, attacker] and
        (MsDS_AllowedToActOnBehalfProperty in ace.propertyRights or
         GenericAll in ace.rights or
         GenericWrite in ace.rights)
}

pred canAbuseRBCD[attacker: Principal, target: Computer] {
    canConfigureRBCD[attacker, target] and
    some sa: ServiceAccount |
        sa.tier = attacker.tier and
        some sa.spn
}
```

RBCD abuse requires write access to `msDS-AllowedToActOnBehalfOfOtherIdentity` plus a controlled account with an SPN.

#### 6. SPN Manipulation (Kerberoasting Setup)

```alloy theme={null}
pred canSetSPN[attacker: Principal, target: User] {
    some ace: target.securityDescriptor.dacl.aces |
        ace.aceType = Allow and
        effectiveTrustee[ace, attacker] and
        (ServicePrincipalNameProperty in ace.propertyRights or
         GenericAll in ace.rights or
         GenericWrite in ace.rights)
}
```

Setting an SPN on a user enables Kerberoasting their password hash.

#### 7. Shadow Credentials

```alloy theme={null}
pred canWriteShadowCredentials[attacker: Principal, target: Principal] {
    some ace: target.securityDescriptor.dacl.aces |
        ace.aceType = Allow and
        effectiveTrustee[ace, attacker] and
        (MsDS_KeyCredentialLink in ace.propertyRights or
         GenericAll in ace.rights or
         GenericWrite in ace.rights)
}
```

Writing to `msDS-KeyCredentialLink` allows authentication as the target without knowing their password.

#### 8. Constrained Delegation Abuse

```alloy theme={null}
pred canAbuseDelegation[attacker: Principal, target: Principal] {
    some sa: ServiceAccount |
        (attacker = sa or canCompromise[attacker, sa]) and
        target in sa.constrainedDelegationTargets
}
```

An attacker can abuse constrained delegation if they control a service account (directly or through compromise) that has delegation rights to the target.

#### 9. Cross-Tier Compromise Chains

```alloy theme={null}
pred crossTierViolation[attacker: Principal, target: Principal] {
    higherPrivilege[target.tier, attacker.tier] and
    canCompromise[attacker, target]
}

fun compromiseTargets[p: Principal]: set Principal {
    {t: Principal | canCompromise[p, t]}
}

pred transitiveCompromise[attacker: Principal, target: Principal] {
    target in attacker.^compromiseTargets
}
```

## Security Assertions

The specification includes 9 key assertions that verify tier isolation:

### 1. NoTier2ToTier0Path

```alloy theme={null}
assert NoTier2ToTier0Path {
    no attacker: Principal, target: Principal |
        attacker.tier = Tier2 and
        target.tier = Tier0 and
        transitiveCompromise[attacker, target]
}
check NoTier2ToTier0Path for 6
```

### 2. NoTier1ToTier0Path

```alloy theme={null}
assert NoTier1ToTier0Path {
    no attacker: Principal, target: Principal |
        attacker.tier = Tier1 and
        target.tier = Tier0 and
        transitiveCompromise[attacker, target]
}
check NoTier1ToTier0Path for 6
```

### 3. TierIsolationMaintained

```alloy theme={null}
assert TierIsolationMaintained {
    no attacker, target: Principal |
        crossTierViolation[attacker, target]
}
check TierIsolationMaintained for 6
```

### 4. DCSyncOnlyTier0

```alloy theme={null}
assert DCSyncOnlyTier0 {
    all p: Principal |
        hasDCSyncRights[p] implies p.tier = Tier0
}
check DCSyncOnlyTier0 for 6
```

### 5. ProtectedGroupsSecure

```alloy theme={null}
assert ProtectedGroupsSecure {
    all g: ProtectedGroup, p: Principal |
        canAddToGroup[p, g] implies p.tier = Tier0
}
check ProtectedGroupsSecure for 6
```

### 6. NoRBCDEscalation

```alloy theme={null}
assert NoRBCDEscalation {
    no attacker: Principal, target: Computer |
        higherPrivilege[target.tier, attacker.tier] and
        canAbuseRBCD[attacker, target]
}
check NoRBCDEscalation for 6
```

### 7. NoDanglingOwners

```alloy theme={null}
assert NoDanglingOwners {
    all sd: SecurityDescriptor |
        sd.owner in Principal
}
check NoDanglingOwners for 6
```

### 8. NoTier2ToTier1Path

```alloy theme={null}
assert NoTier2ToTier1Path {
    no attacker: Principal, target: Principal |
        attacker.tier = Tier2 and
        target.tier = Tier1 and
        transitiveCompromise[attacker, target]
}
check NoTier2ToTier1Path for 6
```

### 9. NoSelfEscalationToProtectedGroups

```alloy theme={null}
assert NoSelfEscalationToProtectedGroups {
    no p: Principal, g: ProtectedGroup |
        p.tier != Tier0 and
        canAddToGroup[p, g] and
        p in g.members
}
check NoSelfEscalationToProtectedGroups for 6
```

## Running the Model

### Prerequisites

1. Download and install the [Alloy Analyzer](https://alloytools.org/download.html)
2. Clone the [ADTierModel-Rust repository](https://github.com/AlchemicalChef/ADTierModel-Rust)

### Basic Analysis

1. Open `ADTierModel_ACL.als` in the Alloy Analyzer
2. Select an assertion to check (e.g., `NoTier2ToTier0Path`)
3. Click "Execute" to run the analysis

### Understanding Scope

The `for N` clause limits the search space:

```alloy theme={null}
check NoTier2ToTier0Path for 6
```

This checks the assertion for configurations with up to 6 instances of each signature. Larger scopes find more issues but take longer.

### Interpreting Results

**No Counterexample Found**

The assertion holds for all configurations within the specified scope. This provides high confidence but not absolute proof.

**Counterexample Found**

Alloy displays a concrete configuration showing:

* The principals involved
* Their tier assignments
* The ACL configuration that enables the attack
* The specific permissions being exploited

<Info>
  Counterexamples are visualized as graphs, making it easy to understand the attack path. Each node represents an AD object, and edges show relationships and permissions.
</Info>

## Extending the Model

### Adding New Attack Patterns

To model a new attack technique:

1. Define any new permission types or properties
2. Create a predicate describing the attack conditions
3. Add the predicate to `canCompromise`
4. Create an assertion verifying tier isolation against the attack

### Analyzing Your Environment

Export your AD configuration to Alloy format:

1. Extract ACLs using PowerShell or tools like BloodHound
2. Transform to Alloy facts defining your specific principals and permissions
3. Run assertions to identify actual attack paths

```alloy theme={null}
// Example: Defining your environment
one sig MyDomain extends Domain {}
one sig AdminUser extends User {} { tier = Tier0 }
one sig HelpDeskUser extends User {} { tier = Tier2 }
one sig FileServer extends Computer {} { tier = Tier1 }

fact MyACLs {
    // Define actual permissions from your environment
}
```