Encontre a bandeira em
um binário CTF.

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.

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.

Leia a máscara e seu alvo a partir do binário

{"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

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.

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;
}

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.

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.

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.

What is the flag? DUCTF{ezzzpzzz_07bcda7bfe81faf43caa}
Correct!

dcd3bec4f608e11f3a12ce461100aaf5f621851ee63a1f870d7c90d4e3dd51ae

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.

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.