FormaliSE 2024
Fri 12 - Sun 21 April 2024 Lisbon, Portugal
co-located with ICSE 2024
Mon 15 Apr 2024 14:00 - 14:30 at Eugénio de Andrade - Machine learning and formal methods Chair(s): Stefania Gnesi

Malware, or software designed with harmful intent, is an ever-evolving threat that can have drastic effects on both individuals and institutions. Neural network malware classification systems are key tools for combating these threats but are vulnerable to adversarial machine learning attacks. These attacks perturb input data to cause misclassification, bypassing these protective systems. Existing defenses often rely on enhancing the training process, thereby increasing the model’s robustness to these perturbations, which is quantified using verification. While training improvements are necessary, we propose focusing on the verification process used to evaluate improvements to training. As such, we present a case study that evaluates a novel verification domain that will help to ensure tangible safeguards against adversaries and provide a more reliable means of evaluating the robustness and effectiveness of anti-malware systems. To do so, we describe malware classification and two types of common malware datasets (feature and image datasets), demonstrate the certified robustness accuracy of malware classifiers using the Neural Network Verification (NNV) and Neural Network Enumeration (nnenum) tools, and outline the challenges and future considerations necessary for the improvement and refinement of the verification of malware classification. By evaluating this novel domain as a case study, we hope to increase its visibility, encourage further research and scrutiny, and ultimately enhance the resilience of digital systems against malicious attacks.

Mon 15 Apr

Displayed time zone: Lisbon change

14:00 - 15:30
Machine learning and formal methodsFormaliSE 2024 at Eugénio de Andrade
Chair(s): Stefania Gnesi Istituto di Scienza e Tecnologie dell'Informazione "Alessandro Faedo"
14:00
30m
Talk
Case Study: Neural Network Malware Detection Verification for Feature and Image Datasets
FormaliSE 2024
Preston K. Robinette Vanderbilt University, Diego Manzanas Lopez Vanderbilt University, Serena Serbinowska Vanderbilt University, Kevin Leach Vanderbilt University, Taylor T Johnson Vanderbilt University
Pre-print
14:30
30m
Talk
Leveraging Large Language Models to Boost Dafny’s Developers Productivity
FormaliSE 2024
Álvaro F. Silva Independent Researcher, Alexandra Mendes University of Porto and HASLab, INESC TEC, João F. Ferreira INESC-ID and IST, University of Lisbon
15:00
10m
Day closing
Closing
FormaliSE 2024