z3 training

2025/cscg/crypto/intro3/exploit.py

@@ -1,4 +1,6 @@
-from z3 import Solver, BitVec, sat
+from z3 import Solver, BitVec, sat, ULE
+
+known_prefix = "CSCG{"
 
 def rng(x, size):
     return (x*A+B) & ((2**size)-1)
@@ -17,25 +19,33 @@ MASK = 0xFF
 
 state = SEED 
 
-with open("./msg.txt", "r") as f:
+with open("./test_msg.txt", "r") as f:
     nums = [int(n) for n in f.readlines()[1:]]
     print(nums)
 
-flag_bytes = [BitVec(f'flag_{i}', 56) for i in range(142)]
+flag = []
 
 solver = Solver()
 
 for i, n in enumerate(nums):
     state = rng(state, BITS)
     cur_num = state & MASK
-    solver.add(n == cur_num ^ flag_bytes[i])
-    solver.add(flag_bytes[i] >= 32, flag_bytes[i] <= 126)
-
+    decrypted_char = cur_num ^ n
+    flag.append(decrypted_char)
+    if i < len(known_prefix):
+        solver.add(decrypted_char == ord(known_prefix[i]))
+                     #    else:
+                     #        solver.add(ULE(32, decrypted_char))
+                     #        solver.add(ULE(decrypted_char, 126))
+   
 if solver.check() == sat:
     model = solver.model()
-    flag = ''.join([chr(model[flag_bytes[i]].as_long()) for i in range(142)])
+    recovered_chars = ""
+    for char_expr in flag:
+        val = model.evaluate(char_expr).as_long()
+        recovered_chars += chr(val)
     print(model)
-    print(flag)
+    print(recovered_chars)
 else:
     print("Not solveable")