2021 SCIST Security Reverse Note

python3 -i [file]跑完進入到 REPL mode

Flags

• CF(Carry Flag) : Set if an aritmnetic carry or borrow has indicated,reset otherwise
• ZF (Zero Flag) : Set if an arithmetic result is 0, reset otherwise
• SF (Sign Flag) : Set if the result is negative (MSB = 1)
• OF(Overflow Flag) : Set if an arithmetic overflow has occurred, reset otherwise

  Practice

  Expression	CF	ZF	SF	OF
  1. 1010 - 1010	0	1	0	0
  2. 0000 - 0001	1	0	1	0
  3. 1110 + 1110	1	0	1	1

objdump

$ objdump -M intel -d <binary>

compile

$ vim hello.c
$ gcc hello.c (filename `a.out` by default)
$ file hello.c
$ ./a.out

common commands

strings
strace
grep

IDA Pro

F5 -> pseudocode
shift + F12 -> Strings window

Z3

Variable type

Int : ℤ
Real : ℝ
Bool : boolean
BitVec : Bit Vector, provide variable-length integer

Bool(‘t’) define t as a boolean variable
BitVec(‘x’,32) define x as a 32bit data

Variable

x = Int('x')
y = [Int(f'x_{i}') for i in range (30)]

Result

• SAT - results are in s.model()
• UNSAT - use reason_unknown() to get the reason

Basic

from z3 import *

# Create Variables
x = Int('x')
y = Int('y')

s = Solver() # Initialize solver

# Add constraints
s.add(x + y > 5)
s.add(y < 3)
s.add(x > 3)

# Check if is SAT
if s.check() == sat:
    print(s.model())
else:
    print('unsat')

Multiple Solutions

e.g.
an array(len==20)

while s.check() == sat:
    m = s.model()
    print(''.join(str(m[x[i]]) for i in range(20)))
    con = [x[i] != m[x[i]] for i in range(20)]
    s.add(Or(con))
else:
    print('unsat')

Angr - A binary analysis framework

usage

from angr import *

p = Porject('./a.out', auto_load_libs = False) # load binary

st = p.factory.entry_state() # create state

sm = p.factory.simgr()

# run
sm.step()
sm.run()
sm.explore(find=0xface, avoid=0xdead)
sm.explore(find=(0xface, 0xcafe, ), avoid=(0xdead, 0xbeef, ))
sm.explore(find=lambda s: ..., avoid=lambda s: ...)

Common Procedure

1. Load binary
2. Create state
3. Add symbolic variables
4. Constrain the state with symbolic variables
5. Create simulation manager
6. Tell simulation manager where to explore
7. Run
8. Get our constrained variables’ value

Claripy

BVS Bitvector Symbolic Variable
BVV Bitvector value
x = BVS('x',32) declare x as a 32-bit BitVector
y = BVV(0xdeadbeef,32) declare y as a 32-bit value將 y 宣告為 32-bit 的 0xdeadbeef 常數

from claripy import *

s = Solver()

x = BVS('x', 32)
y = BVS('y', 32)

s.add(x == 1)
s.add(y == 2)

print(s.eval(x, 1))
print(s.eval(y, 1))

Add comstraints

#common setup
for x in variables:
    st.add_constraints(x >= 0x20)
    st.add_constraints(x < 0x7f)

# every character is a number
for x in variables:
    st.add_constraints(x >= 48, x <= 57)

flag_chars = [BVS(f'x_{i}' , 8) for i in range(10)]
flag = Concat(*flag_chars + [BVV(b'\n')])

st = p.factory.entry.state(args=[bin, flag]) # pass by argv
st = p.factory.entry_state(stdin=flag) # pass by stdin