Z3 사용법

Z3

Z3는 마이크로소프트에서 개발한 수식 해석 도구로, 대표적인 SMT(Satisfiability Modulo Theories)¹ 솔버이다. Z3는 보통 CTF에서 로직 자체는 파악을 다 했으나 역연산이 어려울 때 많이 사용된다.

Install

Python에서 Z3의 모듈의 설치 방법은 다음과 같다.

pip install z3-solver

위 명령어로 손쉽게 설치할 수 있다.

Basic Usage Guide for the Z3 Python API

import

from z3 import *

python에서 z3을 사용하고 싶다면 해당 모듈을 불러오면 된다.

Variable Declaration

변수 선언은 다음과 같이 할 수 있다.

# Int
x = Int("x")
y = Int("y")

# Real
a = Real("a")
b = Real("b")

# Bool
p = Bool("p")
q = Bool("q")

# BitVec
x_bitvec = BitVec("x", 32)
y_bitvec = BitVec("y", 32)

# Array(Array_name, Index_Type, Value_Type)
arr = Array("arr", IntSort(), IntSort())

비트 벡터 선언은 BitVec("Val", N)으로 N비트 Val값을 선언할 수 있다. 또한, 실수형을 선언할 때 자리수를 N자리 까지만 출력하고 싶으면 set_option(precision=N)을 사용할 수 있다.

Solver Class

z3에서 Solver라는 객체를 생성할 수 있는데, Solver 객체로 여러개의 수식을 작성할 수 있다.

s = Solver()

add()

s.add(조건)

s.add()로 수식을 추가할 수 있다.

check()

s.check()

s.check()는 내가 작성한 조건을 만족하는 해가 있으면 sat를 반환하고, 없다면 unsat를 반환한다.

model()

s.model()

s.model()은 값이 존재할 경우 값을 반환하는 함수이다. 만약 unsat이거나 unknown이면 에러를 반환한다.

s.reason_unknown()을 통해서 unknown인 이유를 알려준다.

reset()

s.reset()

내가 작성한 수식들을 초기화 하고 싶다면 s.reset()을 작성하면 된다.

Ref

[1] z3 microsoft

[2] z3 github

[3] Z3 Solver Class

[4] Z3Py Guide

[5] z3에 적응하기 위해 RedVelvet을 풀어보자.

Footnote

1. SMT(Satisfiability Modulo Theories): 다양한 자료형(Boolean, 실수, 정수, list, bit vector, str등)을 사용하는 복합적인 복합적인 수학적 및 논리적 표현식을 만족할 수 있는지 결정하는 문제를 다루는 이론 ↩︎