myria's place

from z3 import *
s = Solver()
x1 = Int('x1')
x2 = Int('x2')
x3 = Int('x3')
x4 = Int('x4')
x5 = Int('x5')
s.add(x1 + x2 + x3 + x4 + x5 == x1*x2*x3*x4*x5)
print s.check()
print s.model()

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
from z3 import *
 
s = Solver()
 
# 변수들
x1 = Int('x1')
x2 = Int('x2')
x3 = Int('x3')
x4 = Int('x4')
x5 = Int('x5')
 
s.add(x1 + x2 + x3 + x4 + x5 == x1*x2*x3*x4*x5)        # 조건식
 
print s.check()
print s.model()
Colored by Color Scripter
cs

angr 간단소개

Angr은 UC Santa Barbara Computer security lab서 개발할 파이선 기반 바이너리 분석 프레임워크이다. 강력한 Symbolic execution 기능으로 2015 blackhat에서 발표되고 angr을 기반으로 제작된 취약점 분석 모듈 들이 2016 DEFCON이후 공개되어 이슈가 되고 있다. 뿐만 아니라 그래프를 그려줄 수 있는 networkx 모듈과 연동하여 Code-flow를 시각화 할 수 있는 점이나 중간언어인 VEX IR을 이용하여 코드의 동작 형태와 시뮬레 이션 결과를 저장하여 보여주는 점 등, 분석에서의 많은 이점을 보여주고 있다.

리버싱 바이너리파일을 이를 이용해서 쉽게 해결할 수 있다고 한다.

또 다른 라이브러리로는 Z3도 있다.

나중에 한번 알아보면 좋을듯... 그때는 이글도 업데이트