International audience

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 new method named Search Modulo Inference Rules (Smir that boosts search-based program synthesis while keeping its generality and flexibility. We instantiate Smir with inference rules for hard synthesis problems like arbitrary constant values and affine or polynomial relations over mixed boolean expressions, yielding the new black-box deobfuscation tool: XSmir. Experiments on obfuscated codes, real-world binaries, and synthetic benchmarks demonstrate that XSmir significantly outperforms prior black-box deobfuscators, synthesizing overall 76% and 84% of the expressions from our real-world obfuscated and non-obfuscated benchmarks where prior works recover 63% and 55%, together with 2 to 3 times less false positive and slightly improved compression rate.

The class of Basic Feasible Functionals BFF is the second-order counterpart of the class of first-order functions computable in polynomial time. We present several implicit characterizations of BFF based on a typed programming language of terms. These terms may perform calls to non-recursive imperative procedures. The type discipline has two layers: the terms follow a standard simply-typed discipline and the procedures follow a standard tier-based type discipline. BFF consists exactly of the second-order functionals that are computed by typable and terminating programs. The completeness of this characterization surprisingly still holds in the absence of lambda-abstraction. Moreover, the termination requirement can be specified as a completeness-preserving instance, which can be decided in time quadratic in the size of the program. As typing is decidable in polynomial time, we obtain the first tractable (i.e., decidable in polynomial time), sound, complete, and implicit characterization of BFF, thus solving a problem opened for more than 20 years.

In automated complexity analysis, noninterference-based type systems statically guarantee, via soundness, the property that well-typed programs compute functions of a given complexity class, e.g., the class FP of functions computable in polynomial time. These characterizations are also extensionally complete - they capture all functions - but are not intensionally complete as some polytime algorithms are rejected. This impact on expressive power is an unavoidable cost of achieving a tractable characterization. To circumvent this issue, an avenue arising from security applications is to find a relaxation of noninterference based on a declassification mechanism that allows critical data to be released in a safe and controlled manner. Following this path, we present a new and intuitive declassification policy preserving FP-soundness and capturing strictly more programs than existing noninterference-based systems. We show the versatility of the approach: it also provides a new characterization of the class BFF of second-order polynomial time computable functions in a second-order imperative language, with first-order procedure calls. Type inference is tractable: it can be done in polynomial time.

We consider the problem of program clone search, i.e. given a target program and a repository of known programs (all in executable format), the goal is to find the program in the repository most similar to the target program -- with potential applications in terms of reverse engineering, program clustering, malware lineage and software theft detection. Recent years have witnessed a blooming in code similarity techniques, yet most of them focus on function-level similarity and function clone search, while we are interested in program-level similarity and program clone search. Actually, our study shows that prior similarity approaches are either too slow to handle large program repositories, or not precise enough, or yet not robust against slight variations introduced by compilers, source code versions or light obfuscations. We propose a novel spectral analysis method for program-level similarity and program clone search called Programs Spectral Similarity (PSS). In a nutshell, PSS one-time spectral feature extraction is tailored for large repositories, making it a perfect fit for program clone search. We have compared the different approaches with extensive benchmarks, showing that PSS reaches a sweet spot in terms of precision, speed and robustness.

Abstract The class of Basic Feasible Functionals $$\mathtt{BFF}$$ BFF is the second-order counterpart of the class of first-order functions computable in polynomial time. We present several implicit characterizations of $$\mathtt{BFF}$$ BFF based on a typed programming language of terms. These terms may perform calls to imperative procedures, which are not recursive. The type discipline has two layers: the terms follow a standard simply-typed discipline and the procedures follow a standard tier-based type discipline. $$\mathtt{BFF}$$ BFF consists exactly of the second-order functionals that are computed by typable and terminating programs. The completeness of this characterization surprisingly still holds in the absence of lambda-abstraction. Moreover, the termination requirement can be specified as a completeness-preserving instance, which can be decided in time quadratic in the size of the program. As typing is decidable in polynomial time, we obtain the first tractable (i.e., decidable in polynomial time), sound, complete, and implicit characterization of $$\mathtt{BFF}$$ BFF , thus solving a problem opened for more than 20 years.

The class of Basic Feasible Functionals BFF$_2$ is the type-2 counterpart of the class FP of type-1 functions computable in polynomial time. Several characterizations have been suggested in the literature, but none of these present a programming language with a type system guaranteeing this complexity bound. We give a characterization of BFF$_2$ based on an imperative language with oracle calls using a tier-based type system whose inference is decidable. Such a characterization should make it possible to link higher-order complexity with programming theory. The low complexity (cubic in the size of the program) of the type inference algorithm contrasts with the intractability of the aforementioned methods and does not overly constrain the expressive power of the language.

We consider the problem of recovering the compiling chain used to generate a given stripped binary code. We present a Graph Neural Network framework at the binary level to solve this problem, with the idea to take into account the shallow semantics provided by the binary code's structured control flow graph (CFG). We introduce a Graph Neural Network, called Site Neural Network (SNN), dedicated to this problem. To attain scalability at the binary level, feature extraction is simplified by forgetting almost everything in a CFG except transfer control instructions and performing a parametric graph reduction. Our experiments show that our method recovers the compiler family with a very high F1-Score of 0.9950 while the optimization level is recovered with a moderately high F1-Score of 0.7517. On the compiler version prediction task, the F1-Score is about 0.8167 excluding the clang family. A comparison with a previous work demonstrates the accuracy and performance of this framework.

The class of Basic Feasible Functionals BFF2 is the type-2 counterpart of the class FP of type-1 functions computable in polynomial time. Several characterizations have been suggested in the literature, but none of these present a programming language with a type system guaranteeing this complexity bound. We give a characterization of BFF2 based on an imperative language with oracle calls using a tier-based type system whose inference is decidable. Such a characterization should make it possible to link higher-order complexity with programming theory. The low complexity (cubic in the size of the program) of the type inference algorithm contrasts with the intractability of the aforementioned methods and does not restrain strongly the expressive power of the language.

Abstract Recurrence can be used as a function definition schema for any nontrivial free algebra, yielding the same computational complexity in all cases. We show that primitive-recursive computing is in fact independent of free algebras altogether, and can be characterized by a generic programming principle, namely the control of iteration by the depletion of finite components of the underlying structure.

Code obfuscation is a major tool for protecting software intellectual property from attacks such as reverse engineering or code tampering. Yet, recently proposed (automated) attacks based on Dynamic Symbolic Execution (DSE) shows very promising results, hence threatening software integrity. Current defenses are not fully satisfactory, being either not efficient against symbolic reasoning, or affecting runtime performance too much, or being too easy to spot. We present and study a new class of anti-DSE protections coined as path-oriented protections targeting the weakest spot of DSE, namely path exploration. We propose a lightweight, efficient, resistant and analytically proved class of obfuscation algorithms designed to hinder DSE-based attacks. Extensive evaluation demonstrates that these approaches critically counter symbolic deobfuscation while yielding only a very slight overhead.

Binary packing, encoding binary code prior to execution and decoding them at run time, is the most common obfuscation adopted by malware authors to camouflage malicious code. Especially, most packers recover the original code by going through a set of "written-then-executed" layers, which renders determining the end of the unpacking increasingly difficult. Many generic binary unpacking approaches have been proposed to extract packed binaries without the prior knowledge of packers. However, the high runtime overhead and lack of anti-analysis resistance have severely limited their adoptions. Over the past two decades, packed malware is always a veritable challenge to anti-malware landscape. This paper revisits the long-standing binary unpacking problem from a new angle: packers consistently obfuscate the standard use of API calls. Our in-depth study on an enormous variety of Windows malware packers at present leads to a common property: malware's Import Address Table (IAT), which acts as a lookup table for dynamically linked API calls, is typically erased by packers for further obfuscation; and then unpacking routine, like a custom dynamic loader, will reconstruct IAT before original code resumes execution. During a packed malware execution, if an API is invoked through looking up a rebuilt IAT, it indicates that the original payload has been restored. This insight motivates us to design an efficient unpacking approach, called BinUnpack. Compared to the previous methods that suffer from multiple "written-then-executed" unpacking layers, BinUnpack is free from tedious memory access monitoring, and therefore it introduces very small runtime overhead. To defeat a variety of ever-evolving evasion tricks, we design BinUnpack's API monitor module via a novel kernel-level DLL hijacking technique. We have evaluated BinUnpack's efficacy extensively with more than 238K packed malware and multiple Windows utilities. BinUnpack's success rate is significantly better than that of existing tools with several orders of magnitude performance boost. Our study demonstrates that BinUnpack can be applied to speeding up large-scale malware analysis.

Software deobfuscation is a crucial activity in security analysis and especially in malware analysis. While standard static and dynamic approaches suffer from well-known shortcomings, Dynamic Symbolic Execution (DSE) has recently been proposed as an interesting alternative, more robust than static analysis and more complete than dynamic analysis. Yet, DSE addresses only certain kinds of questions encountered by a reverser, namely feasibility questions. Many issues arising during reverse, e.g., detecting protection schemes such as opaque predicates, fall into the category of infeasibility questions. We present Backward-Bounded DSE, a generic, precise, efficient and robust method for solving infeasibility questions. We demonstrate the benefit of the method for opaque predicates and call stack tampering, and give some insight for its usage for some other protection schemes. Especially, the technique has successfully been used on state-of-the-art packers as well as on the government-grade X-Tunnel malware - allowing its entire deobfuscation. Backward-Bounded DSE does not supersede existing DSE approaches, but rather complements them by addressing infeasibility questions in a scalable and precise manner. Following this line, we propose sparse disassembly, a combination of Backward-Bounded DSE and static disassembly able to enlarge dynamic disassembly in a guaranteed way, hence getting the best of dynamic and static disassembly. This work paves the way for robust, efficient and precise disassembly tools for heavily-obfuscated binaries.

Symbolic Execution (SE) is a popular and profitable approach to automatic code-based software testing. Concretization and symbolization (C/S) is a crucial part of modern SE tools, since it directly impacts the trade-offs between correctness, completeness and efficiency of the approach. Yet, C/S policies have been barely studied. We intend to remedy to this situation and to establish C/S policies on a firm ground. To this end, we propose a clear separation of concerns between C/S specification on one side, through the new rule-based description language CSml, and the algorithmic core of SE on the other side, revisited to take C/S policies into account. This view is implemented on top of an existing SE tool, demonstrating the feasibility and the benefits of the method. This work paves the way for more flexible SE tools with well-documented and reusable C/S policies, as well as for a systematic study of C/S policies.

When it comes to software analysis, several approaches exist from heuristic techniques to formal methods, which are helpful at solving different kinds ofproblems. Unfortunately very few initiative seek to aggregate this techniques in the same platform. BINSEC intend to fulfill this lack of binary analysis platform by allowing to perform modular analysis. This work focusses on BINSEC/SE, the new dynamic symbolic execution engine (DSE) implemented in BINSEC. We will highlight the novelties of the engine, especially in terms of interactions between concrete and symbolic execution or optimization of formula generation. Finally, two reverse engineering applications are shown in order to emphasize the tool effectiveness.

Fighting malware involves analyzing large numbers of suspicious binary files. In this context, disassembly is a crucial task in malware analysis and reverse engineering. It involves the recovery of assembly instructions from binary machine code. Correct disassembly of binaries is necessary to produce a higher level representation of the code and thus allow the analysis to develop high-level understanding of its behavior and purpose. Nonetheless, it can be problematic in the case of malicious code, as malware writers often employ techniques to thwart correct disassembly by standard tools. In this paper, we focus on the disassembly of x86 self-modifying binaries with overlapping instructions. Current state-of-the-art disassemblers fail to interpret these two common forms of obfuscation, causing an incorrect disassembly of large parts of the input. We introduce a novel disassembly method, called concatic disassembly, that combines CONCrete path execution with stATIC disassembly. We have developed a standalone disassembler called CoDisasm that implements this approach.

In software testing, coverage criteria specify the requirements to be covered by the test cases. However, in practice such criteria are limited due to the well-known infeasibility problem, which concerns elements/requirements that cannot be covered by any test case. To deal with this issue we revisit and improve state-of-the-art static analysis techniques, such as Value Analysis and Weakest Precondition calculus. We propose a lightweight greybox scheme for combining these two techniques in a complementary way. In particular we focus on detecting infeasible test requirements in an automatic and sound way for condition coverage, multiple condition coverage and weak mutation testing criteria. Experimental results show that our method is capable of detecting almost all the infeasible test requirements, 95% on average, in a reasonable amount of time, i.e., less than 40 seconds, making it practical for unit testing.

Analyzing cryptographic implementations has important applications, especially for malware analysis where they are an integral part both of the malware payload and the unpacking code that decrypts this payload. These implementations are often based on well-known cryptographic functions, whose description is publicly available. While potentially very useful for malware analysis, the identification of such cryptographic primitives is made difficult by the fact that they are usually obfuscated. Current state-of-the-art identification tools are ineffective due to the absence of easily identifiable static features in obfuscated code. However, these implementations still maintain the input-output (I/O) relationship of the original function. In this paper, we present a tool that leverages this fact to identify cryptographic functions in obfuscated programs, by retrieving their I/O parameters in an implementation-independent fashion, and comparing them with those of known cryptographic functions. In experimental evaluation, we successfully identified the cryptographic functions TEA, RC4, AES and MD5 both in synthetic examples protected by a commercial-grade packer (AsProtect), and in several obfuscated malware samples (Sality, Waledac, Storm Worm and SilentBanker). In addition, our tool was able to recognize basic operations done in asymmetric ciphers such as RSA.

We present a type system for an extension of lambda calculus with a conditional construction, named STA B , that characterizes the PSPACE class. This system is obtained by extending STA, a type assignment for lambda-calculus inspired by Lafont’s Soft Linear Logic and characterizing the PTIME class. We extend STA by means of a ground type and terms for Booleans and conditional. The key issue in the design of the type system is to manage the contexts in the rule for conditional in an additive way. Thanks to this rule, we are able to program polynomial time Alternating Turing Machines. From the well-known result APTIME = PSPACE, it follows that STA B is complete for PSPACE. Conversely, inspired by the simulation of Alternating Turing machines by means of Deterministic Turing machine, we introduce a call-by-name evaluation machine with two memory devices in order to evaluate programs in polynomial space. As far as we know, this is the first characterization of PSPACE that is based on lambda calculus and light logics.

We propose a type system for an imperative programming language, which certifies program time bounds. This type system is based on secure flow information analysis. Each program variable has a level and we prevent information from flowing from low level to higher level variables. We also introduce a downgrading mechanism in order to delineate a broader class of programs. Thus, we propose a relation between security-typed language and implicit computational complexity. We establish a characterization of the class of polynomial time functions.

Botnets constitute a serious security problem. A lot of effort has been invested towards understanding them better, while developing and learning how to deploy effective counter-measures against them. Their study via various analysis, modelling and experimental methods are integral parts of the development cycle of any such botnet mitigation schemes. It also constitutes a vital part of the process of understanding present threats and predicting future ones. Currently, the most popular of these techniques are botnet studies, where researchers interact directly with real-world botnets. This approach is less than ideal, for many reasons that we discuss this paper, including scientific validity, ethical and legal issues. Consequently, we present an alternative approach employing in the lab experiments involving at-scale emulated botnets. We discuss the advantages of such an approach over reverse engineering, analytical modelling, simulation and in-the-wild studies. Moreover, we discuss the requirements that facilities supporting them must have. We then describe an experiment which we emulated a 3000-node, fully-featured version of the Waledac botnet, complete with an emulated command and control (C&C) infrastructure. By observing the load characteristics and yield (rate of spamming) of such a botnet, we can draw interesting conclusions about its real-world operations and design decisions made by its creators. Furthermore, we conducted experiments with sybil attacks launched against it and verified their viability. However, we were able to determine that mounting such attacks is not so simple: high resource consumption can cause havoc and partially neutralise them. Finally, we were able to repeat the attacks with varying parameters, an attempt to optimise them. The merits of this experimental approach is underlined since by the fact that it would have been difficult to obtain these results by other methods.

The STACS conference of March 4-6, 2010, held in Nancy, is the 27th in this series. The STACS 2010 call for papers led to over 238 submissions from 40 countries. Each paper was assigned to three program committee members. The committee selected 54 papers during a two-week electronic meeting held in November.

Table of contents

Formal specifications and reasoning techniques in software modelling are needed to ensure the correctness of the system at the design phase. Event-B is a formal method with support tools that allows the stepwise development of reactive systems. Such systems include multi-agent systems as a subclass. In this paper, we propose an approach to specify capabilities of a number of software agents. We then verify whether these capabilities help the agents to accomplish a certain task using a supported tool for Event-B. We use the binary numeral system as a case study to illustrate our approach.

The interest in STACS has remained at a high level over the past years. The STACS 2009 call for papers led to over 280 submissions from 41 countries. Each paper was assigned to three program committee members. The program committee held a two-week electronic meeting at the beginning of November and selected 54 papers. As co-chairs of the program committee, we would like to sincerely thank its members and the many external referees for their valuable work. The overall very high quality of the submissions made the selection a difficult task. We would like to express our thanks to the three invited speakers, Monika Henzinger, Jean-Eric Pin and Nicole Schweikardt, for their contributions to the proceedings. Special thanks are due to A. Voronkov for his EasyChair software (www.easychair.org). Moreover we would like to thank Sonja Lauer for preparing the conference proceedings and continuous help throughout the conference organization. For the second time this year's STACS proceedings are published in electronic form. A printed version was also available at the conference, with ISBN 978-3-939897-09-5. The electronic proceedings are available through several portals, and in particular through HAL and DROPS. HAL is an electronic repository managed by several French research agencies, and DROPS is the Dagstuhl Research Online Publication Server. We want to thank both these servers for hosting the proceedings of STACS and guaranteeing them perennial availability. The rights on the articles in the proceedings are kept with the authors and the papers are available freely, under a Creative Commons license (seewww.stacs-conf.org/faq.html for more details).

No abstract available.

The sup-interpretation method is proposed as a new tool to control memory resources of first order functional programs with pattern matching by static analysis. It has been introduced in order to increase the intensionality, that is the number of captured algorithms, of a previous method, the quasi-interpretations. Basically, a sup-interpretation provides an upper bound on the size of function outputs. A criterion, which can be applied to terminating as well as nonterminating programs, is developed in order to bound the stack frame size polynomially. Since this work is related to quasi-interpretation, dependency pairs, and size-change principle methods, we compare these notions obtaining several results. The first result is that, given any program, we have heuristics for finding a sup-interpretation when we consider polynomials of bounded degree. Another result consists in the characterizations of the sets of functions computable in polynomial time and in polynomial space. A last result consists in applications of sup-interpretations to the dependency pair and the size-change principle methods.

A sup-interpretation is a tool which provides upper bounds on the size of the values computed by the function symbols of a program. Sup-interpretations have shown their interest to deal with the complexity of first order functional programs. This paper is an attempt to adapt the framework of sup-interpretations to a fragment of object-oriented programs, including loop and while constructs and methods with side effects. We give a criterion, called brotherly criterion, which uses the notion of sup-interpretation to ensure that each brotherly program computes objects whose size is polynomially bounded by the inputs sizes. Moreover we give some heuristics in order to compute the sup-interpretation of a given method.

We propose a characterization of PSPACE by means of atype assignment for an extension of lambda calculus with a conditional construction. The type assignment STAB is an extension of STA, a type assignment for lambda-calculus inspired by Lafont's Soft Linear Logic.

In this paper, we study characterizations of polynomial complexity classes using first order functional programs and we try to improve their intensionality, that is the number of natural algorithms captured. We use polynomial assignments over the reals. The polynomial assignments used are inspired by the notions of quasiinterpretation and sup-interpretation, and are decidable when considering polynomials of bounded degree ranging over real numbers. Contrarily to quasi-interpretations, the considered assignments are not required to have the subterm property. Consequently, they capture a strictly larger number of natural algorithms (including quotient, gcd, duplicate elimination from a list) than previous characterizations using quasi-interpretations

We provide several machine-independent characterizations of deterministic complexity classes in the model of computation proposed by L. Blum, M. Shub and S. Smale. We provide a characterization of partial recursive functions over any arbitrary structure. We show that polynomial time over an arbitrary structure can be characterized in terms of safe recursion. We show that polynomial parallel time over an arbitrary structure can be characterized in terms of safe recursion with substitutions.

We study the effect of polynomial interpretation termination proofs of deterministic (resp. non-deterministic) algorithms defined by con uent (resp. non-con uent) rewrite systems over data structures which include strings, lists and trees, and we classify them according to the interpretations of the constructors. This leads to the definition of six function classes which turn out to be exactly the deterministic (resp. non-deterministic) polynomial time, linear exponential time and linear doubly exponential time computable functions when the class is based on con uent (resp. non-con uent) rewrite systems. We also obtain a characterisation of the linear space computable functions. Finally, we demonstrate that functions with exponential interpretation termination proofs are super-elementary.