Nel contesto della malware analysis, il reverse engineering di cifrari personalizzati rappresenta una sfida: quando un algoritmo combina più livelli di permutazione, mescolamento delle chiavi e sostituzione, l’analisi manuale rallenta e diventa rapidamente più complessa e imprecisa.
Il nuovo studio del Malware Lab mostra come superare questo limite utilizzando Z3, un solver SMT sviluppato da Microsoft Research che invece di invertire manualmente il cifrario, modella la funzione in forma simbolica, lasciando al solver il compito di ricostruirne automaticamente l’inverso.
Partendo da un caso reale basato su una Substitution-Permutation Network del KALMAR CTF 2024, quest’analisi dimostra come la metodologia di Z3 sia direttamente applicabile anche all’analisi di loader, ransomware e packer.
Dopo aver introdotto i principi operativi di Z3, lo studio illustra uno script completo di risoluzione, approfondisce il tema degli indici simbolici e si conclude con un resoconto delle principali difficoltà incontrate nelle sue prime applicazioni.
Se desideri approfondire ecco il link al nostro studio completo.
Inoltre, puoi registrarti alla mailing list specifica Cyber Studios by T-Defence, per ricevere aggiornamenti sulle prossime ricerche:
