In this paper, we present a general strategy that enables the translation of tableau proofs using different Skolemization rules into machine-checkable proofs. It is part of a framework that enables (i) instantiation of the strategy into algorithms for different sets of tableau rules (e.g., different logics) and (ii) easy soundness proof which relies on the local extensibility of user-defined rules. Furthermore, we propose an instantiation of this strategy for first-order tableaux that handles notably pre-inner Skolemization rules, which is, as far as the authors know, the first one in the literature. This deskolemization strategy has been implemented in the Goéland [17] automated theorem prover, enabling an export of its proofs to Coq [8] and Lambdapi [2]. Finally, we have evaluated the algorithm performances for inner and pre-inner Skolemization rules through the certification of proofs from some categories of the TPTP [39] library.

Protecting software from illegal reverse engineering and malicious hackers is often remedied through either legal or technical means. In the technical domain, software obfuscation provides less than perfect protection against such attacks since there is no perfect obfuscator for all classes of programs. However, semantic preserving transformations can attempt to make the cost of attacks prohibitive in either time or resources. Software-based hardware abstraction (SBHA) is a novel approach that transforms traditional software code segments into a digital logic form and thus virtualizes code into a hardware abstraction. SBHA can be used to protect embedded secrets in programs that are used to guard intellectual property (IP). Secrets such as passwords, PINs, and activation codes authorize legitimate end-users to install or activate software for use and are validated typically through point functions that check for the single unique input that is expected. In this study we extend initial analysis of SBHA against state-of-the-art dynamic symbolic execution (DSE) attacks in recovering embedded program secrets and consider the limits of an attacker that recovers the logic circuit netlist from an SBHA-protected program. We pose four approaches for hardened SBHA configurations and evaluate their effectiveness using typical analysis tools that cover synthesis, binary decision diagram recovery, and symbolic analysis. We show that such attacks can be mitigated by these countermeasures outright and discuss the trade-off in size and overhead relative to the relatively low-cost of SBHA point-functions stand alone. We conclude that for single use operations such as point function checks, the overhead is large but the execution runtime delta is negligible.

Software companies typically embed one or more secrets in their programs to protect their intellectual property (IP) investment. These secrets are most often processed in code through evaluation of point functions, where only the correct password, PIN, or registration/activation code will authorize an end-user to legally install or use a product. Man-at-the-End (MATE) attacks can break assumptions of program security to find embedded secrets because they involve legitimate software owners who have complete access to the software and its execution environment. In this research, we present a novel approach to software MATE protection that leverages gate-level hardware representation, namely software-based hardware abstraction (SBHA). As a new proposed form of virtualization for software protection, SBHA demonstrates a light overhead - especially compared to much costlier traditional virtualization transformations, while completely defeating almost all symbolic execution-based attackers that were studied. Overall, SBHA bridges the gap between hardware and software protection, paving the way for future developments.

Inline assembly is still a common practice in low-level C programming, typically for efficiency reasons or for accessing specific hardware resources. Such embedded assembly codes in the GNU syntax (supported by major compilers such as GCC, Clang and ICC) have an interface specifying how the assembly codes interact with the C environment. For simplicity reasons, the compiler treats GNU inline assembly codes as blackboxes and relies only on their interface to correctly glue them into the compiled C code. Therefore, the adequacy between the assembly chunk and its interface (named compliance) is of primary importance, as such compliance issues can lead to subtle and hard-to-find bugs. We propose RUSTInA, the first automated technique for formally checking inline assembly compliance, with the extra ability to propose (proven) patches and (optimization) refinements in certain cases. RUSTInA is based on an original formalization of the inline assembly compliance problem together with novel dedicated algorithms. Our prototype has been evaluated on 202 Debian packages with inline assembly (2656 chunks), finding 2183 issues in 85 packages -- 986 significant issues in 54 packages (including major projects such as ffmpeg or ALSA), and proposing patches for 92% of them. Currently, 38 patches have already been accepted (solving 156 significant issues), with positive feedback from development teams.

The main goal of the artifact is to support the experimental claims of the paper #992 "Interface Compliance of Inline As-sembly: Automatically Check, Patch and Refine" by making both the prototype and data availableto the community. The expected result is the same output as the figures given in Table I and Table IV (appendix C) of the paper. In addition, we hope the released snapshot of our prototype is simple, documented and robust enough to have some uses for people dealing withinline assembly.

Code obfuscation aims at protecting Intellectual Property and other secrets embedded into software from being retrieved. Recent works leverage advances in artificial intelligence (AI) with the hope of getting blackbox deobfuscators completely immune to standard (whitebox) protection mechanisms. While promising, this new field of AI-based, and more specifically search-based blackbox deobfuscation, is still in its infancy. In this article we deepen the state of search-based blackbox deobfuscation in three key directions: understand the current state-of-the-art, improve over it and design dedicated protection mechanisms. In particular, we define a novel generic framework for search-based blackbox deobfuscation encompassing prior work and highlighting key components; we are the first to point out that the search space underlying code deobfuscation is too unstable for simulation-based methods (e.g., Monte Carlo Tree Search used in prior work) and advocate the use of robust methods such as S-metaheuristics; we propose the new optimized search-based blackbox deobfuscator Xyntia which significantly outperforms prior work in terms of success rate (especially with small time budget) while being completely immune to the most recent anti-analysis code obfuscation methods; and finally we propose two novel protections against search-based blackbox deobfuscation, allowing to counter Xyntia powerful attacks.

Code obfuscation aims at protecting Intellectual Property and other secrets embedded into software from being retrieved. Recent works leverage advances in artificial intelligence with the hope of getting blackbox deobfuscators completely immune to standard (whitebox) protection mechanisms. While promising, this new field of AI-based blackbox deobfuscation is still in its infancy. In this article we deepen the state of AI-based blackbox deobfuscation in three key directions: understand the current state-of-the-art, improve over it and design dedicated protection mechanisms. In particular, we define a novel generic framework for AI-based blackbox deobfuscation encompassing prior work and highlighting key components; we are the first to point out that the search space underlying code deobfuscation is too unstable for simulation-based methods (e.g., Monte Carlo Tres Search used in prior work) and advocate the use of robust methods such as S-metaheuritics; we propose the new optimized AI-based blackbox deobfuscator Xyntia which significantly outperforms prior work in terms of success rate (especially with small time budget) while being completely immune to the most recent anti-analysis code obfuscation methods; and finally we propose two novel protections against AI-based blackbox deobfuscation, allowing to counter Xyntia's powerful attacks.

This presentation is based on the paper "Search-based Local Blackbox Deobfuscation: Understand Improve and Mitigate'' from the same authors, which has been accepted for publication at ACM CCS 2021.

Code obfuscation aims at protecting Intellectual Property and other secrets embedded into software from being retrieved. Recent works leverage advances in artificial intelligence (AI) with the hope of getting blackbox deobfuscators completely immune to standard (whitebox) protection mechanisms. While promising, this new field of AI-based, and more specifically search-based blackbox deobfuscation, is still in its infancy. In this article we deepen the state of search-based blackbox deobfuscation in three key directions: understand the current state-of-the-art, improve over it and design dedicated protection mechanisms. In particular, we define a novel generic framework for search-based blackbox deobfuscation encompassing prior work and highlighting key components; we are the first to point out that the search space underlying code deobfuscation is too unstable for simulation-based methods (e.g., Monte Carlo Tree Search used in prior work) and advocate the use of robust methods such as S-metaheuristics; we propose the new optimized search-based blackbox deobfuscator Xyntia which significantly outperforms prior work in terms of success rate (especially with small time budget) while being completely immune to the most recent anti-analysis code obfuscation methods; and finally we propose two novel protections against search-based blackbox deobfuscation, allowing to counter Xyntia powerful attacks.

Directed fuzzing focuses on automatically testing specific parts of the code by taking advantage of additional information such as (partial) bug stack trace, patches or risky operations. Key applications include bug reproduction, patch testing and static analysis report verification. Although directed fuzzing has received a lot of attention recently, hard-to-detect vulnerabilities such as Use-After-Free (UAF) are still not well addressed, especially at the binary level. We propose UAFuzz, the first (binary-level) directed greybox fuzzer dedicated to UAF bugs. The technique features a fuzzing engine tailored to UAF specifics, a lightweight code instrumentation and an efficient bug triage step. Experimental evaluation for bug reproduction on real cases demonstrates that UAFuzz significantly outperforms state-of-the-art directed fuzzers in terms of fault detection rate, time to exposure and bug triaging. UAFuzz has also been proven effective in patch testing, leading to the discovery of 30 new bugs (7 CVEs) in programs such as Perl, GPAC and GNU Patch. Finally, we provide to the community a large fuzzing benchmark dedicated to UAF, built on both real codes and real bugs.

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.

Formal methods for software development have made great strides in the last two decades, to the point that their application in safety-critical embedded software is an undeniable success. Their extension to non-critical software is one of the notable forthcoming challenges. For example, C programmers regularly use inline assembly for low-level optimizations and system primitives. This usually results in rendering state-of-the-art formal analyzers developed for C ineffective. We thus propose TINA, the first automated, generic, verification-friendly and trustworthy lifting technique turning inline assembly into semantically equivalent C code amenable to verification, in order to take advantage of existing C analyzers. Extensive experiments on real-world code (including GMP and ffmpeg) show the feasibility and benefits of TINA.

Obfuscation is widely used to protect software against man-at-the-end attacks. Recent attacks based on semantic methods, especially dynamic symbolic execution (DSE), have proven extremely powerful against standard obfuscation techniques, leading several teams to investigate anti-DSE protections. Yet, the domain is in its infancy, and the current state of research on the topic is quite unclear. We propose a systematic review of anti-DSE techniques. In particular, we propose a classification and identify strengths and weaknesses of the current lines of research, as well as promising future directions.

Pretty-printing can be described as finding a good-looking solution to typeset data according to a set of formatting conventions. Oppen [6] pioneered the field with an algorithmic solution to pretty-printing, using the notions of boxes and break hints . The Format module is a direct descendant of this work: it is unfortunately often misunderstood or even misused. The first goal of this article is to enhance the available documentation about Format by explaining its basic and advanced features but also its relationship and differences with Oppen’s seminal work. The second goal is to investigate the links that Format has with the document-based pretty-printing tradition fostered by the lazy programming community [3,4,9,10]. ,

We focus in this paper on generating models of quantified first-order formulas over built-in theories, which is paramount in software verification and bug finding. While standard methods are either geared toward proving the absence of solution or targeted to specific theories, we propose a generic approach based on a reduction to the quantifier-free case. Our technique allows thus to reuse all the efficient machinery developed for that context. Experiments show a substantial improvement over state-of-the-art methods.

We prove the syntactic soundness of classical tableaux with free variables and on-the-fly Skolemization. Soundness proofs are usually built from semantic arguments, and this is to our knowledge, the first proof that appeals to syntactic means. We actually prove the soundness property with respect to cut-free sequent calculus. This requires great care because of the additional liberty in freshness checking allowed by the use of Skolem terms. In contrast to semantic soundness, we gain the possibility to state a cut elimination theorem for sequent calculus, under the proviso that completeness of the method holds. We believe that such techniques can be applied to tableaux in other logics as well.

We present b2llvm, a multi-platform code generator for the B-method. The b2llvm code generator currently handles the following elements of the B language: simple data types, imperative instructions and component compositions. In particular, this paper describes a translation for essential implementation constructs of the B language into LLVM source code, implemented into the b2llvm compiler. We use an example-based approach for this description.

We present SMTpp, a tool that operates both as a source-to-source transformer and analyzer for SMT-LIB. The first goal of SMTpp is to offer a framework to which developers of SMT solvers can delegate computing tasks that are both necessary to be competitive (at least on some families of benchmarks), and somehow irrelevant to the essence of SMT-solving. The second goal is to provide facilities to simplify and classify SMT-LIB benchmarks.

This paper describes two syntactic extensions to Smt-Lib scripts: lambda-expressions and polymorphism. After extending the syntax to allow these expressions, we show how to update the typing rules of the Smt-Lib to check the validity of these new terms and commands. Since most Smt-solvers only deal with many-sorted first-order formulas, we detail a monomorphization mechanism to allow to use polymorphism in Smt-Lib syntax while retaining a monomorphic solver core.