angr - (2) Claripy

Claripy ASTs

Claripy는 angr의 solver engine이다.

Claripy ASTs는 Concrete하거나 Symbolic한 표현과 상호작용하는 방법을 알려준다.

• Concrete : 구체적인 값이 있는 것

• Symbolic : 구체적인 값이 없고 미지수가 사용되는 것

Claripy AST는 Claripy가 지원하는 수학적 구성 간의 차이를 추상화하여 트리처럼 나타낸다. 자세한 건 딱히 알 필요 없을 거 같다. Claripy는 요청을 백엔드로 전송하여 기본 객체 자체에 대한 이러한 작업의 적용을 처리한다.

Claripy는 다음과 같은 ASTs를 사용하고 있다.

1. BV

Bit-Vector로, symbolic(with a name) 또는 concrete(with a value)하게 설정할 수 있다. bit size를 설정해준다.

Backend Concrete, BackendVSA, BackendZ3 에서 이를 지원한다.

# Create a 32-bit symbolic bitvector "x"
>>> claripy.BVS('x', 32)
<BV32 x_1_32>

# Create a 32-bit concrete bitvector with the value 0xdeadbeef
>>> claripy.BVV(0xdeadbeef, 32)
<BV32 0xdeadbeef>

예시에서 보다시피 BV는 쓰지 않는다. BV를 쓰면,

>>> claripy.BV(size=32, name='x')
DEPRECATION WARNING: claripy.BV is deprecated and will soon be removed. Please use claripy.BVS, instead.
<BV32 x_2_32>

곧 지워질거라고 한다. ㅠㅡㅠ BVV, BVS를 대신 쓰자. 유용한 기능들만 정리해보자.

chop(bits=1)

>>> x = claripy.BVS('x', 32)

# Chop a BV into consecutive sub-slices.
# Return a list of bitvectors. The first one will be the most significant bits.
>>> x.chop(8)
[<BV8 x_3_32[31:24]>, <BV8 x_3_32[23:16]>, <BV8 x_3_32[15:8]>, <BV8 x_3_32[7:0]>]

# Obviously, the length of this BV must be a multiple of bits
>>> x.chop(7)
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/l0z1k/.virtualenvs/angr/lib/python3.8/site-packages/claripy/ast/bv.py", line 58, in chop
    raise ValueError("expression length (%d) should be a multiple of 'bits' (%d)" % (len(self), bits))
ValueError: expression length (32) should be a multiple of 'bits' (7)

get_byte(index)

# Extract a byte from a BV, where the index refers to the in a big-endian order.
# Return a 8-bit BV
>>> x.get_byte(0)
<BV8 x_3_32[31:24]>
>>> x.get_byte(2)
<BV8 x_3_32[15:8]>

get_bytes(index, size)

# Extracts several bytes from a bitvector. Big-endian
>>> x.get_bytes(0, 3)
<BV24 x_3_32[31:8]>

1.1. BVS

bit-vector 변수를 만들어준다.

parameters

• name - 변수 이름
• size - bit-vector의 size(bit 단위)
• min - 변수가 가질 수 있는 최솟값
• max - 변수가 가질 수 있는 최댓값
• stride - 증가폭? 예를 들어, 10으로 설정하면 변수는 10, 20, 30, .. 이런식으로 가진다.

1.2. BVV

concrete한 bit-vector value를 만들어준다.

parameters

• value - bit-vector의 값

• size - bit-vector의 size. 만약 문자열로 들어오면 알아서 정수로 변환하여 처리한다.

2. FP

IEEE754 floating point number를 표현할 때 사용한다.

BackendConcrete , BackendZ3 에서 이를 지원한다.

variables

• length - 이 값의 길이
• sort - 이 값의 type? 보통 FSORT_FLOAT , FSORT_DOUBLE 을 사용한다.

# Create a symbolic floating point 'b'
>>> claripy.FPS('x', claripy.fp.FSORT_FLOAT)
<FP32 FPS(FP_x_6_32, FLOAT)>

# Create a floating point with value 3.2
>>> claripy.FPV(3.2, claripy.fp.FSORT_DOUBLE)
<FP64 FPV(3.2, DOUBLE)>

2.1. FPS

Create a floating-proin symbol

parameters

• name - symbol 이름
• sort - 아까 말한거
• explicit_name - If False, an identifier is appended to the name to ensure uniqueness.

2.2. FPV

Create a concrete floating-point value.

parameters

• value
• sort

3. Bool

Boolean 연산을 할 수 있게 해준다.

BackendConcrete , BackendVSA , BackendZ3 에서 이를 지원한다.

>>> x = claripy.BVS('x', 32)
>>> y = claripy.BVS('y', 32)

# comparing two ASTs
>>> cmp = x == y
>>> cmp
<Bool x_7_32 == y_8_32>

Solver

Claripy Solver를 이용하여 간단한 연산을 해보자.

# create the solver and an expression
>>> s = claripy.Solver()
>>> x = claripy.BVS('x', 8)

# Add a constraint on x. x is less than unsigned 5.
>>> s.add(claripy.ULT(x, 5))

eval

This function returns up to n possible solutinos for expression expr.

parameters

• expr - expression to evaluate
• n - number of results to return

# 이전에 x가 5보다 작아야한다는 조건을 만족시키는 x 값을 출력하는 것이다.
>>> s.eval(x, 1)
(4,)
>>> s.eval(x, 5)
(2, 4, 1, 0, 3)

# 가능한 x값 중 최대, 최소값 출력
>>> s.max(x)
4
>>> s.min(x)
0

>>> y = claripy.BVV(65, 8)

# 만약 x가 1이라면, x 값을 가지고 그렇지 않다면 y 값을 가진다.
>>> z = claripy.If(x==1, x, y)

# x가 1일 수도 아닐 수도 있기 때문에, 두 값을 모두 가지게 된다.
>>> s.eval(z, 10)
(1, 65)

---