2016 POX_FINAL meow

이 문제는 동아리 여자애들이 작년 POX_FINAL에서 받아온 문제다.

첨에 그냥 알고리즘문제 인가보다 하고 넘어갔다가 최근에 생각나서 풀어보았다.

나는 비트연산과 z3을 이용해서 간단히 풀었다.

문제는 스위치가 64개 있고, 각각의 스위치에는 3,4개 정도의 LED번호가 있다.

스위치는 한번 누르면 다시 누를수가없다.

즉, 64개의 스위치를 누르지않거나 누르거나 해서 64개의 LED를 True상태로 만들어야한다.

나는 각각의 스위치에 해당하는 LED를 64bit에 해당하는 2진수로 바꿔서 생각을 했다.

이렇게 하면 64개의 스위치중 특정 스위치들을 xor했을 때, 1*64 개가 되는 값을 찾으면 바로 정답이 나온다.

또한 seed범위가 1000까지 밖에 안되기 때문에,  seed마다의 스위치상태를 다 저장해놓고

서버에서 0번째 스위치를 눌렸을때 trigger되는 LED를 통해 seed를 알아내고, 해당 seed의 스위치상태를 불러와서 z3를 통해 문제를 풀 수 있었다.

from z3 import *
from pwn import *
import random

make_bin = lambda x : bin(x).lstrip('0b').rjust(64, '0')

def change_bit(arr):
    sum_ = 0
    for i in arr:
        sum_ += 2**i
    return sum_

def make_button():
    button_list = []
    button_seed = {}
    for idx in range(1000):
	random.seed(idx)
	sets = []
	LED = [False] * 64
	BUTTON = {}
	for x in range(len(LED)):
            sets.extend([x] * 4)
	random.shuffle(sets)
	COUNT = 0

	for n in range(64):
            BUTTON[n] = set([sets.pop() % 64 for _ in range(4)])
        button_list.append(BUTTON)
        first_value = change_bit(list(BUTTON[0]))
        button_seed[make_bin(first_value)] = idx
    return button_list, button_seed

def solver(seed_button):
    s = Solver()

    unk = [0 for _ in range(64)]

    for i in range(64):
        unk[i] = BitVec('unk[{}]'.format(i), 64)

    value_list = [ list(seed_button[i]) for i in seed_button ]

    for idx, dat in enumerate(value_list):
        value_list[idx] = change_bit(dat)

    for i in range(64):
        s.add(
            unk[i] < 2,
            unk[i] >= 0,
        )

    str_ = ''
    for i in range(64):
        str_ += '{0}*{1}'.format(value_list[i], unk[i])
        str_ += '^'
    str_ = str_[:-1]
    str_ += ' == '
    str_ += '{0}'.format(2**64-1)

    s.add( eval(str_) )
    try:
        s.check()
        m = s.model()
        key = []
        for d in m.decls():
            if m[d] == 1:
                key.append(d.name().strip('unk[]'))
        return key
    except:
        return []

def find_seed(button_seed):
    led = []
    fast(':', 2, 0)
    p.recvuntil('command: ')
    p.sendline('1')
    dat = p.recvuntil('1. check')
    for d in dat.split('\n')[:-1]:
        idx, value = d.strip('()').split(', ')
        if value == 'True':
            led.append(idx)
    key = make_bin(change_bit(map(int, led)))
    return button_seed[key]

def command(token, *args) :
    p.recvuntil(token)
    for i in args :
        i = str(i)
        p.sendline(i)

fast = lambda token, *args : command(token, *args)

if __name__ == '__main__':
    button_list, button_seed = make_button()
    print '[+] Success button list'
    while True:
        p = remote(secret)
        seed = find_seed(button_seed)
        print '[+] Success Find Seed -> {}'.format(seed)
        button = solver(button_list[seed])
        if len(button) == 0:
            print '[-]Fuck!'
            continue
        print '[+] Good! Get Flag!'
        for dat in button:
            if dat != 0:
                fast('command', 2, dat)
        p.recvuntil('1')
        p.interactive()
        break