close
프로필 배경
프로필 로고

그러니까 PWN

etc · 2025. 6. 27. fullscreen 넓게보기

[SMT-Solver] Handling z3

이거 제가 공부하고 싶어서 적는 글입니다. 별로 도움은 되지 못 할 거에요.

Data Type

Python z3 비고
bool BoolRef 파이썬은 T/F, z3에서는 논리 조건식을 나타내는 심볼릭 객체(AST Node)
int IntRef z3는 오버플로우 없이 무한 수학적 정수
- BitVecRef z3은 특정 비트 크기를 가진 고정폭 정수를 제공, 비트 연산과 오버플로우 자동처리
float RealRef, FPRef z3는 유리수로 처리, FPREF는 IEEE-754 표준
str SeqRef 파이썬은 문자열 변경 가능, z3의 문자열은 불편, 연산을 통해 새로운 식 생성해야함
list, dict ArrayRef z3는 불편, 수학적 Map 형태로 사용된다. Store 연산으로 변경 시 새 배열 생성
사용자 정의 클래스 DatatypeRef 구조체나 열거형처럼 사용자 자료형 선언

 

내가 간과한 사항

성능 문제

z3는 논리식을 다룰 때 내부적으로 AST구조를 사용한다.

식이 지나치게 복잡하거나 중복이 많으면 성능이 급격히 떨어질 수 있다.

 

# 성능 저하 예시
x = Int('x')
s = Solver()
s.add(x + x + x + x + x + x + x + x + x + x == 10)

# 성능 개선 예시
s.add(10 * x == 10)

 

주기적으로 simplify() 사용하면 효율성 증가

expr = x + x + 2 - 2
simplified_expr = simplify(expr)  # 결과: 2 * x

 

식의 재사용

같은 식을 반본적으로 정의하면 성능 저하 -> 자주 쓰는 표현은 변수로 정의

# 비효율적
s.add(And(x > 0, y > 0))
s.add(And(x > 0, y < 5))
s.add(And(x > 0, y != 2))

# 효율적
common_cond = x > 0
s.add(And(common_cond, y > 0))
s.add(And(common_cond, y < 5))
s.add(And(common_cond, y != 2))

 

 

부동소수점(FPRef) 오차

z3의 FPRef는 정밀하지만, IEEE-754를 준수하기에 mantissa 오차 발생 가능

 

fp1 = FP('fp1', Float32())
s = Solver()
s.add(fp1 == FPVal(0.1, Float32()))  # 0.1은 정확히 표현되지 않음 -> [fp1 = 1.60000002384185791015625*(2**-4)]

# 정확한 비교를 위한 방법
rm = RNE()  # Round Nearest Even
s.add(fpEQ(fp1, FPVal(0.1, Float32(), rm)))

print(s.check())
print(s.model())

 

 

무한의 해 (응용에서 리뷰할 것)

도메인이 중요하다..

Example

Bool

from z3 import *

p = BoolVal(True)
q = Bool('q')
s = Solver()
s.add(And(p, q))
print(s.check())
print(s.model())	# [q = True]

 

참인 값과 심볼릭 Bool 변수를 AND 조건으로 묶고 해를 구하는 간단한 예제

 

정수

x = Int('x')
y = Int('y')
s = Solver()
s.add(x + y == 10, x > 2, y < 5)
print(s.check())
print(s.model())	# [y = 0, x = 10]

두 정수 변수의 합과 개별 조건을 만족하는 값을 찾는 예시

 

BitVec (오버플로우 확인)

bv = BitVec('bv', 8)
s = Solver()
s.add(bv + 1 == 0)
print(s.check())
print(s.model()) 	# [bv = 255]: 8비트 정수로 255에서 1을 더하면 0이 되는 오버플로우 상황

BitVec 자료형의 특성을 보여주는 예

비트 연산 시 오버플로우가 어떻게 처리되는지 이해하는데 유용

 

문자열

s1 = String('s1')
s2 = String('s2')
s = Solver()
s.add(Concat(s1, s2) == "hello world", Length(s1) == 5)
print(s.check())
print(s.model())	# [s1 = "hello", s2 = " world"]

두 문자열 변수를 연결하여 특정 문자열과 길이 조건을 만족하는 값을 찾는다.

z3에서는 문자열 변경이 불가능하다는걸 기억하자.

 

배열

arr = Array('arr', IntSort(), IntSort())
s = Solver()
s.add(Select(arr, 0) == 10)
updated_arr = Store(arr, 0, 20)
s.add(Select(updated_arr, 0) == 20)
print(s.check())
print(s.model())	# [arr = K(Int, 10)]

z3 배열은 불변이다. 불변이다. 불변이다.

값 변경할 때마다 Store로 새로운 배열 생성, 특정 위치 값 확인시 Select

 

사용자 정의 자료형

List = Datatype('List')
List.declare('nil')
List.declare('cons', ('head', IntSort()), ('tail', List))
List = List.create()

lst = List.cons(1, List.cons(2, List.nil))
s = Solver()
s.add(List.head(lst) == 1)
print(s.check())  # sat
print(s.model())

사용자 정의 자료형으로 연결리스트를 정의했다.

 

응용 -> 모델 열거하기

z3는 기본적으로 하나의 해만 찾는다. 여러 개의 가능한 해를 모두 찾고 싶다면 도메인을 닫을 줄 알아야 한다.

 

예시로, 다음 예제를 보자

s.add(x + y == 10, x > 2, y < 5)

다음 예제를 만족하는 x와 y 세트 값은 무한하다.

$ (x, y) = (6, 4) | ... | (x, y) = (10, 0) | ... |(x, y) = (20, -10) | ... | (x, y) = (1000, -990) | ... $

 

만족하는 모든 해를 찾는 코드를 돌리면 컴퓨터는 지구가 멸망할 때까지 돈다. 즉, 도메인을 설계하거나 필요한 만큼 찾아야한다.

 

1. BitVec 도메인 유한화

from z3 import *

# 8-bit: 0~255(부호 없는 산술),  -128~127(부호 있는 비교)
x, y = BitVecs('x y', 8)

s = Solver()
s.add(x + y == 10,   # mod 256 합
      x > 2,         # > 는 2의 보수 signed 비교
      y < 5)

solutions = []
while s.check() == sat:
    m = s.model()
    solutions.append({'x': m[x].as_long(), 'y': m[y].as_long()})
    s.add(Or(x != m[x], y != m[y]))

print(len(solutions), solutions)

 

더보기 
andsopwn@lxc:~/-$ python3 -u "/home/andsopwn/-/z3e.py"
sol 122개: [{'x': 103, 'y': 163}, {'x': 6, 'y': 4}, {'x': 10, 'y': 0}, {'x': 8, 'y': 2}, {'x': 72, 'y': 194}, {'x': 68, 'y': 198}, {'x': 100, 'y': 166}, {'x': 104, 'y': 162}, {'x': 7, 'y': 3}, {'x': 71, 'y': 195}, {'x': 73, 'y': 193}, {'x': 74, 'y': 192}, {'x': 66, 'y': 200}, {'x': 64, 'y': 202}, {'x': 48, 'y': 218}, {'x': 16, 'y': 250}, {'x': 12, 'y': 254}, {'x': 28, 'y': 238}, {'x': 30, 'y': 236}, {'x': 34, 'y': 232}, {'x': 18, 'y': 248}, {'x': 14, 'y': 252}, {'x': 94, 'y': 172}, {'x': 98, 'y': 168}, {'x': 96, 'y': 170}, {'x': 92, 'y': 174}, {'x': 78, 'y': 188}, {'x': 82, 'y': 184}, {'x': 80, 'y': 186}, {'x': 76, 'y': 190}, {'x': 102, 'y': 164}, {'x': 106, 'y': 160}, {'x': 90, 'y': 176}, {'x': 86, 'y': 180}, {'x': 38, 'y': 228}, {'x': 42, 'y': 224}, {'x': 26, 'y': 240}, {'x': 22, 'y': 244}, {'x': 36, 'y': 230}, {'x': 40, 'y': 226}, {'x': 24, 'y': 242}, {'x': 23, 'y': 243}, {'x': 87, 'y': 179}, {'x': 119, 'y': 147}, {'x': 121, 'y': 145}, {'x': 117, 'y': 149}, {'x': 125, 'y': 141}, {'x': 123, 'y': 143}, {'x': 99, 'y': 167}, {'x': 84, 'y': 182}, {'x': 116, 'y': 150}, {'x': 108, 'y': 158}, {'x': 44, 'y': 222}, {'x': 60, 'y': 206}, {'x': 124, 'y': 142}, {'x': 115, 'y': 151}, {'x': 83, 'y': 183}, {'x': 19, 'y': 247}, {'x': 35, 'y': 231}, {'x': 91, 'y': 175}, {'x': 75, 'y': 191}, {'x': 11, 'y': 255}, {'x': 27, 'y': 239}, {'x': 101, 'y': 165}, {'x': 85, 'y': 181}, {'x': 21, 'y': 245}, {'x': 37, 'y': 229}, {'x': 93, 'y': 173}, {'x': 77, 'y': 189}, {'x': 13, 'y': 253}, {'x': 29, 'y': 237}, {'x': 32, 'y': 234}, {'x': 63, 'y': 203}, {'x': 127, 'y': 139}, {'x': 95, 'y': 171}, {'x': 39, 'y': 227}, {'x': 67, 'y': 199}, {'x': 59, 'y': 207}, {'x': 31, 'y': 235}, {'x': 105, 'y': 161}, {'x': 9, 'y': 1}, {'x': 65, 'y': 201}, {'x': 33, 'y': 233}, {'x': 97, 'y': 169}, {'x': 113, 'y': 153}, {'x': 49, 'y': 217}, {'x': 45, 'y': 221}, {'x': 109, 'y': 157}, {'x': 81, 'y': 185}, {'x': 17, 'y': 249}, {'x': 61, 'y': 205}, {'x': 69, 'y': 197}, {'x': 41, 'y': 225}, {'x': 89, 'y': 177}, {'x': 111, 'y': 155}, {'x': 47, 'y': 219}, {'x': 43, 'y': 223}, {'x': 107, 'y': 159}, {'x': 79, 'y': 187}, {'x': 15, 'y': 251}, {'x': 55, 'y': 211}, {'x': 120, 'y': 146}, {'x': 112, 'y': 154}, {'x': 114, 'y': 152}, {'x': 126, 'y': 140}, {'x': 70, 'y': 196}, {'x': 122, 'y': 144}, {'x': 118, 'y': 148}, {'x': 110, 'y': 156}, {'x': 88, 'y': 178}, {'x': 58, 'y': 208}, {'x': 56, 'y': 210}, {'x': 57, 'y': 209}, {'x': 25, 'y': 241}, {'x': 50, 'y': 216}, {'x': 62, 'y': 204}, {'x': 46, 'y': 220}, {'x': 54, 'y': 212}, {'x': 53, 'y': 213}, {'x': 51, 'y': 215}, {'x': 52, 'y': 214}, {'x': 20, 'y': 246}]

이 경우 도메인 크기는 8-bit로 자동 제한

+는 항상 $mod 256$. >, < 등 부호 있는 비교; 부호 없는 UGT, ULT 사용

 

2. 카운터로 해 개수만 제한

from z3 import *

x, y = Ints('x y')

s = Solver()
s.add(x + y == 10,
      x > 2,
      y < 5)

solutions = []
MAX = 100

while len(solutions) < MAX and s.check() == sat:
    m = s.model()
    solutions.append({'x': m[x], 'y': m[y]})
    s.add(Or(x != m[x], y != m[y]))

print(f"sol {len(solutions)}개:", solutions)
더보기 
andsopwn@lxc:~/-$ python3 -u "/home/andsopwn/-/z3p.py"
sol 100개: [{'x': 10, 'y': 0}, {'x': 11, 'y': -1}, {'x': 12, 'y': -2}, {'x': 13, 'y': -3}, {'x': 14, 'y': -4}, {'x': 15, 'y': -5}, {'x': 16, 'y': -6}, {'x': 17, 'y': -7}, {'x': 18, 'y': -8}, {'x': 19, 'y': -9}, {'x': 20, 'y': -10}, {'x': 21, 'y': -11}, {'x': 22, 'y': -12}, {'x': 23, 'y': -13}, {'x': 24, 'y': -14}, {'x': 25, 'y': -15}, {'x': 26, 'y': -16}, {'x': 27, 'y': -17}, {'x': 28, 'y': -18}, {'x': 29, 'y': -19}, {'x': 30, 'y': -20}, {'x': 31, 'y': -21}, {'x': 32, 'y': -22}, {'x': 33, 'y': -23}, {'x': 34, 'y': -24}, {'x': 35, 'y': -25}, {'x': 36, 'y': -26}, {'x': 37, 'y': -27}, {'x': 38, 'y': -28}, {'x': 39, 'y': -29}, {'x': 40, 'y': -30}, {'x': 41, 'y': -31}, {'x': 42, 'y': -32}, {'x': 43, 'y': -33}, {'x': 44, 'y': -34}, {'x': 45, 'y': -35}, {'x': 46, 'y': -36}, {'x': 47, 'y': -37}, {'x': 48, 'y': -38}, {'x': 49, 'y': -39}, {'x': 50, 'y': -40}, {'x': 51, 'y': -41}, {'x': 52, 'y': -42}, {'x': 53, 'y': -43}, {'x': 54, 'y': -44}, {'x': 55, 'y': -45}, {'x': 56, 'y': -46}, {'x': 57, 'y': -47}, {'x': 58, 'y': -48}, {'x': 59, 'y': -49}, {'x': 60, 'y': -50}, {'x': 61, 'y': -51}, {'x': 62, 'y': -52}, {'x': 63, 'y': -53}, {'x': 64, 'y': -54}, {'x': 65, 'y': -55}, {'x': 66, 'y': -56}, {'x': 67, 'y': -57}, {'x': 68, 'y': -58}, {'x': 69, 'y': -59}, {'x': 70, 'y': -60}, {'x': 71, 'y': -61}, {'x': 72, 'y': -62}, {'x': 73, 'y': -63}, {'x': 74, 'y': -64}, {'x': 75, 'y': -65}, {'x': 76, 'y': -66}, {'x': 77, 'y': -67}, {'x': 78, 'y': -68}, {'x': 79, 'y': -69}, {'x': 80, 'y': -70}, {'x': 81, 'y': -71}, {'x': 82, 'y': -72}, {'x': 83, 'y': -73}, {'x': 84, 'y': -74}, {'x': 85, 'y': -75}, {'x': 86, 'y': -76}, {'x': 87, 'y': -77}, {'x': 88, 'y': -78}, {'x': 89, 'y': -79}, {'x': 90, 'y': -80}, {'x': 91, 'y': -81}, {'x': 92, 'y': -82}, {'x': 93, 'y': -83}, {'x': 94, 'y': -84}, {'x': 95, 'y': -85}, {'x': 96, 'y': -86}, {'x': 97, 'y': -87}, {'x': 98, 'y': -88}, {'x': 99, 'y': -89}, {'x': 100, 'y': -90}, {'x': 101, 'y': -91}, {'x': 102, 'y': -92}, {'x': 103, 'y': -93}, {'x': 104, 'y': -94}, {'x': 105, 'y': -95}, {'x': 106, 'y': -96}, {'x': 107, 'y': -97}, {'x': 108, 'y': -98}, {'x': 109, 'y': -99}]

len(solutions) < max 로 루프 제어.

대량 탐색시 s.push(), s.pop() 대신 재사용이 가장 간단

 

 

 

내가 보려고 만든 맛있는 Reference

[z3 예제]

https://ericpony.github.io/z3py-tutorial/guide-examples.htm

 

[z3Prover]

https://z3prover.github.io/papers/programmingz3.html

 

[z3 언어별 API]

https://github.com/Z3Prover/doc

 

[마소 가이드]

https://microsoft.github.io/z3guide/docs/theories/Bitvectors/

 

 

기타 REF

https://www.cs.colostate.edu/~cs440/spring19/slides/z3-tutorial.pdf

https://www.iitp.ac.in/~arijit/web/courses/2025/CS5201/Z3_Solver_Updated.pdf

https://opencourse.inf.ed.ac.uk/sites/default/files/https/opencourse.inf.ed.ac.uk/fv/2023/ex2.pdf

 

 

'etc' 카테고리의 다른 글

[9P] UTM : Directory Share Mode on Linux(VM, Emulator)  (1) 2025.02.06
[회고록] 24년 상반기  (0) 2024.06.12
Dreamhack 커리큘럼 순서 정리  (0) 2024.06.01
etc 관련 글
더 보기

티스토리툴바