-
Fine-Grained Static Detection of Obfuscation Transforms Using Ensemble-Learning and Semantic Reasoning
Authors:
Ramtine Tofighi-Shirazi,
Irina Mariuca Asavoae,
Philippe Elbaz-Vincent
Abstract:
The ability to efficiently detect the software protections used is at a prime to facilitate the selection and application of adequate deob-fuscation techniques. We present a novel approach that combines semantic reasoning techniques with ensemble learning classification for the purpose of providing a static detection framework for obfuscation transformations. By contrast to existing work, we provi…
▽ More
The ability to efficiently detect the software protections used is at a prime to facilitate the selection and application of adequate deob-fuscation techniques. We present a novel approach that combines semantic reasoning techniques with ensemble learning classification for the purpose of providing a static detection framework for obfuscation transformations. By contrast to existing work, we provide a methodology that can detect multiple layers of obfuscation, without depending on knowledge of the underlying functionality of the training-set used. We also extend our work to detect constructions of obfuscation transformations, thus providing a fine-grained methodology. To that end, we provide several studies for the best practices of the use of machine learning techniques for a scalable and efficient model. According to our experimental results and evaluations on obfuscators such as Tigress and OLLVM, our models have up to 91% accuracy on state-of-the-art obfuscation transformations. Our overall accuracies for their constructions are up to 100%.
△ Less
Submitted 18 November, 2019;
originally announced November 2019.
-
Context-Updates Analysis and Refinement in Chisel
Authors:
Irina Mariuca Asavoae,
Mihail Asavoae,
Adrian Riesco
Abstract:
This paper presents the context-updates synthesis component of Chisel--a tool that synthesizes a program slicer directly from a given algebraic specification of a programming language operational semantics. (By context-updates we understand programming language constructs such as goto instructions or function calls.) The context-updates synthesis follows two directions: an overapproximating phase…
▽ More
This paper presents the context-updates synthesis component of Chisel--a tool that synthesizes a program slicer directly from a given algebraic specification of a programming language operational semantics. (By context-updates we understand programming language constructs such as goto instructions or function calls.) The context-updates synthesis follows two directions: an overapproximating phase that extracts a set of potential context-update constructs and an underapproximating phase that refines the results of the first step by testing the behaviour of the context-updates constructs produced at the previous phase. We use two experimental semantics that cover two types of language paradigms: high-level imperative and low-level assembly languages and we conduct the tests on standard benchmarks used in avionics.
△ Less
Submitted 20 September, 2017;
originally announced September 2017.
-
Software Model Checking: A Promising Approach to Verify Mobile App Security
Authors:
Irina Mariuca Asavoae,
Hoang Nga Nguyen,
Markus Roggenbach,
Siraj Ahmed Shaikh
Abstract:
In this position paper we advocate software model checking as a technique suitable for security analysis of mobile apps. Our recommendation is based on promising results that we achieved on analysing app collusion in the context of the Android operating system. Broadly speaking, app collusion appears when, in performing a threat, several apps are working together, i.e., they exchange information w…
▽ More
In this position paper we advocate software model checking as a technique suitable for security analysis of mobile apps. Our recommendation is based on promising results that we achieved on analysing app collusion in the context of the Android operating system. Broadly speaking, app collusion appears when, in performing a threat, several apps are working together, i.e., they exchange information which they could not obtain on their own. In this context, we developed the Kandroid tool, which provides an encoding of the Android/Smali code semantics within the K framework. Kandroid allows for software model checking of Android APK files. Though our experience so far is limited to collusion, we believe the approach to be applicable to further security properties as well as other mobile operating systems.
△ Less
Submitted 15 June, 2017;
originally announced June 2017.
-
Towards Automated Android App Collusion Detection
Authors:
Irina Mariuca Asavoae,
Jorge Blasco,
Thomas M. Chen,
Harsha Kumara Kalutarage,
Igor Muttik,
Hoang Nga Nguyen,
Markus Roggenbach,
Siraj Ahmed Shaikh
Abstract:
Android OS supports multiple communication methods between apps. This opens the possibility to carry out threats in a collaborative fashion, c.f. the Soundcomber example from 2011. In this paper we provide a concise definition of collusion and report on a number of automated detection approaches, developed in co-operation with Intel Security.
Android OS supports multiple communication methods between apps. This opens the possibility to carry out threats in a collaborative fashion, c.f. the Soundcomber example from 2011. In this paper we provide a concise definition of collusion and report on a number of automated detection approaches, developed in co-operation with Intel Security.
△ Less
Submitted 7 March, 2016;
originally announced March 2016.
-
Interacting via the Heap in the Presence of Recursion
Authors:
Jurriaan Rot,
Irina Măriuca Asăvoae,
Frank de Boer,
Marcello M. Bonsangue,
Dorel Lucanu
Abstract:
Almost all modern imperative programming languages include operations for dynamically manipulating the heap, for example by allocating and deallocating objects, and by updating reference fields. In the presence of recursive procedures and local variables the interactions of a program with the heap can become rather complex, as an unbounded number of objects can be allocated either on the call…
▽ More
Almost all modern imperative programming languages include operations for dynamically manipulating the heap, for example by allocating and deallocating objects, and by updating reference fields. In the presence of recursive procedures and local variables the interactions of a program with the heap can become rather complex, as an unbounded number of objects can be allocated either on the call stack using local variables, or, anonymously, on the heap using reference fields. As such a static analysis is, in general, undecidable.
In this paper we study the verification of recursive programs with unbounded allocation of objects, in a simple imperative language for heap manipulation. We present an improved semantics for this language, using an abstraction that is precise. For any program with a bounded visible heap, meaning that the number of objects reachable from variables at any point of execution is bounded, this abstraction is a finitary representation of its behaviour, even though an unbounded number of objects can appear in the state. As a consequence, for such programs model checking is decidable.
Finally we introduce a specification language for temporal properties of the heap, and discuss model checking these properties against heap-manipulating programs.
△ Less
Submitted 16 December, 2012;
originally announced December 2012.
