Malware analysis represents a difficult task due to its ever-changing nature, where attackers invent new techniques for avoiding or counter-attacking analysis and prevention mechanisms. During fast-response investigations, a vital element is extracting or checking information, in order to take proper action. One key aspect that is currently missing, in a general sense, is a system which security researchers can query in order to obtain a quick verdict about the capabilities of a malware. The proposed solution is a framework for formal analysis of applications’ behavior, called Formal Tainting-Based Framework, that uses a combination of binary instrumentation, taint analysis, and runtime verification in order to selectively extract behavioral properties of a malware. These are then formalized in order to check if the application expresses certain capabilities. The formal aspect also represents a significant contribution, as we introduce a specific temporal logic, which overcomes obstacles for expressing program events. The findings are accompanied by a concrete implementation, which proved effective and efficient against real-life malware, as highlighted by an evaluation. Furthermore, the framework has been evaluated in realistic cyber forensics scenarios, demonstrating its potential to assist security researchers by reducing analysis time and effort.

Malware analysis is a demanding task regarding techniques, time and creativity. On multiple occasions, however, security researchers are interested in checking if the analyzed threat possesses specific capabilities, disregarding the overall picture. In this paper, we combine our malware expertise with the results of a Large Language Model, in order to expand the knowledge and creativity in generating specific rules that encode these capabilities. The rules, along with malicious applications, are then used as inputs for a malware analysis framework created by us, in order to determine if the application has those specific capabilities. The findings show promising results, sustained by synthetic and real-life experiments.

Malware attacks are a significant part of the new software security threats detected each year. Intel Software Guard Extensions (SGX) are a set of hardware instructions introduced by Intel in their recent lines of processors that are intended to provide a secure execution environment for user-developed applications. To our knowledge, there was no serious attempt yet to overcome the SGX protection by exploiting the weaknesses in the software supply chain infrastructure, namely at the level of the development, build or signing servers. While SGX protection does not specifically take into consideration such threats, we show in the current paper that a simple malware attack exploiting a separation between the build and signing processes can have a serious damaging impact, practically nullifying SGX integrity protection measures. We also explore two possible mitigations against the attack, one centralized leveraging SGX itself, and one distributed that relies on a smart contract deployed on a blockchain infrastructure. Our evaluation shows that both methods are feasible in practice and their added costs are acceptable for the offered protection.

Malware attacks represent a significant part of today's security threats. Software guard extensions (SGX) are a set of hardware instructions introduced by Intel in their recent lines of processors that are intended to provide a secure execution environment for user-developed applications. To our knowledge, there was no serious attempt yet to overcome the SGX protection by leveraging the software supply chain infrastructure, such as weaknesses in the development, build or signing servers. While SGX protection does not specifically take into consideration such threats, we show in the current paper that a simple malware attack exploiting a separation between the build and signing processes can have a serious damaging impact, practically nullifying the SGX integrity protection measures. Finally, we also suggest some possible mitigations against the attack.