new

.gitignore

@@ -0,0 +1 @@
+venv

crackmes/xorsimple/solve.py

@@ -0,0 +1,40 @@
+import time
+import angr
+
+if __name__ == "__main__":
+    # Загрузка бинарного файла
+    proj = angr.Project('a.exe', auto_load_libs=False)
+    ENTRY_POINT = 0x140001837 # Адрес функции после вызова scanf
+    TARGET_ADDR = 0x140001848 # Целевой адрес, нахождение на нем означает что програмам взломана
+
+    # Создание начального состояния
+    state = proj.factory.entry_state(
+        addr=ENTRY_POINT,
+        add_options={angr.options.ZERO_FILL_UNCONSTRAINED_REGISTERS, 
+                    angr.options.ZERO_FILL_UNCONSTRAINED_MEMORY}
+    )
+
+    # Инициализация стека
+    state.regs.rbp = 0x7ffffffffffffff
+    state.regs.rsp = 0x7ffffffffffffff
+
+    # Симуляция ввода пользователя
+    input_size = 5
+    input_data = state.solver.BVS('input_data', 8 * input_size)
+    state.memory.store(state.regs.rbp - 0x50, input_data)
+
+    # Установка ограничений
+    for byte in input_data.chop(8):
+        state.add_constraints(byte >= 0x20)
+        state.add_constraints(byte <= 0x7e)
+
+    simgr = proj.factory.simulation_manager(state)
+    start_time = time.time()
+    simgr.explore(find=TARGET_ADDR)
+    elapsed = time.time() - start_time
+
+    if simgr.found:
+        input_data = simgr.found[0].solver.eval(input_data, cast_to=bytes)
+        print(f"Success cracked! Input: {input_data} | Pwd cracking time = {elapsed}")
+    else:
+        print("Fail!")

crackmes/xorsimple/xorcr.c

@@ -0,0 +1,24 @@
+#include <stdio.h>
+
+char *serial = "\x31\x3e\x3d\x26\x31";
+
+int check(char *ptr) {
+    int i = 0;
+    while (i < 5){
+        if (((ptr[i]) ^ 0x55) != serial[i]) 
+            return 0;
+        i++;
+    }
+    return 1;
+}
+
+int main() {
+    char inp[72] = {0};
+    scanf_s("%s", inp);
+    if (check(inp) == 1) {
+        printf("win");
+    } else {
+        printf("fail"); 
+    }
+    return 0;
+}

z3example.py

@@ -0,0 +1,8 @@
+import z3
+
+z = z3.Solver()
+x = z3.BitVec('x', 32)
+y = z3.BitVec('y', 32)
+z.add(x + y == 20)
+print(z.check()) # sat -> разрешимо
+print(z.model()) # y = 0, x = 20