Dans le cadre de notre séminaire « La Cybersécurité sur un plateau » (Cybersecurity on a Plate), nous aurons 2 présentations le mardi 09 septembre prochain. Le séminaire CoaP aura lieu à 10h30 dans le bâtiment IMT/TP/TSP, en salle 3.A213.

Si vous venez participer pour la première fois, n'hésitez pas à contacter les organisateurs pour ne pas être bloqué à l'entrée.

Guillaume Scerri (ENS Paris-Saclay): Capturing new cryptographic proofs techniques using logic: extensions to the computationally complete symbolic attacker

Abstract: When proving cryptographic protocols, one has to deal with a malicious attacker. In particular this means that it is crucial to carefully capture attacker capabilities. This is best done by reducing security of protocols to known hard problems. However these cryptographic reductions can be quite complex and when done by hand such reductions can be rather hard to check. In recent years there has been a push to capture such reductions using logics that can be checked using (dedicated) proof assistants. In this talk we explore the intricacies of capturing complex cryptographic reductions in one of these logics the Computationally Complete Symbolic Attacker logic. We will focus on two main techniques: hybrid arguments and rewinding, and show how they can be applied to proofs of new protocols, namely e-voting mixnets.

Vidal Attias (CEA): Augmenting Search-based Program Synthesis with Local Inference Rules to Improve Black-box Deobfuscation

Abstract: Code obfuscation aims to protect programs from reverse engineering, with applications ranging from intellectual property protection to malware hardening. Recent works on black-box analyses propose to leverage program synthesis in order to infer the semantics of highly obfuscated code blocks. Being fully black-box, these approaches are immune to syntactic complexity and can thus bypass standard obfuscation mechanisms. Yet, they are restricted by their synthesis capabilities and can only be applied to semantically simple code blocks. It explains why they have mainly been used on virtual machine handlers, where behaviors are usually simple enough. Applying black-box deobfuscation at scale beyond virtualization is still an open problem, notably because black-box methods cannot synthesize complex behaviors involving, for example, arbitrary constant values or affine or polynomial relations over mixed-boolean-arithmetic expressions. In this article, we show how to combine search-based program synthesis with local inference rules, resulting in a black-box method named Search Modulo Inference Rules (Smir) which allows boosting the capabilities of search-based program synthesis while keeping its generality and flexibility.

We instantiate our method with inference rules dedicated to hard synthesis problems like arbitrary constant values and affine or polynomial relations over mixed boolean expressions, yielding a new black-box deobfuscation tool named XSmir. Experiments demonstrate that XSmir significantly outperforms prior black-box deobfuscators.