Effectiveness of Synthesis in Concolic Deobfuscation

Abstract : Control flow obfuscation techniques can be used to hinder software reverse-engineering. Symbolic analysis can counteract these techniques, but only if they can analyze obfuscated conditional statements. We evaluate the use of dynamic synthesis to complement symbolic analysis in the analysis of obfuscated conditionals. We test this approach on the taint-analysis-resistant Mixed Boolean Arithmetics (MBA) obfuscation method that is commonly used to obfuscate and randomly diversify statements. We experimentally ascertain the practical feasibility of MBA obfuscation. We study using SMT-based approaches with different state-of-the-art SMT solvers to counteract MBA obfuscation, and we show how targeted algebraic simplification can greatly reduce the analysis time. We show that synthesis-based deobfuscation is more effective than current SMT-based deobfuscation algorithms, thus proposing a synthesis-based attacker model to complement existing attacker models.
Type de document :
Article dans une revue
Computers and Security, Elsevier, 2017, 70, pp.500-515. 〈10.1016/j.cose.2017.07.006〉
Liste complète des métadonnées

Littérature citée [49 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01241356
Contributeur : Fabrizio Biondi <>
Soumis le : dimanche 5 novembre 2017 - 22:19:39
Dernière modification le : mercredi 16 mai 2018 - 11:24:14
Document(s) archivé(s) le : mardi 6 février 2018 - 12:27:43

Fichier

cosemain.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Fabrizio Biondi, Sébastien Josse, Axel Legay, Thomas Sirvent. Effectiveness of Synthesis in Concolic Deobfuscation. Computers and Security, Elsevier, 2017, 70, pp.500-515. 〈10.1016/j.cose.2017.07.006〉. 〈hal-01241356v2〉

Partager

Métriques

Consultations de la notice

335

Téléchargements de fichiers

1808