Question

결국 문제는 해결을 했는데.. 도저히 이해가 안가는 결론이 나와서 질문드립니다. flag를 1바이트 * 0x40 배열로 선언해서 z3 를 이용해서 해결했는데요.
아래와 같은 조건으로는 unsat이 떠서 해결이 안됐습니다. 그래서 대회 내내 뻘짓을 했구요..

s = Solver()
flag = [BitVec('flag{}'.format(i), 8) for i in range(0x40)]
for i in range(0x40):
    s.add(flag[i] <= 0x7F)
    s.add(flag[i] >= 0x20)

근데 8비트가 아닌 9비트로 늘려주고 마지막에 값을 검증하는 부분을 조금 바꿔주니 sat가 뜨더군요. 근데 마지막에 0xff and 연산을 빼면 또 unsat 입니다.

s = Solver()
flag = [BitVec('flag{}'.format(i), 9) for i in range(0x40)]
for i in range(0x40):
    s.add(flag[i] <= 0x7F)
    s.add(flag[i] >= 0x20)
    
def check(a1): #a1 에는 flag 가 들어갑니다.
   .....
    for i in range(0, 0x40):
        s.add((a1[i]&0xFF) == last[i]) #0xFF와 AND연산 추가

제약 조건상으로 0x20 ~ 0x7F 면 이미 1바이트라는 제약조건이 걸린게 아닌가요 ? 그리고 1바이트라는 제약조건이 있을 때도 0xFF AND 연산이 왜 결과에 영향을 줄까요?
혹시 상위 1비트를 부호비트를 쓸까? 해서 테스트를 해봤는데, 그것도 아니네요..

#reversing

Answer 1

BitVec 을 이미 BitVec('flag{}'.format(i), 8) 로 만드셨기 때문에 8비트인 상태는 맞습니다.
아마 ror/rol 부분에서 >> 를 쓰셔서 arithmetic shift right 가 된 것 같습니다. (참고)
z3.LShR 쓰면 해결할 수 있고 저도 z3 쓰는 풀이 첨부해뒀습니다.

아니면 그냥 z3 에 RotateLeft / RotateRight 쓰면 문제 없는 것 같네요

2023.08.13. 03:53