Today's security threats are characterized by effective dissemination mechanisms (e.g., droppers, drive-by download), malicious mobile apps, and targeted attacks. The large amount of malware samples are often mutations and porting of known families (also to mobile platforms). Malicious mobile apps are difficult to analyze because they do not show their full malicious behavior if not properly stimulated. Modern malware attempts to evade both dynamic and static approaches, with anti-debugging, obfuscation and metamorphism techniques. In these cases, a semantic approach to hybrid (dynamic and static) analysis techniques would lead to a more precise understanding of the malware behavior and, therefore, to the development of more effective detection mechanisms. Indeed, formal approaches to program analysis are a promising research direction, although their application to malware is still quite poor. Uniform reasoning on malware is also hard because of the lack of naming and classification conventions. As a result, a uniform and formal roadmap that can be followed to mitigate modern malware is still missing.

We believe that semantics-based formal approaches for modeling and reasoning on the evolving behavior of metamorphic malware will provide a significant contribution to both research community and industry. The main challenge is the isolation of the common malicious behavior shared across the metamorphic variants. FACE will leverage formal approaches for modeling 1) the common malicious behaviors and 2) the execution environment (e.g., target system, sandbox), so to account for environment-sensitive malware. Throughout our approach we consider also naming inconsistencies.

We aim at modeling differences and invariants between metamorphic or ported malware variants. To this end, we plan to disassemble such variants and apply abstraction techniques to obtain a semantic model of the differences. To model the invariants, we design new abstract-interpretation-based domains for analyzing code properties and for extracting metamorphic signatures; to this end we will leverage also the analysis of (mutated) malware samples across multiple anti-malware tools. For malware-environment interplay analysis we plan to develop an high-order theory of noninterference to study the dependencies among programs.

The novelty of FACE consists in the 1) malware-environment analysis, which requires new theoretical studies for lifting the noninterference theory high order, 2) application of abstract-interpretation and semantics-based approaches to metamorphic malware modeling, and 3) new techniques to trigger the malicious behavior of mobile apps.

We will design tools that implement our theoretical approach for 1) extracting metamorphic signatures, 2) analyzing differences, 3) model malware-environment interplay, and 4) increase code coverage of dynamic analysis of mobile malicious apps.