[Secuinside CTF_2017] TrippleRotate(reversing)

## Secuinside CTF_2017(TrippleRotate, rev)

[Summary]

1. 0과 1로 이루어진 encrypt 파일이 하나 주어지고 문제 바이너리가 주어짐.

2. 문제 바이너리는 9글자 Input을 받고 해당 문자를 암호화 루틴을 거쳐 파일로 떨굼.

3. 복잡한 암호화 알고리즘이 있는데 z3를 이용하여 조건을 만족하는 답을 찾으면 됨.

[Analysis] 

  TrippleRotate 문제는 IDA를 이용하여 분석해보면 아래 [그림 1]과 같이 Input문자를 받는데 9글자인지 체크를 한다.

만약 9글자가 아니면 "check your input"이라는 문자를 출력하고 프로그램이 종료된다.

[그림 1] main 분석

 또한 그 바로 밑에서 Length를 입력 받는데 이 length는 무조건 0xC8보다 커야하고 만약 작다면 "check your length"

라는 문자열을 출력하고 종료한다. 이제 아래부터는 풀었던 방식대로 단계별로 분석을 하도록 하겠다.

 1) 실제로 이 length값은 encrypt 값의 0과 1의 갯수가 된다. 따라서 우리가 decrypt하려는 encrypt파일의 0과 1의 

개수를 확인하면 201이라는 것을 확인할 수 있다.

 2) 이제 [그림 1]에서 보이는 encrypt_400876()함수를 분석해야하는데 해당 함수 내부는 아래 [그림 2]와 같다.

[그림 2] encrypt_400876  분석

 위 [그림 2]를 보면 유심히 살펴봐야할 부분이 빨간 네모박스 친 4군데가 있다. 위에서 부터 차례대로 분석을 해보면 

첫번째 박스는 3번째 네모박스와 연관이 있다. 3번째 for문을 보면 v5변수에 1씩 증가시키면서 함수를 호출하는데 

결과적으로 v5에 저장된 sub_400ACF, v6에 저장된 sub_400B22, v7에 저장된 sub_400B9B함수를 실행시키는 

부분이다.

 실제로는 그 전에 sub_400998함수를 실행하는데 이 함수의 내부를 잘 동적 분석을 해보면 우리가 넣은 인풋의 

한 글자 한 글자마다 2진수로 특정 메모리에 저장하는 것을 알 수 있다. 따라서 이 함수는 string to binary역할을 

하는 함수이다. 그런 다음 Input 스트링을 binary로 변환한 결과를 한 비트씩 0x16번째 비트까지는 first chunk에

집어넣는데 첫번째 비트는 first_chunk[0x16]에 두 번째 비트는 first_chunk[0x15]에 집어넣는 식으로 

first_chunk[0x0]까지 집어넣는 과정을 거친다. 이런 식으로 second_chunk에는 0x17부터 0x18만큼 거꾸로 

집어넣고, third_chunk에는 그 뒤부터 0x19만큼 집어넣는다. 그럼 총 0x17 + 0x18 + 0x19 = 0x48(72)bit

총 9바이트 9글자가 된다.

 예를 들면 아래 [그림3]과 같은 식이다.

[그림 3] first_chunk, second_chunk, third_chunk 값 입력 예제

 마지막 네모 박스는 나중에 설명하도록 하겠다.

 3) 이제 첫 번째 네모 박스의 각 함수에 대해 분석을 해야하는데 sub_400ACF() 함수는 아래 [그림 4]과 같다.

[그림 4] sub_400ACF() 함수 분석

 이 함수에서는 first_chunk배열의 0x17번부터 값을 채워나가는데 [그림 4]의 계산식을 보면 (first_chunk + 5 + i)와 

(first_chunk + i)의 값을 xor하여 (i+0x17)번째 위치에 대입하는 루틴이다.

 4) 이제 첫 번재 네모박스의 sub_400B22()함수에 대해 분석을 할 차례인데 아래 [그림 5]와 같다.

[그림 5] sub_400B22() 함수 분석

 이 함수에서는 second_chunk배열의 0x18번부터  값을 채워나가는데 [그림 5]의 계산식을 보면 

(second_chunk + 1 + i)와 (second_chunk + 3 + i)와 (second_chunk + 4 + i)와 (second_chunk + i)의 

값들을 xor하여 (i+0x18)번째 위치에 대입하는 루틴이다.

 5) 이제 첫 번째 네모박스의 sub_400B9B()함수에 대해 분석을 할 차례인데 아래 [그림 6]과 같다.

[그림 6] sub_400B9B() 함수 분석

 이 함수에서는 third_chunk배열의 0x19번부터 값을 채워나가는데 [그림 6]의 계산식을 보면 (third_chunk + 3 + i)와

(third_chunk + i)를 xor하여 (i+0x19)번째 위치에 대입하는 루틴이다.

 6) 이제 여기까지 분석을 했다면 다시 [그림 2]를 참고하여 23번째 줄 까지 끝낸 상황이다. 이제부터는 24번째 

줄부터인 마지막 박스를 분석해야하는데 이는 매우 쉽다. 위 5번까지 실행을 끝마치면 각 chunk에 값들이 다들어간 

상황이고 이를 단순히 xor과 and연산으로 섞어서 계산하는 부분이기 때문이다. [그림 2]의 마지막 박스에 있는 

계산식을 보면 

{ (second_chunk[k]) & (third_chunk[k]) } xor { (second_chunk[k]) & (first_chunk[k]) } xor { (third_chunk[k]) }

이 최종 결과 값 배열[k]에 대입된다.

 7) 여기까지 완성되면 "encrypt"라는 파일을 쓰는 루틴이 끝이다. 

이제 정연산 분석은 끝났고 역연산 루틴을 짜야하는데 and연산도 있고 해서 짜기가 까다롭다. 그래서 나는 파이썬의 

Z3 모듈을 사용하여 위 정연산 분석했던 조건들을 그대로 집어넣어 결과 값으로 문제에서 주어진 "encrypt"의 결과가 

나오도록 스크립트를 아래와 같이 작성하였다. 

 실제로 스크립트를 돌리면 아래[그림 7]과 같이 조건에 맞는 답이 나타나는데 출력은 각 청크의 0x16까지, 0x17까지, 

0x18까지 출력하도록 하였고, 이를 8비트씩 모아 1바이트로 만들고 9글자를 아스키 문자로 변환하면 키 값을 확인할 수 

있다.

[그림 7] z3사용 스크립트 실행 결과

[Exploit Code] - tripple_rotate_z3_exploit.py

from z3 import *
 
array1 = []
array2 = []
array3 = []
encrypted = [0,0,1,0,0,0,1,0,1,1,0,1,0,1,1,0,1,1,1,0,0,0,1,0,1,0,1,1,1,0,1,0,0,0,0,1,0,0,0,1,1,0,1,1,0,1,1,0,0,0,0,0,1,1,0,1,1,1,0,0,1,0,1,0,1,0,1,1,0,0,1,0,1,0,1,0,1,0,0,0,0,1,1,1,0,1,0,0,1,1,0,0,0,0,0,1,1,1,0,1,1,0,0,0,1,1,1,1,1,1,1,1,0,1,1,1,0,1,0,1,1,0,1,0,1,0,0,1,0,0,0,1,0,0,0,1,1,0,0,1,0,1,0,0,1,0,0,1,1,0,0,0,1,1,0,1,1,1,0,0,1,0,0,1,0,1,1,0,0,1,1,0,1,1,1,1,0,1,1,1,0,1,0,1,1,0,0,1,0,0,1,0,0,0,1,0,1,0,0,0,1]
 
s = Solver()
 
for i in xrange(0xc9):
    array1.append(BitVec('a1_%.3i'%i,1))
for i in xrange(0x17, 0xc9):
    s.add(array1[i] == (array1[i-0x17] ^ array1[i-0x17+5]))
 
for i in xrange(0xc9):
    array2.append(BitVec('a2_%.3i'%i,1))
for i in xrange(0x18, 0xc9):
    s.add(array2[i] == (array2[i-0x18] ^ array2[i-0x18+1] ^ array2[i-0x18+3] ^ array2[i-0x18+4]))
 
for i in xrange(0xc9):
    array3.append(BitVec('a3_%.3i'%i,1))
for i in xrange(0x19, 0xc9):
    s.add(array3[i] == (array3[i-0x19] ^ array3[i-0x19+3]))
 
for i in xrange(0xc9):
    s.add((array2[i] & array3[i]) ^ (array2[i] & array1[i]) ^ (array3[i]) == encrypted[i])
 
print s.check()
answer = s.model()
 
def varname(t):
    return t[0]
 
array1_decrypted = []
array2_decrypted = []
array3_decrypted = []
 
for i in answer.decls():
    if "a1_" in str(i.name()):
        array1_decrypted.append((str(i.name()),answer[i]))
    if "a2_" in str(i.name()):
        array2_decrypted.append((str(i.name()),answer[i]))
    if "a3_" in str(i.name()):
        array3_decrypted.append((str(i.name()),answer[i]))
 
    #print "%s = %s"%(i.name(), answer[i])
 
array1_decrypted.sort(key=varname)
array2_decrypted.sort(key=varname)
array3_decrypted.sort(key=varname)
 
print "## first chunk ##"
for i in xrange(0x17):
    print array1_decrypted[i][1],
print "\n## second chunk ##"
for i in xrange(0x18):
    print array2_decrypted[i][1],
print "\n## third chunk ##"
for i in xrange(0x19):
    print array3_decrypted[i][1],
    
 

끝~!