SearcharxivSearch

arXiv subjects

Jean-Yves Marion

Publications and source records attributed to Jean-Yves Marion.

17 recordsLinked to original sources

Inside Crypter-as-a-Service: An Ecosystem Analysis of the exploit.in Underground Forum Research Talks

Crypter-as-a-Service (CraaS) has become a key enabling layer of the contemporary malware economy by providing on-demand evasion capabilities through underground service markets. In this paper, we present a longitudinal characterization of the CraaS ecosystem on exploit.in, a major Russian-language cybercrime forum with a presence on both the clear web and the dark web. From a collection of approximately 1,000,000 posts, we combine keyword filtering, LLM-assisted annotation, and manual validation to extract a corpus of 491 threads and 2,949 posts spanning January 2020 to August 2025. Our analysis shows that crypters on exploit.in are not merely sold as static tools, but as continuously maintained operational services whose value depends on recurring stub renewal - sometimes on a daily basis - sustained antivirus evasion, and trust-based delivery. We develop a taxonomy of five seller types and four buyer profiles, and map the buyer-seller correspondences that structure market transactions. We further document pricing models ranging from low-cost per-build Telegram bot services to high-end custom development and salaried recruitment. Using social-network analysis, we find that the market is hierarchically structured around a small core of highly central actors, many of whom appear to function as trust brokers or other influential intermediaries, while its stability relies on a broader trust and governance infrastructure including escrow, guarantors, reputation systems, and security deposits. Finally, we discuss differences between the CraaS model observed on exploit.in and that reported on HackForums. Although both forums share similar service logics, our corpus suggests that exploit.in exhibits a more professionalized and service-oriented CraaS configuration.

cs.CY

Attacking the First-Principle: A Black-Box, Query-Free Targeted Mimicry Attack on Binary Function Classifiers

Binary function classifiers play a crucial role in maintaining the security and integrity of software systems by detecting malicious code and unauthorized modifications. However, machine learning-based classifiers are vulnerable to adversarial attacks that can evade detection. In this study, we present Kelpie, a novel framework for executing mimicry attacks, a stronger type of targeted evasion attacks, on binary function classifiers in a black-box, zero-query setting. Unlike previous approaches that rely on querying the target classifier to refine untargeted evasion attacks, Kelpie leverages code transformations that preserve the functionality of malicious payloads while causing them to be misclassified as we want. Through extensive experimentation, we demonstrate that Kelpie can successfully execute mimicry attacks against six state-of-the-art binary function classifiers representing different model architectures without requiring direct interaction with them. We further validate our approach with a practical demonstration, involving a keylogger and a wiper concealed within benign-looking functions embedded in an application. This work, to our best knowledge, is the first to demonstrate such a mimicry attack in a black-box, zero-query context, raising important questions about the reliability and security of existing machine learning-based binary function classifiers.

cs.LG

Complete and tractable machine-independent characterizations of second-order polytime

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.

cs.LO

Declassification Policy for Program Complexity Analysis

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 overcome 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.

cs.LO

Scalable Program Clone Search Through Spectral Analysis

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.

cs.CR

A tier-based typed programming language characterizing Feasible Functionals

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.

cs.LO

How to Kill Symbolic Deobfuscation for Free; or Unleashing the Potential of Path-Oriented Protections

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.

cs.CR

Implicit complexity via structure transformation

Implicit computational complexity, which aims at characterizing complexity classes by machine-independent means, has traditionally been based, on the one hand, on programs and deductive formalisms for free algebras, and on the other hand on descriptive tools for finite structures. We consider here "uninterpreted" programs for the transformation of finite structures, which define functions over a free algebra A once the elements of A are themselves considered as finite structures. We thus bridge the gap between the two approaches above to implicit complexity, with the potential of streamlining and clarifying important tools and techniques, such as set-existence and ramification. We illustrate this potential by delineating a broad class of programs, based on the notion of loop variant familiar from imperative program construction, that characterizes a generic notion of primitive-recursive complexity, without reference to any data-driven recurrence.

cs.LO

Targeting Infeasibility Questions on Obfuscated Codes

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 has an interesting alternative, more robust than static analysis and more complete than dynamic analysis. Yet, DSE addresses 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. In this article, we present the 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.

cs.CR

Analysis and Diversion of Duqu's Driver

The propagation techniques and the payload of Duqu have been closely studied over the past year and it has been said that Duqu shared functionalities with Stuxnet. We focused on the driver used by Duqu during the infection, our contribution consists in reverse-engineering the driver: we rebuilt its source code and analyzed the mechanisms it uses to execute the payload while avoiding detection. Then we diverted the driver into a defensive version capable of detecting injections in Windows binaries, thus preventing further attacks. We specifically show how Duqu's modified driver would have detected Duqu.

cs.CR

Complexity Information Flow in a Multi-threaded Imperative Language

We propose a type system to analyze the time consumed by multi-threaded imperative programs with a shared global memory, which delineates a class of safe multi-threaded programs. We demonstrate that a safe multi-threaded program runs in polynomial time if (i) it is strongly terminating wrt a non-deterministic scheduling policy or (ii) it terminates wrt a deterministic and quiet scheduling policy. As a consequence, we also characterize the set of polynomial time functions. The type system presented is based on the fundamental notion of data tiering, which is central in implicit computational complexity. It regulates the information flow in a computation. This aspect is interesting in that the type system bears a resemblance to typed based information flow analysis and notions of non-interference. As far as we know, this is the first characterization by a type system of polynomial time multi-threaded programs.

cs.CC

Proceedings Second Workshop on Developments in Implicit Computational Complexity

This volume contains the proceedings of the Second International Workshop on Developments in Implicit Computational complExity (DICE 2011), which took place on April 2-3 2011 in Saarbruecken, Germany, as a satellite event of the Joint European Conference on Theory and Practice of Software, ETAPS 2011. Implicit Computational Complexity aims at studying computational complexity without referring to external measuring conditions or particular machine models, but instead by considering restrictions on programming languages or logical principles implying complexity properties. The aim of this workshop was to bring together researchers working on implicit computational complexity, from its logical and semantics aspects to those related to the static analysis of programs, so as to foster their interaction and to give newcomers an overview of the current trends in this area. The first DICE workshop was held in 2010 at ETAPS and published in EPTCS, volume 23 (http://eptcs.org/content.cgi?DICE2010).

cs.LO

An Implicit Characterization of PSPACE

We present a type system for an extension of lambda calculus with a conditional construction, named STAB, 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 STAB 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.

cs.LO

On tiered small jump operators

Predicative analysis of recursion schema is a method to characterize complexity classes like the class FPTIME of polynomial time computable functions. This analysis comes from the works of Bellantoni and Cook, and Leivant by data tiering. Here, we refine predicative analysis by using a ramified Ackermann's construction of a non-primitive recursive function. We obtain a hierarchy of functions which characterizes exactly functions, which are computed in O(n^k) time over register machine model of computation. For this, we introduce a strict ramification principle. Then, we show how to diagonalize in order to obtain an exponential function and to jump outside deterministic polynomial time. Lastly, we suggest a dependent typed lambda-calculus to represent this construction.

cs.CC

On the defence notion

'Trojan horses', 'logic bombs', 'armoured viruses' and 'cryptovirology' are terms recalling war gears. In fact, concepts of attack and defence drive the world of computer virology, which looks like a war universe in an information society. This war has several shapes, from invasions of a network by worms, to military and industrial espionage ...

cs.CR

Resource control of object-oriented programs

A sup-interpretation is a tool which provides an upper bound on the size of a value computed by some symbol of a program. Sup-interpretations have shown their interest to deal with the complexity of first order functional programs. For instance, they allow to characterize all the functions bitwise computable in Alogtime. This paper is an attempt to adapt the framework of sup-interpretations to a fragment of oriented-object programs, including distinct encodings of numbers through the use of constructor symbols, loop and while constructs and non recursive methods with side effects. We give a criterion, called brotherly criterion, which ensures that each brotherly program computes objects whose size is polynomially bounded by the inputs sizes.

cs.PL

Quasi-friendly sup-interpretations

In a previous paper, the sup-interpretation method was proposed as a new tool to control memory resources of first order functional programs with pattern matching by static analysis. Basically, a sup-interpretation provides an upper bound on the size of function outputs. In this former work, a criterion, which can be applied to terminating as well as non-terminating programs, was developed in order to bound polynomially the stack frame size. In this paper, we suggest a new criterion which captures more algorithms computing values polynomially bounded in the size of the inputs. Since this work is related to quasi-interpretations, we compare the two notions obtaining two main features. The first one is that, given a program, we have heuristics for finding a sup-interpretation when we consider polynomials of bounded degree. The other one consists in the characterizations of the set of function computable in polynomial time and in polynomial space.

cs.CC