OZ1NG의 뽀나블(Pwnable)

[*] 이슈 z3에서 미지수를 만들때 사용하는 BitVec()은 기본적으로 모든 미지수를 signed 값으로 취급한다. 때문에 이런 이슈가 발생하게 된다. from z3 import * # 미지수 a0, a1을 1bit 크기의 미지수로 설정 a0 = BitVecs('a0', 1) a1 = BitVecs('a1', 1) s = Solver() s.add(a0 > a1) print(s.check()) print(s.model()) $ python3 z3test.py sat [a0 = 0, a1 = 1] # ?????????????????? 위와 같이 a1의 값이 1로 더 크게 나와버린다. - signed는 최상위 bit를 부호 비트로 사용하여 1이면 음수라고 인식하는데, a0과 a1은 1 bit 크기의 미지..