Disclaimer: how I make slides

• I use an AI-integrated slide-making app here:

  • https://github.com/kmicinski/slides

• I initially dictate the slides at a high level, and then generate a markdown document

• I use an AI agent to make figures for the slides

• Writing on the slides and the general structure is developed by me

  • But I often use AI for copyediting on my slides

• Please let me know if you notice any mistakes, kkmicins@syr.edu

High-level picture: what's the goal?

• We want to find a safety violation: identify a bug in a program
• We can often see this in terms of reachability:
  • Is it possible to reach / drive the program execution to an exploited state starting from its normal path of execution?

For example...

if (len < 64 && magic == 0x41424344) {
  memcpy(buf, input, len + 16);
}

We might ask...

Is there any input that reaches this point while violating a memory safety condition?

Many ways to identify safety violations

• Computer science has explored many ways of finding (memory, etc.) safety violations
  • Testing
  • Fuzzing
  • Reachability-based program analysis / abstract interpretation / etc.
  • Symbolic execution
  • Program logics
• All of these rely upon different formal foundations.
  • For example, abstract interpretation uses properties of lattices and monotonic functions defined over these lattices.
  • Meanwhile, symbolic execution uses SAT/SMT

This lecture

• This class we'll talk about SMT and symbolic execution, along with cyber-reasoning systems that put LLMs in a loop with tools including SMT, SE, etc.

• Next class we'll take a look at program analysis and how it can be implemented.

• Later in the class we'll study how we can harmonize these things, adding program analysis as a tool to the cyber-reasoning pipeline...

Symbolic execution versus program analysis

SAT versus SMT

Propositional SAT asks whether a Boolean formula can be made true.

$$(x \lor y) \land (\neg x \lor z)$$

• Can use SAT to ask: "does a counterexample exist?". The variables are implicitly existentially quantified. So it's really, "does there $\exists x,y,z.$ s.t. the formula $(x \lor y) \land (\neg x \lor z)$ is true?"

By contrast, SMT asks whether a formula is satisfiable modulo a first-order theory:

$$0 \le n < 64 \land n + 16 > 72$$

Here, the symbols $\leq$, $<$, $+$, and $>$ appeal to a theory of arithmetic

• Can't be all of arithmetic, that would be impossible (Gödel's incompleteness theorems)

Background: de Moura and Bjørner, "Z3: An Efficient SMT Solver," TACAS 2008; Barrett et al., "The SMT-LIB Standard."

How is SMT solving useful in vulnerability discovery?

Security questions often mix control flow with low-level data facts:

• Can attacker input reach this branch?
• Can a length arithmetic operation wrap around?
• Can two pointers alias?
• Can a string satisfy a parser's checks?

SMT is useful because these are not just Boolean questions. They involve machine integers, memory, strings, and path reachability.

The challenge is how to phrase our attack-relevant statements in the language of SMT

Is "SMT" really AI?

• SAT solving is classic symbolic AI.
  • SMT solvers still incorporate aspects of SAT solving, e.g., DPLL(T), CDCL, clause learning, etc.
• SMT solvers are an extension of SAT to first-order theories
• What about modern LLMs? Do we really need SMT in the age of modern LLMs and tools?
  • As far as I know, this is an open question--one we will try to explore...

How SMT solving works, the 1000-foot view

• SMT tries to build an assignment by guessing at unconstrained variables and then forcing implications. For example, if we guess x = 5 and we have $x < 0 \to y = 5$, we must have $y=5$

  • This is called propagation; in this case theory propagation, since we are appealing to the theory of arithmetic

• A SAT engine explores the SAT fragment of the problem

• Theory-specific solvers reason about specific theories: numbers, memory, equality

• Learned explanations allow generalizing knowledge to learn from previous mistakes

Bjørner et al., Z3 Internals, §2.1.

A theory-specific conflict can yield a learned lemma

Barbosa et al., cvc5, §2.1.

The solver's wall-clock time depends on workload

• Changing the way we send formulas to SMT can radically change its performance!

Navigating the Universe of Z3 Theory Solvers; Fazekas et al., IPASIR-UP, SAT 2023.

From concrete execution to symbolic execution

input = "AAAA"
x = 0x41414141
branch: x == 0xdeadbeef  // false

input = α0 α1 α2 α3
x = concat(α0, α1, α2, α3)
branch condition: x == 0xdeadbeef

Now the question is not "what happened on this run?" It is: is there any input that makes the branch go the other way?

Classic system: Cadar, Dunbar, and Engler, "KLEE," OSDI 2008.

Path conditions

A path condition is the conjunction of branch decisions needed to reach a program point.

if (n < 64) {
  if (tag == 0x1337) {
    sink(buf[n + 8]);
  }
}

Path to sink:

$$\text{n} < 64 \land \text{tag} = 0x1337$$

Potential out-of-bounds query:

$$\text{n} < 64 \land \text{tag} = 0x1337 \land \text{n} + 8 \ge |\text{buf}|$$

Figure: building a path condition

Useful theories for reverse engineering...

SMT-LIB is a uniform standard for defining SMT queries via S-expressions and allows us to reuse a variety of solvers via a simple, uniform interface.

For vulnerability identification, the most important theories are usually:

• Bit-vectors: machine integers, overflow, shifts, masks
• Arrays: memory as select and store
• Linear arithmetic: sizes, bounds, counters
• Strings / regexes: web input, parsers, validation logic
• Uninterpreted functions: abstraction when exact behavior is unknown

Not every theory is equally important for every target. For example, strings / regex is much more useful for doing web exploitation, whereas bit-vectors are useful for binaries / C-style apps

Bit-vectors: machine arithmetic, not integers

• C integers are fixed-width.

• For example, in 8-bit unsigned arithmetic we have 250 + 10 = 4, because arithmetic is modulo $2^8$

A vulnerability query may depend on exactly this behavior:

uint8_t total = len + header;
if (total < 64) memcpy(buf, input, len);

• If len + header wraps, the check may validate the wrong quantity!

• Thus, a bit-vector theory has to track the size of each bit vector, and operations must properly account for things like overflow, etc.

How SMT solvers work, roughly

Modern SMT solving often looks like:

1. Boolean (SAT solver) search proposes an assignment
2. Theory solver checks whether it makes sense
3. If contradiction, theory solver explains the conflict and returns a "lemma"
4. Boolean search learns, backtracks, and tries again

Figure: DPLL(T) intuition

So the Boolean search learns: not all of $A, B, C$ can be true.

What is a cyber-reasoning system?

Term I made up; but I mean a frontier-LLM-orchestrated pipeline which does the following...

1. build and run a target
2. explore behavior
3. find suspicious states
4. prove or demonstrate a vulnerability
5. repair or mitigate it
6. validate the result

• My claim: cyber reasoning systems will become increasingly important for both defensive and offensive tasks

Figure: the CRS loop

Which parts should be neural, which symbolic, which concrete?

Why not just ask an LLM?

LLMs are useful for:

• code comprehension
• hypothesis generation
• recognizing protocols and formats
• explaining tool output
• proposing harnesses or patches

Main idea: Guess / generate hypotheses with LLM, then check with tools to provide ground truth

• Tests, symbolic execution, fuzzing (e.g., with seed generated by LLM)

Reading map

There are several different kinds of cyber-reasoning systems in the literature:

• Disclaimer: I have not read all of these papers myself, though I've skimmed them; we will cover these papers based on student interest this semester.

ChatAFL — LLM-guided protocol fuzzing

NDSS 2024, Meng et al., built on AFLNet. The LLM has already read the RFCs: ask it narrow questions, and let coverage judge every answer.

Source: Meng et al., "Large Language Model guided Protocol Fuzzing," NDSS 2024.

Tool-using agents — PentestGPT and Project Naptime

Both are the CRS loop (explore → observe → reason → act → validate); the hard part is keeping state across many tool calls. SWE-agent made the same point: the agent-computer interface decides what the agent can find.

Sources: Deng et al., PentestGPT, USENIX Security 2024; Project Naptime; SWE-agent, NeurIPS 2024.

In the wild: autonomous pentesting agents

Composite of public engineering write-ups from commercial autonomous pentesters (e.g. XBOW, RunSybil); no single vendor's internals are shown. Leaderboard claim: XBOW blog, 2025.

The DARPA AIxCC Competition

Final round, DEF CON 33, August 2025. Seven fully autonomous CRSs, no human in the loop, against 70 vulnerabilities injected into OSS-Fuzz-style C and Java projects (SQLite, libxml2, FreeRDP, Apache Tika, ZooKeeper, …).

1st Team Atlanta (4M USD) • 2nd Trail of Bits (3M USD) • 3rd Theori (1.5M USD). Source: DARPA AIxCC final results, Aug 2025. All seven CRSs were open-sourced after the final.

Inside an AIxCC-style CRS: who does what

The recurring architecture

Every system here runs one loop: semantic hint → executable experiment → feedback

Viewing a single bug through from POV of many tools...

char buf[64];
if (len < 64 && magic == 0x41424344) {
  memcpy(buf, input, len + 16);
}

So, does SMT still matter?

Yes, as a component, not the driver. Each engine is trusted for something different:

• Fuzzing: cheap and never wrong, but blind.
• Symbolic execution + SMT: exact, and can say "no such input exists," but can't prove
• LLM: great at guessing, use in a loop with conventional tools

To me, the big question is: how does LLM+X change the game versus traditional tools?

We'll explore this question as the answer evolves over the course of the semester! :-)