Alloy Specification - AlchemicalChef

This page assumes familiarity with Alloy. If you’re new to the language, start with Alloy Basics and the Alloy Syntax Guide.

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

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.

Data Model

Principal Hierarchy

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

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

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

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

abstract sig Right {}

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

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

Object Rights

one sig CreateChild, DeleteChild, Delete extends Right {}
one sig ListChildren, ListObject extends Right {}

Property Rights

one sig WriteProperty, ReadProperty extends Right {}
one sig Self_, ExtendedRight extends Right {}

Extended Rights (by GUID)

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

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:

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 for exact implementation.

Effective Trustee Resolution

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

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:

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

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

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

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)
}

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.

4. DCSync Exploitation

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)

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)

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

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

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

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

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

2. NoTier1ToTier0Path

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

3. TierIsolationMaintained

assert TierIsolationMaintained {
    no attacker, target: Principal |
        crossTierViolation[attacker, target]
}
check TierIsolationMaintained for 6

4. DCSyncOnlyTier0

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

5. ProtectedGroupsSecure

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

6. NoRBCDEscalation

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

7. NoDanglingOwners

assert NoDanglingOwners {
    all sd: SecurityDescriptor |
        sd.owner in Principal
}
check NoDanglingOwners for 6

8. NoTier2ToTier1Path

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

9. NoSelfEscalationToProtectedGroups

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

Download and install the Alloy Analyzer
Clone the ADTierModel-Rust repository

Basic Analysis

Open ADTierModel_ACL.als in the Alloy Analyzer
Select an assertion to check (e.g., NoTier2ToTier0Path)
Click “Execute” to run the analysis

Understanding Scope

The for N clause limits the search space:

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

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.

Extending the Model

Adding New Attack Patterns

To model a new attack technique:

Define any new permission types or properties
Create a predicate describing the attack conditions
Add the predicate to canCompromise
Create an assertion verifying tier isolation against the attack

Analyzing Your Environment

Export your AD configuration to Alloy format:

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

// 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
}

​Overview

​Data Model

​Principal Hierarchy

​Container Structure

​Tier Model

​Security Descriptors and ACLs

​ACL Structure

​Permission Rights

​Protected Groups

​Attack Path Detection

​Effective Trustee Resolution

​Core Compromise Predicate

​Attack Scenarios

​1. WriteDACL/WriteOwner Abuse

​2. Group Membership Manipulation

​3. Password Reset Attacks

​4. DCSync Exploitation

​5. Resource-Based Constrained Delegation (RBCD)

​6. SPN Manipulation (Kerberoasting Setup)

​7. Shadow Credentials

​8. Constrained Delegation Abuse

​9. Cross-Tier Compromise Chains

​Security Assertions

​1. NoTier2ToTier0Path

​2. NoTier1ToTier0Path

​3. TierIsolationMaintained

​4. DCSyncOnlyTier0

​5. ProtectedGroupsSecure

​6. NoRBCDEscalation

​7. NoDanglingOwners

​8. NoTier2ToTier1Path

​9. NoSelfEscalationToProtectedGroups

​Running the Model

​Prerequisites

​Basic Analysis

​Understanding Scope

​Interpreting Results

​Extending the Model

​Adding New Attack Patterns

​Analyzing Your Environment

Overview

Data Model

Principal Hierarchy

Container Structure

Tier Model

Security Descriptors and ACLs

ACL Structure

Permission Rights

Protected Groups

Attack Path Detection

Effective Trustee Resolution

Core Compromise Predicate

Attack Scenarios

1. WriteDACL/WriteOwner Abuse

2. Group Membership Manipulation

3. Password Reset Attacks

4. DCSync Exploitation

5. Resource-Based Constrained Delegation (RBCD)

6. SPN Manipulation (Kerberoasting Setup)

7. Shadow Credentials

8. Constrained Delegation Abuse

9. Cross-Tier Compromise Chains

Security Assertions

1. NoTier2ToTier0Path

2. NoTier1ToTier0Path

3. TierIsolationMaintained

4. DCSyncOnlyTier0

5. ProtectedGroupsSecure

6. NoRBCDEscalation

7. NoDanglingOwners

8. NoTier2ToTier1Path

9. NoSelfEscalationToProtectedGroups

Running the Model

Prerequisites

Basic Analysis

Understanding Scope

Interpreting Results

Extending the Model

Adding New Attack Patterns

Analyzing Your Environment