dingdong

training/IntroZ3/tasks/chall2_dreamer/exploit.py

@@ -6,10 +6,17 @@ import sys
 
 
 def ROL(X, N):
-    return ((((X) << (N)) | ((X) >> (64 - (N)))) % (2 ** 64))
+    if isinstance(X, z3.BitVecRef):
+        return z3.RotateLeft(X,N)
+    else:
+        return ((((X) << (N)) | ((X) >> (64 - (N)))) % (2 ** 64))
+
 
 def ROR(X, N):
-    return ((((X) >> (N)) | ((X) << (64 - (N)))) % (2 ** 64))
+    if isinstance(X, z3.BitVecRef):
+        return z3.RotateRight(X,N)
+    else:
+        return ((((X) >> (N)) | ((X) << (64 - (N)))) % (2 ** 64))
 
 def custom_random(state):
     NEW_STATE = ROL(state,30) ^ ROR(state,12) ^ ROL(state,42) ^ ROL(state,4) ^ ROR(state,5);

training/IntroZ3/tasks/chall2_dreamer/test.py

@@ -24,6 +24,7 @@ def get_seed_for_sequence(bytesequence):
     s = z3.Solver() 
     base_state = z3.BitVec("base_state", 64)
     cur_state = base_state
+    s.add(base_state > 0)
     for byte in bytesequence:
         gen_byte, cur_state = custom_random(cur_state)
         s.add(gen_byte == byte)
@@ -44,7 +45,7 @@ def gen_sequence(seed, length):
     return bytes(r)
 
 
-test = random.getrandbits(32).to_bytes(4)
+test = random.getrandbits(32).to_bytes(4, "little")
 seed = get_seed_for_sequence(test)
 print(seed)
 print(test)

training/IntroZ3/tasks/chall3_archventure/README.md

@@ -7,10 +7,10 @@ The license key has the form XXXXX-XXXXX-XXXXX-XXXXX
 The template code will mostly ignore the '-' (since the binary does it mostly as well) and `license[5]` will refer to the 6th X
 
 For context:
- - The binary will perform some general constraint checks on the license
- - The binary will extract 4 binaries of different architectures that each contain different parts of a constraint set and are then executed
-   - The constraints are described in the template and the relevant arrays extracted already
 
+- The binary will perform some general constraint checks on the license
+- The binary will extract 4 binaries of different architectures that each contain different parts of a constraint set and are then executed
+  - The constraints are described in the template and the relevant arrays extracted already
 
 To validate your license key, run the binary (it requires qemu and some dependencies, so using the Dockerfile might be easiest):