ASIS 2015 fake

이상한 연산결과를 통해서

v5부터 v9까지 연속해서 출력해준다.

그냥 저식대로 z3에 넣어주면됨.

ASIS ctf 키값 형식이 ASIS{~~} 니까 앞의 글자 5개는 스택에 {SISA로 들어가게 될것이다.

따라서

>>> s.add((((0x3CC6C7B7 * v2)) & 0x000000ffffffffff) == int("{SISA".encode('hex'),16))

>>> s.model()

Traceback (most recent call last):

  File "<stdin>", line 1, in <module>

  File "/usr/lib/python2.7/dist-packages/z3.py", line 5952, in model

    raise Z3Exception("model is not available")

z3types.Z3Exception: model is not available

>>> s.check()

sat

>>> s.model()

[v2 = 25313971399]

ㅎ