--- title: 'Engenharia reversa de CTF: Verificador Da Bandeira de DownUnderCTF-REA' url: https://rea.tools/pt-BR/showcase/ctf/ --- [Casa](https://rea.tools/pt-BR/) / [Vitrines](https://rea.tools/pt-BR/showcase/) / CTF Estudo de caso \* DownUnderCTF 2023 # Encontre a bandeira em um binário CTF. Use REA para inspecionar um pequeno verificador de bandeiras, transformar suas regras em equações e encontrar uma entrada que faça o programa original imprimir `Correct!`. verificador Mascarado da bandeira dos quadrados \* fácil \* Linux x86-64 [Veja o desafio original](https://github.com/DownUnderCTF/Challenges_2023_Public/tree/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker) De um binário para uma resposta verificada 1. 01 \* encontrar o cheque **Cadeias de caracteres extraterritoriais** REA encontra o prompt, suas referências e o código que aceita ou rejeita uma entrada. 2. 02 \* extrair as regras **36 caracteres \* 26 somas** REA retorna as instruções e os dados por trás de cada verificação. O Agente os transforma em equações. 3. 03 \* resolver e executar **Bandeira recuperada valuetech Correct!** Um script Python resolve as equações. REA captura o programa original aceitando o resultado. O desafio é de joseph, publicado no repositório oficial da DownUnderCTF. ## Encontrar o código de verificação O folheto é um executável de 15 KB. Pede uma bandeira, depois imprime `Correct!` ou `Incorrect!`. Comece com um simples pedido ao seu agente. O seu agente de codificação Use REA para analisar ms_flag_checker e encontrar o sinalizador. Explique como funcionam as verificações e, em seguida, verifique a resposta com o programa original. Um exemplo de alerta, com o desafio baixado disponível localmente e uma análise do provedor de programas de código de máquina conectado. 1. #### Siga o prompt de entrada para sua função 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 extraterritorial \* resultados seleccionados ``` 0x102004 "What is the flag? " 0x10201c "Incorrect!" 0x102027 "Correct!" Prompt referenced at: 0x10126d Containing function: 0x10124d ``` A referência dá ao Agente um local para investigar, mesmo que os nomes das funções originais do executável tenham sido removidos. 2. #### Leia o verificador e seus dois ajudantes Agente REA ``` analyze_function {"procedure": "0x10124d"} analyze_function {"procedure": "0x101189"} analyze_function {"procedure": "0x101217"} ``` REA7 agente \* instruções 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 ``` O primeiro ciclo copia códigos de 36 caracteres. O ciclo de verificação descodifica uma máscara, soma os códigos seleccionados e compara o resultado com um número memorizado. Sua `0x18`- passos byte através `0x270` bytes dar 26 máscaras. Estes são resultados seleccionados de uma nova análise REA. O caminho de destino local é encurtado para exibição; os endereços referem-se à imagem importada de REA. ## Uma verificação revela um carácter O verificador organiza o input numa grelha de 6-6. Uma máscara escolhe quais células contribuem para uma soma. Sua codificação compacta usa números negativos para pular células e números positivos para selecioná-los. ![A sétima máscara Pula 21 células, seleciona a posição 21 e, em seguida, Pula 14. Só essa célula contribui para a soma. Seu código de caracteres exigido é 55, o que significa que o caractere é 7.](https://rea.tools/assets/localized/pt-BR/figures/ctf-mask-equation.svg) A sétima verificação selecciona apenas uma posição. [Figura aberta](https://rea.tools/assets/localized/pt-BR/figures/ctf-mask-equation.svg). ### Leia a máscara e seu alvo a partir do binário Agente REA \* read_bytes ``` {"address": "0x1040e0", "length": 624} {"address": "0x104060", "length": 144} ``` REA7agente \* sétima entrada ``` Mask at 0x104170: eb 01 f2 00 → -21, +1, -14, stop Target at 0x104078: 37 00 00 00 → 55 ``` A instrução `MOVSX` lê bytes de máscara como valores assinados. É por isso que `eb` meios -21. O alvo é um número inteiro little-endian. Juntos, esses bytes informam ao agente que `code[21] = 55`, então esse personagem é `7`. ## Das instruções a um controlo legível Selecione uma etapa para conectar o Auxiliar de soma e seu chamador à mesma regra em C. REA \* instruções originais selecionadas ``` 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 ``` C · resumo de uma verificação legível ``` 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 \* Comece em zero.** `ECX` detém a soma corrente. **02 \* Verifique a célula da máscara.** Um valor zero ignora o caractere; um valor diferente de zero o inclui. **03 \* adicionar um código de caracteres.** O número inteiro da entrada no mesmo deslocamento é adicionado à soma. **04 \* passar para a célula seguinte.** O loop original avança quatro bytes por inteiro e visita seis linhas de seis células. **05 \* comparar com o alvo armazenado.** O chamador recebe a soma em `EAX`. Uma incompatibilidade salta para `Incorrect!`. As instruções vêm do Auxiliar de Somação e do seu interlocutor. O C é um Resumo Explicativo com nomes descritivos e um loop de 36 células achatado. ## Resolva as 26 equações A maioria das máscaras seleciona várias células. Por exemplo, a primeira verificação adiciona 16 códigos de caracteres e requer um total de 1441. As seleções sobrepostas fornecem equações que um pequeno script Python pode resolver juntos. Python \* trecho do 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 é um solucionador que encontra valores que satisfazem essas equações. Este excerto utiliza as verificações extraídas e assume uma `DUCTF{…}` bandeira com letras, dígitos, sublinhados e chaves. O download completo inclui todas as 26 Máscaras e alvos. [Baixe o solucionador completo](https://rea.tools/showcase/ctf/solve.py) ## Verifique a resposta com o programa original A captura de processo do REA regista o executável original que aceita o sinalizador resolvido. Alterar um carácter seleccionado de `z` para `y` faz a primeira soma 1440 em vez de 1441, e o programa rejeita-a. | Entrada | Resultados observados | Código de saída | | --- | --- | --- | | Bandeira do Solver | `Correct!` | 0 | | Um caractere alterado | `Incorrect!` | 255 | Mostrar o sinalizador recuperado e a saída capturada REA \* saída original do programa ``` What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa} Correct! ``` O valor recuperado também corresponde ao sinalizador nos metadados do Desafio publicados pelos organizadores, verificados após a resolução do binário. Fonte, identidade do alvo e dados de análise Nova análise e duas capturas de processo em 8 de outubro de 2026, utilizando REA 4.1.0 com Ghidra 12.1.4 em Linux x64. O binário é um Elf x86-64 despojado, 15.248 bytes. Executável Original \* SHA-256 ``` dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae ``` As referências, funções e constantes das cadeias de caracteres foram inspecionadas antes da leitura da fonte ou solução dos organizadores. O solucionador Python e o diagrama foram construídos a partir desses resultados REA. [Compare com a fonte dos organizadores](https://github.com/DownUnderCTF/Challenges_2023_Public/blob/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/src/ms_flag_checker.c) · [Metadados do Desafio e sinalizador](https://github.com/DownUnderCTF/Challenges_2023_Public/blob/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/ctfcli.yaml) · [REA notas de prova](https://github.com/morluto/rea/blob/main/website/evidence/ctf-masked-squares.md) ## Experimente você mesmo Baixe o desafio original e o solucionador em uma pasta. Use o prompt acima para investigar com seu agente ou execute o script incluído. [Baixe o desafio original](https://raw.githubusercontent.com/DownUnderCTF/Challenges_2023_Public/b48f83db2984bc7fa2ec7879a32d7efb1be8d333/rev/masked-squares-flag-checker/publish/ms_flag_checker)[Baixar solver](https://rea.tools/showcase/ctf/solve.py) Terminal \* resolver e executar ``` 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 ``` O script imprime um sinalizador candidato; cole-o no prompt do programa. Resolvendo necessidades Python e `z3-solver`. A execução do executável original Precisa de Linux x86-64. [Configurar REA com o seu agente de codificação](https://rea.tools/get-started/)