← Back to blog

Latent Logic: Deriving Attack Paths from Documentation

Windows security is fully documented. So are detection rules. That's a solvable constraint system.

Microsoft documents how Windows works. Thousands of pages. Every privilege, every API, every security boundary. Defenders document how they detect attacks. MITRE ATT&CK. Sigma rules. Vendor blogs.

That's a complete specification. Preconditions and effects. Detection triggers. The rules of the game.

Given the rules, what else becomes possible?

I built a tool that treats this as a constraint satisfaction problem. Feed it your current state. It uses Z3 to derive paths to SYSTEM that weren't explicitly programmed.

The logic was always there, latent in the design.


The Problem

Windows privilege escalation follows patterns. You have certain privileges. Certain handles. A certain integrity level. From that state, some operations are possible. Each operation changes the state. Eventually you reach SYSTEM.

Traditional tools enumerate what you have and match against known techniques. "You have SeImpersonatePrivilege, try Potato." Pattern matching. If/else chains. Hardcoded playbooks.

But the underlying logic is more general. Every Windows API has preconditions (what you need) and effects (what changes). Every detection rule has triggers. That's a formal system. And formal systems can be solved.

State = { privileges, handles, integrity, user }
Operations = { OpenProcess, DuplicateToken, CreateService, ... }
Goal = { integrity == SYSTEM }

Each operation:
  - Preconditions: what state must be true
  - Effects: what state changes
  - Cost: detection likelihood

Query: Find minimum-cost path from State to Goal

This is bounded model checking. Encode the state space. Encode the transitions. Ask the solver for a satisfying assignment. Not symbolic execution of binaries. Symbolic reasoning over documented security semantics.


How It Works

The tool has three components:

Ingestor. Enumerates the live system. What privileges do you have? What services can you modify? What paths are writable? What's in the registry? This populates the initial state.

Knowledge Base. 54 operations with preconditions, effects, and MITRE tags. Token manipulation, service abuse, potato variants, DLL hijacking, registry persistence, scheduled tasks. Each operation knows what it requires and what it produces.

Z3 Solver. State encoded as bitvectors. Privileges as bit flags. Handles as bit flags. Integrity as an enum. The solver searches for operation sequences that transition from initial state to goal state while minimizing detection cost.

# Simplified encoding
privileges = BitVec('privs', 32)
handles = BitVec('handles', 32)
integrity = Int('integrity')

# Operation: OpenProcess
# Requires: SeDebugPrivilege
# Produces: process_handle
op_openprocess = And(
    privileges & SEDEBUG != 0,  # precondition
    handles_next == handles | PROCESS_HANDLE  # effect
)

# Goal: reach SYSTEM integrity
goal = integrity == SYSTEM

# Query: find path
solver.add(initial_state)
solver.add(transition_constraints)
solver.add(goal)
solver.check()

Z3 returns a sequence of operations. Each step is valid given the previous state. The final state satisfies the goal. The solver found a path that I didn't explicitly program. Detection cost is a relative ordinal derived from common EDR heuristics: process creation, service modification, token abuse, and so on.


What It Finds

I ran it on my own machine. Non-admin shell. Just SeChangeNotifyPrivilege. Nothing interesting.

============================================================
LATENT LOGIC
============================================================
[USER CONTEXT]
  Username:    PCNAME\user
  Integrity:   MEDIUM
  Admin:       False
  Privileges:  SeChangeNotifyPrivilege

[*] Found 26 writable PATH directories
[*] Discovered access capabilities:
    • file_write_path
    • reg_write_run

[+] ESCALATION PATH FOUND (cost: 4)
    1. CreateFile [cost: 1]
    2. DLL_Hijack_Path [cost: 3]

Z3 derived a DLL hijack chain. I can write to directories in my PATH. If a privileged process searches those paths for a missing DLL, I win.


Running Elevated

Same machine, admin shell:

[USER CONTEXT]
  Username:    PCNAME\user
  Integrity:   HIGH
  Admin:       True
  Privileges:  SeChangeNotifyPrivilege, SeImpersonatePrivilege, 
               SeDebugPrivilege, SeBackupPrivilege, ...

[+] BEST PATH (confidence: 85%, risk: 2/5)
  1. uac_fodhelper
  2. potato_godpotato
  MITRE: T1548.002, T1134.001

[*] ALL PATHS: 120 total
    (1 direct, 99 two-step, 20 prereq chains)

120 paths to SYSTEM. Ranked by detection risk. MITRE-tagged. The solver explored the state space and found every valid composition.

Not pattern matching. The solver doesn't know "fodhelper + potato" as a named technique. It knows fodhelper produces SeImpersonatePrivilege at HIGH integrity. It knows potato requires SeImpersonatePrivilege. It composed them.


The Service Abuse Demo

To prove the paths are real, I executed one.

The solver found I had SERVICE_CHANGE_CONFIG on the Appinfo service. It derived: modify the service binary path, start the service, code executes as SYSTEM.

[+] ESCALATION PATH FOUND (cost: 2)
    1. StartServiceW [cost: 2]
[*] Attack Pattern: SERVICE_ABUSE

PS> python latent_logic.py live --execute

[+] Modifying Appinfo service...
[+] Starting service...
[+] SUCCESS! Payload executed as SYSTEM
[+] Created user: latentlogic (Administrators group)

The tool derived the path. Generated the payload. Executed it. Created an admin account via SYSTEM.

I didn't write "if service modifiable, do X." The solver found that path from the constraint model.


Why This Matters

The defensive industry publishes everything needed to attack them.

MSDN documents every API. Windows Internals explains the security model. MITRE catalogs techniques. Sigma rules specify detection logic. It's all public. It's meant to help defenders. But it's also a complete specification of the attack surface.

Traditional tools hard-code known techniques. Researcher finds path, writes check, ships update. Reactive. Always behind.

Constraint solving inverts this. Model the rules. Let the solver find paths. Paths that exist in the specification but haven't been documented as techniques yet. Paths that are mathematically valid but semantically obscure.

The knowledge base scales the solver. Adding a new operation isn't writing new code. It's adding a dict entry with preconditions and effects. Z3 automatically incorporates it into path finding.


Limitations

The model is only as complete as the knowledge base. Missing operations mean missing paths. The current implementation has ~54 operations. Windows has thousands of APIs. There's room to grow.

Some paths require external triggers. Potato attacks need a SYSTEM process to connect to your named pipe. The solver finds the path but can't force the trigger. That's marked in the output.

Detection costs are estimates. The solver optimizes for "quietest" path, but real detection depends on the target environment's specific tooling. A path rated 2/5 risk might be noisy in one environment and silent in another.

This is a reasoning tool, not a magic button. It finds what's possible. Execution still requires tradecraft.


The Broader Pattern

Latent Logic applies the same thinking as the rest of this research program:

Each one questions an assumption. Format recognition assumes structure. Code detection assumes presence. Technique discovery assumes human insight.

The assumptions are load-bearing. Remove them and the security model shifts.


The Rules Define the Game

Windows security isn't arbitrary. It follows rules. Documented rules. Every privilege has defined capabilities. Every API has defined behavior. Every detection has defined triggers.

That documentation is meant to help defenders understand the system. But understanding flows both ways. If the rules are public, they can be reasoned about. If they can be reasoned about, a solver can find compositions that weren't intended.

The paths exist whether or not anyone's written them down. They're latent in the specification. Z3 just makes them explicit.

They published the rules. I asked the solver what else becomes possible.

Chris Aziz, Bombadil Systems

Latent Logic is part of ongoing research. For questions or collaboration: [email protected]