6_Symbolic Execution, Z3 체험해보기

YUMMMM 2023. 5. 12. 05:33

이번 주에는 Z3와 symbolic execution을 체험해보는 과제를 진행했지만 많은 것을 얻지 못 했다.

1. Z3 사용해보기(2)

먼저 Z3로 테스트 해 볼 조건들은 다음과 같다.

0 == (x*(x+1)) % 2 #s
0 != (x*(x+1))%2 #s2

x == (x+1-1) #s3
x == 2*x #s4
x != 2*x #s5

x != (x+1-1) #s6

밑은 해당 조건들을 테스트하고, 만족하는지 결과를 출력해주는 코드이다. (s2가 주석처리 되어있는 이유는 밑에서 설명)

from z3 import *

x = Int('x')
s = Solver()
print(s)
s.add(0 == (x*(x+1)) % 2)
print(s)
s.check()
print(s.check())

print()

'''
x = Int('x')
s2 = Solver()
print(s2)
s2.add(0 != (x*(x+1))%2)
print(s2)
s2.check()
print(s2.check())
'''

s3 = Solver()
print(s3)
s3.add(x == (x+1-1))
print(s3)
s3.check()
print(s3.check())

print()

s4 = Solver()
print(s4)
s4.add(x == 2*x)
print(s4)
s4.check()
print(s4.check())

print()

s5 = Solver()
print(s5)
s5.add(x != 2*x)
print(s5)
s5.check()
print(s5.check())

print()

s6 = Solver()
print(s6)
s6.add(x != (x+1-1))
print(s6)
s6.check()
print(s6.check())

> 실행결과 (위 s, s3, s4, s5, s6/ 아래 s2)

s의 경우, 연속하는 두 정수의 곱은 항상 짝수이므로 sat

s3의 경우, x + 1 - 1은 늘 x와 같으므로 sat

s4의 경우, x가 0일 때 만족하므로 sat

s5의 경우, x가 0이 아닐 때 만족하므로 sat

s6의 경우, s3과 반대인 경우이므로 unsat

s2의 경우는 s와 반대라고 생각하여 당연히 unsat이 나올 줄 알았는데 check() 상태가 출력되지 않은 채로 계속해서 돌아간다. 교수님께서 sat이 나오는 경우는 해당 조건을 만족하는 경우가 한 번이라도 있으면 바로 sat을 출력하는 것 같다고 말씀을 해주셨는데, 그럼 만족하는 값이 혹시나 있을까 해서 모든 값을 연산해보는 걸까? 왜 unsat이 바로 나오지 않고 계속해서 돌아가는지 궁금하다. z3-solver 깃허브를 조금 훑어봤는데 unsat, 무한루프와 관련된 issue(https://github.com/Z3Prover/z3/issues/578)를 찾긴 했는데 이것과 비슷한 경우인지 더 알아봐야 할 것 같다. 아직은 머리만 긁적여봤다. 아니면.. 아무일 없다는 듯이 넘어가주면 됨

2. Symbolic execution 체험해보기(3)

벌써 세 번째 체험기인데, 이번에는 조교님께서 전에 사용하던 코드에 cpu 아키텍처를 인식해 자동으로 설정하는 코드를 추가해서 주셨다.

하지만 miasm 자체에서 여전히 m2 맥을 지원하지 않기 때문에 맥에서 컴파일한 실행파일은 돌아가지 않았다. (아래 참고)

그래서 윈도우 64비트에서 돌린 실행파일을 넣어서 실행해보기로 했다.

먼저 c 파일 코드들이다. 약간 같은 결과를 내는 비슷한 코드들의 symbolic execution이 어떻게 나올지 궁금해서 짜본 비슷한 코드들과 분기문을 넣은 코드이다.

test_1

int main() {
	int a = 1;
    int b = 2;
    int result;
    
    result = a + b;
    
    return result;
}

test_2

int main() {
	int result = 1 + 2;
    
    return result;
}

test_3

int main() {
	int a = 1;
    int b = 2;
    
    return a + b;
}

test_4

int main() {
	int a = 3;
    int b = 2;
    int result = 0;
    
    if(a >= b)
    	result = a;
    else
    	result = b;
        
    return result;

}

컴파일

> 실행결과

결과 캡처가 한 개만 있는 것은 이유가 있다. 모든 실행파일을 돌렸을 때 모두 이 결과가 나왔다. 문제가 있는 것이 분명한데 뭐가 문제인지를 모르겠다. 전에 만들어놨던 실행파일, 새로 만든 실행파일, 조교님이 주셨던 실행파일 모두 이 결과가 나온다.. 문제가 뭘까? ㅜㅜ 아무래도 또 여쭤봐야 할 것 같다.

3. 느낀 점

오랜만에 진행한 과제인데 결과가 또 좋지 않은 것 같고 얻는 게 아무것도 없는 느낌이다. 질문하지 않고는 아무것도 못 하는 것 같다.

그래도.. 기죽지 말아야지