Sommaire

Introduction

Voici le writeup d’un challenge de reverse engineering / speedrun du FCSC 2025. Ce challenge simule une machine virtuelle personnalisée exécutant un microcode qui vérifie la validité d’une entrée.

Description du challenge

Vous nous aviez dit que vous connaissiez le secret. Si cela est bien le cas alors il n'y aura aucun problème. Sinon...

Analyse initiale

Informations sur le binaire

On nous donne un exécutable Windows 64 bits :

file polygraph.exe;
polygraph.exe: PE32+ executable (console) x86-64, for MS Windows

Le binaire est un PE32+ partiellement strippé.

Points d’entrée clés

  • Le programme lit l’entrée utilisateur via gets_s(input, 0x11), limitant ainsi l’entrée à 16 octets maximum.
gets_s(input,0x11);
  • Initialisation d’un tableau global de registres à zéro :
_registers_start = ZEXT816(0);
_DAT_140005f70 = 0;
  • Interprétation d’un microcode composé de 773 instructions, chacune codée sur 3 octets :
microcode_size = 0x305;
do {
opcode = microcode[-1];
	if (opcode == 0xb) {
	  uVar1 = *(uint *)(&registers_start + (ulonglong)microcode[1] * 4);
	LAB_140001286:
	  *(uint *)(&registers_start + (ulonglong)*microcode * 4) =
		   *(int *)(&registers_start + (ulonglong)*microcode * 4) + uVar1;
	}
	else if (opcode == 0x16) {
	  *(int *)(&registers_start + (ulonglong)*microcode * 4) =
		   *(int *)(&registers_start + (ulonglong)*microcode * 4) -
		   *(int *)(&registers_start + (ulonglong)microcode[1] * 4);
	}
	else if (opcode == 0x2c) {
	  *(int *)(&registers_start + (ulonglong)*microcode * 4) =
		   *(int *)(&registers_start + (ulonglong)*microcode * 4) << (microcode[1] & 0x1f);
	}
	else if (opcode == 0x37) {
	  *(uint *)(&registers_start + (ulonglong)*microcode * 4) =
		   *(uint *)(&registers_start + (ulonglong)*microcode * 4) >> (microcode[1] & 0x1f);
	}
	else if (opcode == 0x42) {
	  *(int *)(&registers_start + (ulonglong)*microcode * 4) =
		   *(int *)(&registers_start + (ulonglong)*microcode * 4) *
		   *(int *)(&registers_start + (ulonglong)microcode[1] * 4);
	}
	else if (opcode == 0x4d) {
	  *(uint *)(&registers_start + (ulonglong)*microcode * 4) =
		   *(uint *)(&registers_start + (ulonglong)*microcode * 4) |
		   *(uint *)(&registers_start + (ulonglong)microcode[1] * 4);
	}
	else if (opcode == 0x58) {
	  *(uint *)(&registers_start + (ulonglong)*microcode * 4) = (uint)(byte)input[microcode[1]];
	}
	else if (opcode == 99) {
	  uVar1 = (uint)microcode[1];
	  goto LAB_140001286;
	}
	microcode = microcode + 3;
	microcode_size = microcode_size + -1;
} while (microcode_size != 0);
  • Vérification et affichage du flag :
if (_registers_start == 0) {
		iVar2 = sha256_hash(input);
		if (iVar2 == 0) {
		  puts("Something went wrong.");
		  goto LAB_14000131d;
		}
		custom_print("You\'re honest.\nFCSC{");
		do {
		  custom_print(&DAT_140003300,flag_buffer[microcode_size]);
		  microcode_size = microcode_size + 1;
	} while (microcode_size < 0x20);
	_Str = "}";
}

Reverse engineering de la VM

Structure du microcode

Chaque instruction est un triplet (opcode, dst, src) de 3 octets. Le compteur microcode_size commence à 0x305 (773 en décimal) et est décrémenté à chaque itération, tandis que le pointeur microcode avance de 3 octets à chaque instruction.

Cela nous donne la taille totale du microcode : 773 * 3 = 2319 octets.

Registres et accès mémoire

Le programme utilise une zone mémoire pour stocker les registres. _registers_start est un pointeur vers le début de cette zone. Tous les registres sont initialisés à zéro avant l’exécution du microcode.

Jeu d’instructions

Opcode Nom Équivalent en C
0x0B ADD R[dst] = (R[dst] + R[src]) mod 2^32
0x16 SUB R[dst] = (R[dst] - R[src]) mod 2^32
0x2C SHL R[dst] <<= (src & 0x1F)
0x37 SHR R[dst] = R[dst] >> (src & 0x1F)
0x42 MUL R[dst] = (R[dst] * R[src]) mod 2^32
0x4D OR R[dst] = R[dst] OR R[src]
0x58 MOVB R[dst] = (uint8_t)input[src] (zero-extend)
0x63 ADDI R[dst] = (R[dst] + imm8) mod 2^32

Les opérations mod 2^32 indiquent que nous travaillons avec des uint32_t qui subissent un wrap-around, tronquant tout dépassement.

Modélisation et résolution symbolique

Choix de l’approche

Pour résoudre ce challenge, nous utiliserons Z3, un solveur SMT, afin de raisonner sur les opérations effectuées par la VM :

  • 16 BitVec(8) pour représenter les octets de la clé d’entrée (16 octets max)
  • N BitVec(32) pour les registres, où N est le nombre maximum de registres utilisés
  • Contrainte finale : R0 == 0 après exécution de toutes les instructions

Pour déterminer le nombre de registres nécessaires, nous pouvons utiliser ce script :

import struct
code = open('microcode.bin','rb').read()
it = struct.iter_unpack('<BBB', code)
max_idx = 0
for op, dst, src in it:
    max_idx = max(max_idx, dst, src)
num_registers = max_idx + 1
print(num_registers)

Ce script nous donne 254 comme index maximum, donc nous avons besoin de 255 registres (0 à 254).

Construction du solveur

troplaflemme

Pour gagner du temps, j’ai utilisé un émulateur partiellement généré par ChatGPT :

#!/usr/bin/env python3
import sys, pathlib, struct, z3, importlib

UINT32 = 32
NB_REG = 256

class VMZ3:
    def __init__(self, code: bytes):
        if len(code) % 3:
            raise ValueError("Le micro-code doit être un multiple de 3 octets")

        self.code   = code
        self.key    = [z3.BitVec(f"k{i}", 8) for i in range(16)]
        self.reg    = [z3.BitVec(f"r{i}", UINT32) for i in range(NB_REG)]
        self.solver = z3.Solver()
        self._build_constraints()

    # ---------------- VM operations ---------------- #
    def _wrap32(self, expr):
        return z3.Extract(31, 0, expr)

    def _ADD (self, d, s): self.reg[d] = self._wrap32(self.reg[d] + self.reg[s])
    def _SUB (self, d, s): self.reg[d] = self._wrap32(self.reg[d] - self.reg[s])
    def _SHL (self, d, imm): self.reg[d] = self._wrap32(self.reg[d] << imm)
    def _SHR (self, d, imm): self.reg[d] = z3.LShR(self.reg[d], imm)
    def _MUL (self, d, s): self.reg[d] = self._wrap32(self.reg[d] * self.reg[s])
    def _OR  (self, d, s): self.reg[d] = self.reg[d] | self.reg[s]
    def _MOVB(self, d, idx): self.reg[d] = z3.ZeroExt(24, self.key[idx & 0x0F])
    def _ADDI(self, d, imm): self.reg[d] = self._wrap32(self.reg[d] + imm)


    # ---------------- Build full trace ------------- #
    def _build_constraints(self):
        it = struct.iter_unpack("<BBB", self.code)
        for op, dst, src in it:
            if   op == 0x0B: self._ADD(dst, src)
            elif op == 0x16: self._SUB(dst, src)
            elif op == 0x2C: self._SHL(dst, src & 0x1F)
            elif op == 0x37: self._SHR(dst, src & 0x1F)
            elif op == 0x42: self._MUL(dst, src)
            elif op == 0x4D: self._OR (dst, src)
            elif op == 0x58: self._MOVB(dst, src)
            elif op == 0x63: self._ADDI(dst, src)
            else:
                raise ValueError(f"Opcode inconnu 0x{op:02X}")

        # condition finale r0 == 0
        self.solver.add(self.reg[0] == 0)



    def solve(self):
        if self.solver.check() != z3.sat:
            raise RuntimeError("Aucune clé trouvée")
        model = self.solver.model()
        return bytes(model.evaluate(k).as_long() for k in self.key)

def main():
    if len(sys.argv) < 2:
        sys.exit(1)

    code = pathlib.Path(sys.argv[1]).read_bytes()

    vm  = VMZ3(code)
    key = vm.solve()
    print("Clé trouvée (hex) :", key.hex())

if __name__ == "__main__":
    main()

Ce script nous donne une clé qui, après traitement par le microcode, satisfait la condition R0 == 0.

2025-04-27-212429_798x347_scrot.png

Génération du flag final

Normalement, exécuter le programme avec la clé trouvée devrait fonctionner. Cependant, comme je travaille sous Linux avec Wine, ça ne fonctionne pas. J’ai donc décidé de reproduire la fonction sha256_hash pour calculer le flag :

import binascii
import hashlib

key = binascii.unhexlify("2ab857a5fbe0a867bfd8abebf1e9c831")
digest = hashlib.sha256(key).hexdigest()

print("FCSC{%s}" % digest)

2025-04-27-213034_714x474_scrot.png

Conclusion

Ce challenge était particulièrement intéressant et instructif. J’ai pu approfondir mes connaissances en reverse engineering et en résolution symbolique. Je pense en revanche qu’il aurait mérité une étoile supplémentaire pour la difficulté à produire un émulateur fonctionnel.

memequandmeme

back to top