Chaining

결국 문제는 해결을 했는데.. 도저히 이해가 안가는 결론이 나와서 질문드립니다. 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비트를 부호비트를 쓸까? 해서 테스트를 해봤는데, 그것도 아니네요..