Success - smileyCTF 2025
Haskellのソースコードが与えられる
基本的な演算を繰り返しているだけなので、いい感じにパースして解く
code:python
import re
from z3 import *
with open('success.hs', 'r') as f:
lines = f.readlines()
PAT1 = re.compile(r'\((^)+)\) \(chars !! (\d+)\) \(chars !! (\d+)\) == (^ +)') PAT2 = re.compile(r'xor \(chars !! (\d+)\) \(chars !! (\d+)\) == (^ +)') PAT3 = re.compile(r'\((^)+)\) \(\((^)+)\) \(chars !! (\d+)\) \(chars !! (\d+)\)\) (\d+) == (^ +)') s = Solver()
def do_op(op, opr1, opr2):
match op:
case '+':
return opr1 + opr2
case '-':
return opr1 - opr2
case '*':
return opr1 * opr2
case '.|.':
return opr1 | opr2
case '.&.':
return opr1 & opr2
case 'xor':
return opr1 ^ opr2
case _:
exit(op)
for line in lines:
if m := PAT1.search(line):
op = m.group(1)
idx1 = int(m.group(2))
idx2 = int(m.group(3))
result = int(m.group(4))
s.add(do_op(op, flagidx1, flagidx2) == result) if m := PAT2.search(line):
op = 'xor'
idx1 = int(m.group(1))
idx2 = int(m.group(2))
result = int(m.group(3))
s.add(do_op('xor', flagidx1, flagidx2) == result) if m := PAT3.search(line):
op1 = m.group(1)
op2 = m.group(2)
idx1 = int(m.group(3))
idx2 = int(m.group(4))
opr = int(m.group(5))
result = int(m.group(6))
s.add(do_op(op1, do_op(op2, flagidx1, flagidx2), opr) == result) assert s.check() == sat
m = s.model()
print(''.join(chr(m[flagi].as_long()) for i in range(39)))