--- title: 'Ingeniería inversa CTF: Comprobador de banderas DownUnderCTF-REA' url: https://rea.tools/es/showcase/ctf/ --- [Inicio](https://rea.tools/es/) / [Vitrinas](https://rea.tools/es/showcase/) / CTF Estudio de caso · DownUnderCTF 2023 # Encuentra la bandera en un binario CTF. Use REA para inspeccionar un pequeño verificador de indicadores, convertir sus reglas en ecuaciones y encontrar una entrada que haga que se imprima el programa original `Correct!`. comprobador de banderas de cuadrados enmascarados \* Fácil \* Linux x86-64 [Ver el desafío original](https://github.com/DownUnderCTF/Challenges_2023_Public/tree/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker) De una respuesta binaria a una respuesta marcada 1. 01 \* Encuentra el cheque **Cadenas → funciones de comprobación** REA encuentra el indicador, sus referencias y el código que acepta o rechaza una entrada. 2. 02 \* Extraer las reglas **36 caracteres · 26 sumas** REA devuelve las instrucciones y los datos detrás de cada comprobación. El agente los convierte en ecuaciones. 3. 03 \* Resuelve y corre **Bandera recuperada → ¡Correcto!** Un script de Python resuelve las ecuaciones. REA captura el programa original aceptando el resultado. El desafío es de joseph, publicado en el repositorio oficial de DownUnderCTF. ## 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. Su agente de codificación Use REA para analizar ms_flag_checker y encontrar el indicador. Explique cómo funcionan las comprobaciones y luego verifique la respuesta con el programa original. 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. ![La séptima máscara omite 21 celdas, selecciona la posición 21 y luego omite 14. Solo esa celda contribuye a la suma. Su código de carácter requerido es 55, lo que significa que el carácter es 7.](https://rea.tools/assets/localized/es/figures/ctf-mask-equation.svg) La séptima comprobación selecciona solo una posición. [Figura abierta](https://rea.tools/assets/localized/es/figures/ctf-mask-equation.svg). ### Lea la máscara y su objetivo desde el binario Agente → REA \* read_bytes ``` {"address": "0x1040e0", "length": 624} {"address": "0x104060", "length": 144} ``` REA → agente \* séptima entradas ``` 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. REA \* instrucciones originales seleccionadas ``` 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 ``` Resumen legible de C \* one-check ``` 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; } ``` **01 \* Comience en cero.** `ECX` contiene la suma corriente. **02 \* Compruebe la celda de la máscara.** Un valor cero omite el carácter; un valor distinto de cero lo incluye. **03 \* Agregue un código de carácter.** El entero de la entrada en el mismo desplazamiento se agrega a la suma. **04 \* Pasar a la siguiente celda.** El bucle original avanza cuatro bytes por entero y visita seis filas de seis celdas. **05 \* Comparar con el objetivo almacenado.** La persona que llama recibe la suma en `EAX`. Un desajuste salta a `Incorrect!`. 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. Extracto de Python \* solver ``` 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. [Descargue el solucionador completo](https://rea.tools/showcase/ctf/solve.py) ## 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. | Entrada | Salida observada | Código de salida | | --- | --- | --- | | Bandera del solucionador | `Correct!` | 0 | | Un personaje cambió | `Incorrect!` | 255 | Mostrar el indicador recuperado y la salida capturada REA \* salida del programa original ``` What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa} Correct! ``` El valor recuperado también coincide con la bandera en los metadatos de desafío publicados por los organizadores, marcada después de resolver el binario. Detalles de origen, identidad de destino y análisis Análisis reciente y dos capturas de procesos el 8 de octubre de 2026, utilizando REA 4.1.0 con Ghidra 12.1.4 en Linux x64. El binario es un ELF x86-64 despojado, 15.248 bytes. Ejecutable original \* SHA-256 ``` dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae ``` Las referencias de cadena, funciones y constantes se inspeccionaron antes de leer la fuente o solución de los organizadores. El solucionador de Python y el diagrama se construyeron a partir de esos resultados de REA. [Compare con la fuente de los organizadores](https://github.com/DownUnderCTF/Challenges_2023_Public/blob/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/src/ms_flag_checker.c) · [Metadatos de desafío y bandera](https://github.com/DownUnderCTF/Challenges_2023_Public/blob/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/ctfcli.yaml) · [Notas de evidencia REA](https://github.com/morluto/rea/blob/main/website/evidence/ctf-masked-squares.md) ## 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. [Descarga el desafío original](https://raw.githubusercontent.com/DownUnderCTF/Challenges_2023_Public/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/publish/ms_flag_checker)[Descargar solver](https://rea.tools/showcase/ctf/solve.py) Terminal \* resuelve y ejecuta ``` 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. [Configure REA con su agente de codificación](https://rea.tools/get-started/)