1 of 20

Automation and Anti-automation

CSE 598 – Applied Program Analysis and Debugging

Fall 2025

​

Fish Wang

Arizona State University

2 of 20

Emulators

  • If we can interpret Python statements, we can also interpret assembly instructions

​

  • Emulators emulate behaviors of each instruction in a simulated environment
    • For example, we can use a Python dict to model registers
    • We can use a Python dict to model memory spaces

​

2

3 of 20

Emulators

  • You have full control over what to execute and how to execute
    • You can pretty much control everything on a real CPU, but things can be more difficult at times…

​

3

4 of 20

Symbolic Execution

  • Emulator is like a CPU (but slower).
    • Everything must be concrete
    • mov rax, rbx�Your emulator must know the value of rbx before emulating this instruction

​

  • Symbolic execution allows you to use unknown variables during execution
    • Assuming rbx stores a 64-bit unknown variable x0
    • After symbolically executing, rax holds x0, too

4

5 of 20

Symbolic Execution (Cont.)

  • Many people use symbolic execution and a constraint solver to reason about input
    • mov rax, rbx�cmp rax, 5�je label
    • At label, we know x0 == rax == rbx == 5 after constraint solving

5

6 of 20

Symbolic Constraints

  • Every path predicate (or path condition) introduces a new constraint

6

mov rax, rbx

cmp rax, 5

je label

label:

!label:

rax == 5

rax != 5

7 of 20

States

  • State forking: When there are two branches, we will fork the parent state into two states
    • Each state has a different path condition

7

mov rax, rbx

cmp rax, 5

je label

label:

!label:

rax == 5

rax != 5

8 of 20

Constraint Solver

  • Once we know x0 == 5, we can ask a constraint solver to solve it and give us a model

8

mov rax, rbx

cmp rax, 5

je label

label:

!label:

rax == 5

rax != 5

{x0: 5}

{x0: 8}

Models

9 of 20

Basic blocks

  • States will not fork when there is only one exit going out of a instruction
    • Basic blocks: single-exit sequences of instructions

9

mov rax, rbx

cmp rax, 5

je label

label:

!label:

rax == 5

rax != 5

10 of 20

Basic blocks

  • States will not fork when there is only one exit going out of a instruction
    • Basic blocks: single-exit sequences of instructions

10

​

​

mov rax, rbx

cmp rax, 5

je label

​

​

label:

!label:

rax == 5

rax != 5

11 of 20

Say hi to angr

  • Let's use angr to solve csaw2012reversing.exe

11

12 of 20

Let's solve regme with angr

12

13 of 20

Software Registration Models

  • check(reg_key) == true

​

​

​

​

  • reg_key = f(username)

13

14 of 20

Software Registration Models

  • reg_key = f(hardware_key)

​

14

15 of 20

Software Registration Models

  • reg_file, is_signed(reg_file) == true

​

15

16 of 20

Software Registration Models

  • Key + activation

​

16

17 of 20

Securing Registration Models

  • How can we attack each model?
    • Bruteforcing
    • Cracking and patching
    • Dumping plain text reg_keys
    • Constraint solving
    • Replacing public keys

​

  • DO NOT REINVENT YOUR OWN CRYPTO

17

18 of 20

"angrables"

  • Using angr to find registration keys (or their equivalences)
    • Where to start symbolic execution?
    • How to provide input?
    • What is the success condition?
    • What to find and what to avoid?

18

19 of 20

Try it

19

20 of 20

Defeating Symbolic Execution

  • Anything non-linear is difficult for symbolic execution engines
    • Use strong crypto algorithms
    • Use strong hash algorithms
    • DO NOT REINVENT YOUR OWN CRYPTO
  • Path explosion is difficult to deal with
    • But not impossible to fix with some manual effort
    • Strong crypto is your best friend

20