From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 911757FA5E for ; Tue, 25 Apr 2017 10:14:06 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=sebastien.bardin@cea.fr; spf=Pass smtp.mailfrom=sebastien.bardin@cea.fr; spf=None smtp.helo=postmaster@oxalide-smtp-out.extra.cea.fr Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of sebastien.bardin@cea.fr) identity=pra; client-ip=132.168.224.13; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="sebastien.bardin@cea.fr"; x-sender="sebastien.bardin@cea.fr"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of sebastien.bardin@cea.fr designates 132.168.224.13 as permitted sender) identity=mailfrom; client-ip=132.168.224.13; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="sebastien.bardin@cea.fr"; x-sender="sebastien.bardin@cea.fr"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@oxalide-smtp-out.extra.cea.fr) identity=helo; client-ip=132.168.224.13; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="sebastien.bardin@cea.fr"; x-sender="postmaster@oxalide-smtp-out.extra.cea.fr"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AblSBLRbdimEj3Pjwc7fSriT/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZoMu7bnLW6fgltlLVR4KTs6sC0LuK9fi4EUU7or+5+EgYd5JNUxJXwe?= =?us-ascii?q?43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRp?= =?us-ascii?q?OOv1BpTSj8Oq3Oyu5pHfeQtFiT6ybL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+?= =?us-ascii?q?RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPC?= =?us-ascii?q?TQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD?= =?us-ascii?q?0fOjA57W/XhNJ+gqFVrh2vqBNwwZLbbo6OOfpifa7QZ88WSXZPU8tTUSFKH4Oy?= =?us-ascii?q?b5EID+oEJetYtJfyqEAUohulGQmsBf3gyjlVjXDtx6I6yfkuEQDA3Ac9GN8Oq2?= =?us-ascii?q?rbo87vO6cJTeC1zbfHzTPZY/xNwzj98pXHchEnofyXQb1/b9DexVMhFwPfl1id?= =?us-ascii?q?r5HuMTCN1ukVrmSW4fRsWfiyh2MmqAx9uCajytkjh4XTm44YxEjI+Th3zYorP9?= =?us-ascii?q?G0VU92bN++HJdNsyyWKZF6T8IkTmp1oig10KcGtoS+fCUSyJQo2Rrfa/uffoiP?= =?us-ascii?q?7RPsTuKRITZli317Yb6/nBOy8VS4yuHlUcm0zUpKojBbndjDqnANzQbc5tKbRf?= =?us-ascii?q?Rj5EitwziP1xrL5uFFJ0A7i7bbJoY8zrM+iJYfq1nPEy71lUnskqOaaEop9vK1?= =?us-ascii?q?5+npernmo4WTN45wigHwKKQuncm/DPwjMgcQRGeU4/+81KHi/ULnRrVGlOY5nb?= =?us-ascii?q?PDsJ/HJMQboLW0DBNL3Yk58Rq/AS2m3MwCnXYbNFJFZA6Hj4/xNl7SOv/4CPO/?= =?us-ascii?q?j02okDdq3PDGIqbsAo7NL3jGiLfuZ6xx609ayAopzNBQ/YhYCr8bIKG7Zkikv9?= =?us-ascii?q?XdClo9Mheo6+fhEtR0kI0ECkyVBarMK67YuESU5+8pa+OFfoMUvn6pMPUv7uXy?= =?us-ascii?q?jHI/31UUZ6Wo27McZXn+EO4wcBbRWmblntpUSTRChQE5VuG/0FA=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0ClAQC9BP9Yhw3gqIRbGgEBAQECAQEBA?= =?us-ascii?q?QgBAQEBFQEBAQECAQEBAQgBAQEBhRaDIUaLCKhtgm6DNgKEG0MUAQEBAQEBAQE?= =?us-ascii?q?BAQESAQEBCgsJCCgvgjMggkMDAwwXDwE1BAQGEwkUCAImAgJJDhMGAgEBihiNX?= =?us-ascii?q?51egiaLHQELJoELhUiCCIpLgl8FiTqUB3CXT4U8hmKPcIQpNoEnZ1WEaRAMGYF?= =?us-ascii?q?Mc4k2AQEB?= X-IPAS-Result: =?us-ascii?q?A0ClAQC9BP9Yhw3gqIRbGgEBAQECAQEBAQgBAQEBFQEBAQE?= =?us-ascii?q?CAQEBAQgBAQEBhRaDIUaLCKhtgm6DNgKEG0MUAQEBAQEBAQEBAQESAQEBCgsJC?= =?us-ascii?q?CgvgjMggkMDAwwXDwE1BAQGEwkUCAImAgJJDhMGAgEBihiNX51egiaLHQELJoE?= =?us-ascii?q?LhUiCCIpLgl8FiTqUB3CXT4U8hmKPcIQpNoEnZ1WEaRAMGYFMc4k2AQEB?= X-IronPort-AV: E=Sophos;i="5.37,248,1488841200"; d="scan'208";a="221416217" Received: from oxalide-smtp-out.extra.cea.fr ([132.168.224.13]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 25 Apr 2017 10:14:05 +0200 Received: from pisaure.intra.cea.fr (pisaure.intra.cea.fr [132.166.88.21]) by oxalide-sys.extra.cea.fr (8.14.7/8.14.7/CEAnet-Internet-out-4.0) with ESMTP id v3P8E4js167274 for ; Tue, 25 Apr 2017 10:14:04 +0200 Received: from pisaure.intra.cea.fr (localhost [127.0.0.1]) by localhost (Postfix) with SMTP id B9C6120A483 for ; Tue, 25 Apr 2017 10:14:04 +0200 (CEST) Received: from muguet1.intra.cea.fr (muguet1.intra.cea.fr [132.166.192.6]) by pisaure.intra.cea.fr (Postfix) with ESMTP id B047820A3EF for ; Tue, 25 Apr 2017 10:14:04 +0200 (CEST) Received: from [10.8.33.166] (is148220.intra.cea.fr [10.8.33.166]) by muguet1.intra.cea.fr (8.15.2/8.15.2/CEAnet-Intranet-out-1.4) with ESMTP id v3P8E4Id004518 for ; Tue, 25 Apr 2017 10:14:04 +0200 From: sebastien bardin References: To: caml-list@inria.fr Message-ID: Date: Tue, 25 Apr 2017 10:14:05 +0200 User-Agent: Mozilla/5.0 (X11; Linux i686; rv:45.0) Gecko/20100101 Thunderbird/45.8.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: 8bit X-Validation-by: sebastien.bardin@cea.fr Subject: [Caml-list] =?UTF-8?Q?=5Bsujet_de_th=C3=A8se=5D_d=C3=A9obfuscatio?= =?UTF-8?Q?n_et_analyse_de_malware_=28CEA-LORIA=2C_deadline_15_mai=29?= Le CEA Saclay propose un sujet de thèse sur l'utilisation des méthodes formelles pour l'analyse de malware et de programmes obfusqués, en co-encadrement avec le LORIA (Jean-Yves Marion). deadline : 15 mai contact : sebastien.bardin@cea.fr ------------------------------------------------ titre : Symbolic execution for deobfuscation, and application to malware analysis - mots-clés: reverse, déobfuscation, malware, désassembage, méthodes formelles, exécution symbolique - bourse DGA-CEA, co-encadrement CEA-Université de Lorraine - lieu : CEA (Paris-Saclay), avec visites au LORIA (Nancy) - encadrants : Sébastien Bardin (CEA), Jean-Yves Marion (LORIA, directeur de thèse) - démarrage en octobre 2017 - deadline pour répondre : 15 mai - contact, plus d'information : sebastien.bardin@cea.fr sujet ----- La sécurité logicielle est un problème majeur de la société de l'information, les conséquences d'un système non sécurisé pouvant affecter aussi bien des individus (phishing, paiement non autorisé, etc.) que des compagnies (fuite d'informations confidentielles) ou des états (attaques cybernétiques, virus stuxnet). Un des vecteurs d'attaque les plus privilégiés est l'utilisation de codes malveillants (malware), tels que les virus ou les vers [2]. La contre-mesure classique consiste à détecter le malware par des techniques de signature syntaxique [2] puis à l'éradiquer. Cependant cette approche est très simple à contourner en utilisant des méthodes d'obfuscation (modification automatique d'un programme pour en altérer la forme sans modifier son comportement) [3]. La recherche en matière de détection de malware s'oriente actuellement vers des notions de signatures "sémantiques" plus robustes, voir par exemple les travaux menés au Laboratoire de Haute Sécurité (LHS) du LORIA [1]. Cependant, à cause de l'obfuscation, la signature calculée ne prend en compte qu'une partie du programme malveillant, ce qui entraîne des pertes de précision en termes de détection. D'un autre côté, des progrès récents ont été obtenus au Laboratoire de Sécurité Logicielle (LSL) du CEA LIST dans le domaine de l'analyse automatique de code binaire. Ainsi la plate-forme open-source BINSEC [5] fournit une représentation intermédiaire multi-plateforme et différentes analyses sémantiques, permettant notamment l'exploration partielle des comportements du code exécutable ou encore la reconstruction du Graphe de Flot de Contrôle (CFG) d'un programme (non protégé) donné sous forme exécutable. Nos premiers travaux, en collaboration CEA-LORIA, ont déjà permis l'ajout d'un moteur puissant d'exploration des chemins d'un malware [5] (via *exécution symbolique*), ainsi qu'une première étude de l'utilisation de l'exécution symbolique pour aider à la déobfuscation -- notamment via la détection de "prédicats opaques" [6,7]. Le but de ce sujet de thèse est de consolider ces premiers résultats, en explorant de manière systématique l'utilisation de l'exécution symbolique pour la déobfuscation et la reconnaissance de malware. Le candidat devra notamment : 1. Etudier comment reconstruire des approximations fidèles du CFG de codes exécutables obfusqués, en étendant et/ou combinant les techniques actuelles d'analyse de code binaire. C'est la tâche principale de la thèse. Le candidat devra notamment considérer un spectre large des principales obfuscations de code rencontrées en pratique (automodification, virtualisation, etc.). D'un point de vue technique, la combinaison de techniques d'exécution symbolique, de tracing dynamique (disponible au LORIA) et d'analyse statique niveau binaire (également disponible dans BINSEC) est une piste prometteuse pour attaquer les codes protégés, continuant les efforts déjà entrepris [6,4]. 2. Etudier comment connecter ces résultats peuvent se combiner avec les techniques de reconnaissance sémantique de malware du LORIA [1], et en évaluer le gain. Au-delà du bénéfice d'un désassemblage plus précis, on pourra par exemple étudier comment les techniques symboliques d'analyse de binaire [6,7] peuvent être utilisées directement pour calculer des éléments pertinents de signature sémantique, complétant les approches déjà proposées [1]. ---- Références [1] Bonfante, G., Kaczmarek, M., Marion, J.-Y. : Architecture of a morphological malware detector. In : Journal in Computer Virology (2009) [2] Filiol, É. : Les virus informatiques : théorie, pratique et applications. Springer (2004) [3] Moser, A., Kruegel, C., Kirda, E. : Limits of Static Analysis for Malware Detection. In: Annual Computer Security Applications Conference (ACSAC 2007) [4] Bonfante, G., Fernandez, J. M., Marion, J.-Y., Rouxel, B., Sabatier, F., Thierry, A.: CoDisasm: Medium Scale Concatic Disassembly of Self-Modifying Binaries with Overlapping Instructions. In: ACM Conference on Computer and Communications Security (CCS 2015) [5] David, R., Bardin, S., Ta, T. D., Feist, J., Mounier, L., Potet, M.-L., Marion, J.-Y.: BINSEC/SE : A Dynamic Symbolic Execution Toolkit for Binary-level Analysis. In: IEEE International Conference on Software Analysis, Evolution, and Reengineering (SANER 2016) [6] S. Bardin, R. David, JY Marion. Backward-bounded DSE: Targeting Infeasibility Questions on Obfuscated Codes. In: IEEE Symposium on Security & Privacy (S&P 2017) [7] R. David, S. Bardin. Code Deobfuscation: Intertwining Dynamic, Static and Symbolic Approaches. In: Black Hat Europe 2016