Encuentra la bandera en
un binario CTF.

Encuentra el código de verificación

El folleto es un ejecutable de 15 KB. Pide una bandera, luego imprime Correct! o Incorrect!. Comience con una simple solicitud a su agente.

Un mensaje de ejemplo, con el desafío descargado disponible localmente y un análisis del proveedor de programas de código máquina conectado.

1. Siga el indicador de entrada a su función

   Agente → REA

   open_binary
   {"path": "ms_flag_checker"}
   
   search_strings
   {"pattern": "flag|correct|wrong|input",
    "mode": "regex", "case_sensitive": false}
   
   xrefs
   {"address": "0x102004"}
   
   resolve_containing_procedure
   {"address": "0x10126d"}

   REA → agente * resultados seleccionados

   0x102004  "What is the flag? "
   0x10201c  "Incorrect!"
   0x102027  "Correct!"
   
   Prompt referenced at: 0x10126d
   Containing function: 0x10124d

   La referencia le da al agente un lugar para investigar, aunque se hayan eliminado los nombres de funciones originales del ejecutable.

2. Lea el corrector y sus dos ayudantes

   Agente → REA

   analyze_function
   {"procedure": "0x10124d"}
   
   analyze_function
   {"procedure": "0x101189"}
   
   analyze_function
   {"procedure": "0x101217"}

   REA → agente * instrucciones seleccionadas

   0x1012c1: CMP EDI, 0x24
   0x1012c6: LEA RBX, [0x1040e0]
   0x1012cd: LEA RBP, [0x104060]
   0x1012d4: LEA R13, [RBX + 0x270]
   0x1012e1: CALL 0x00101189
   0x1012ec: CALL 0x00101217
   0x1012f1: CMP dword ptr [RBP], EAX
   0x1012f4: JNZ 0x00101335
   0x1012f6: ADD RBX, 0x18

   El primer bucle copia códigos de 36 caracteres. El bucle de comprobación decodifica una máscara, suma los códigos seleccionados y compara el resultado con un número almacenado. Su 0x18- pasos de bytes a través 0x270 los bytes dan 26 máscaras.

Estos son resultados seleccionados de un análisis REA reciente. La ruta de destino local se acorta para su visualización; las direcciones se refieren a la imagen importada de REA.

Un cheque revela un carácter

El verificador organiza la entrada en una cuadrícula de 6×6. Una máscara elige qué celdas contribuyen a una suma. Su codificación compacta utiliza números negativos para omitir celdas y números positivos para seleccionarlos.

Lea la máscara y su objetivo desde el binario

{"address": "0x1040e0", "length": 624}
{"address": "0x104060", "length": 144}

Mask at 0x104170:
eb 01 f2 00  →  -21, +1, -14, stop

Target at 0x104078:
37 00 00 00  →  55

La instrucción MOVSX lee bytes de máscara como valores firmados. Esta es la razón eb significa -21. El objetivo es un entero little-endian. Juntos, estos bytes le dicen al agente que code[21] = 55, entonces ese personaje es 7.

De las instrucciones a un cheque legible

Seleccione un paso para conectar el ayudante de suma y su interlocutor a la misma regla en C.

0x10121c: MOV ECX, 0x0

0x10122c: CMP dword ptr [RSI + RAX*0x1], 0x0
0x101230: JZ 0x00101223

0x101232: ADD ECX, dword ptr [RDI + RAX*0x1]

0x101223: ADD RAX, 0x4

0x1012f1: CMP dword ptr [RBP], EAX
0x1012f4: JNZ 0x00101335

int check_one_mask(const int codes[36],
                   const int mask[36],
                   int target) {
    int total = 0;
    for (int i = 0; i < 36; ++i) {
        if (mask[i]) {
            total += codes[i];
        }
    }
    return total == target;
}

Las instrucciones provienen del ayudante de suma y de su persona que llama. La C es un resumen explicativo con nombres descriptivos y un bucle aplanado de 36 celdas.

Resuelve las 26 ecuaciones

La mayoría de las máscaras seleccionan varias celdas. Por ejemplo, la primera verificación agrega códigos de 16 caracteres y requiere un total de 1441. Las selecciones superpuestas dan ecuaciones que un pequeño script de Python puede resolver juntas.

from z3 import Int, Or, Solver, Sum, sat

codes = [Int(f"code_{i}") for i in range(36)]
solver = Solver()
alphabet = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789_{}"
for code in codes:
    solver.add(Or(*[code == ord(c) for c in alphabet]))
for code, char in zip(codes, "DUCTF{"):
    solver.add(code == ord(char))
solver.add(codes[-1] == ord("}"))

for selected, target in checks:
    solver.add(Sum([codes[i] for i in selected]) == target)

assert solver.check() == sat
model = solver.model()
print("".join(chr(model.eval(code).as_long()) for code in codes))

Z3 es un solucionador que encuentra valores que satisfacen estas ecuaciones. Este extracto usa los cheques extraídos y asume un DUCTF{…} bandera con letras, dígitos, guiones bajos y llaves. La descarga completa incluye las 26 máscaras y objetivos.

Verifique la respuesta con el programa original

La captura de procesos de REA registra el ejecutable original aceptando el indicador resuelto. Cambiar un carácter seleccionado de z para y hace la primera suma 1440 en lugar de 1441, y el programa la rechaza.

What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa}
Correct!

dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae

Pruébalo tú mismo

Descargue el desafío original y el solucionador en una carpeta. Utilice el mensaje anterior para investigar con su agente o ejecute el script incluido.

python3 -m venv .venv
.venv/bin/python -m pip install z3-solver
.venv/bin/python solve.py

chmod +x ms_flag_checker
./ms_flag_checker

El script imprime un indicador de candidato; péguelo en el indicador del programa. Resolviendo necesidades Python y z3-solver. Ejecutar el ejecutable original necesita Linux x86-64.