Optimizing symbolic execution for malware behavior classification. Issue 93 (June 2020)

• Record Type: Journal Article
• Authors: Sebastio, Stefano; Baranov, Eduard; Biondi, Fabrizio; Decourbe, Olivier; Given-Wilson, Thomas; Legay, Axel; Puodzius, Cassius; Quilbeuf, Jean
• Is Part Of: Computers & security. Issue 93(2020)
• Publication Date: 2020-06
• Subjects: Malware classification -- Empirical studies -- SMT solving -- Behavior graphs -- Symbolic execution; Computer security -- Periodicals; Electronic data processing departments -- Security measures -- Periodicals; 005.805
• DOI: 10.1016/j.cose.2020.101775
• Languages: English
• ISSNs: 0167-4048

Abstract

Highlights: Improving effective symbolic execution state exploration. Optimization of SMT solving for binary execution and malware. Improving behavioral representation of binary program signatures. Behavioral graph-based signatures for effective multi-class malware classification. Optimizing whole toolchains and understanding their relations holistically. Abstract: Increasingly software correctness, reliability, and security is being analyzed using tools that combine various formal and heuristic approaches. Often such analysis becomes expensive in terms of time and at the cost of high quality results. In this experience report we explore the tuning and optimization of the tools underlying binary malware detection and classification. We identify heuristics and SMT solver tactics for the effective symbolic execution of binary files. We combine these with effective heuristics for the construction of behavioral signatures of programs that can be used for a supervised learning multi-class malware classifier. Further, a set of experiments following the full-factorial design allowed us to identify the correlations between heuristics and the overall performance of the classifier.