Springer Verlag Publishers – Catastrophic Cyber-Physical Malware
Abstract: With the advent of highly sophisticated cyber-physical malware (CPM) such as Industroyer, a cyberattack could be as destructive as the terrorist attack on 9/11, it would virtually paralyze the nation. We discuss as the major risks the vulnerability of: telecommunication infrastructure, industrial control systems (ICS), and mission-critical software. In differentiating CPM from traditional malware, […]
ICSE 2018 – COMB: Computing Relevant Program Behaviors
Abstract: The paper presents COMB, a tool to improve accuracy and efficiency of software engineering tasks that hinge on computing all relevant program behaviors. Computing all behaviors and selecting the relevant ones is computationally intractable. COMB uses Projected Control Graph (PCG) abstraction to derive the relevant behaviors directly and efficiently. The PCG is important as […]
2017 Winter Simulation Conference – Modeling Lessons from Verifying Large Software Systems for Safety and Security
Abstract: Verifying software in mission-critical Cyber-Physical Systems (CPS) is an important but daunting task with challenges of accuracy and scalability. This paper discusses lessons learned from verifying properties of the Linux kernel. These lessons have raised questions about traditional verification approaches, and have led us to a model-based approach for software verification. These models are […]
VizSec 2017 – Interactive Visualization Toolbox to Detect Sophisticated Android Malware
Abstract: Detecting zero-day sophisticated malware is like searching for a needle in the haystack, not knowing what the needle looks like. This paper describes Android Malicious Flow Visualization Toolbox that empowers a human analyst to detect such malware. Detecting sophisticated malware requires systematic exploration of the code to identify potentially malignant code, conceiving plausible malware […]
ICSE 2016 – Let’s Verify Linux: Accelerated Learning of Analytical Reasoning through Automation and Collaboration
Abstract: We describe our experiences in the classroom using the internet to collaboratively verify a significant safety and security property across the entire Linux kernel. With 66,609 instances to check across three versions of Linux, the naive approach of simply dividing up the code and assigning it to students does not scale, and does little […]
ICPC 2016 – Human-Machine Resolution of Invisible Control Flow
Abstract: Invisible Control Flow (ICF) results from dynamic binding and asynchronous processing. For modern software replete with ICF, the ability to analyze and resolve ICF is crucial for verifying software. A fully automated analysis to resolve ICF suffers from imprecision and high computational complexity. As a practical alternative, we present a novel solution of interactive […]
ICSE 2016 – Rethinking Verification: Accuracy, Efficiency and Scalability through Human-Machine Collaboration
Abstract: With growing dependence on software in embedded and cyber-physical systems where vulnerabilities and malware can lead to disasters, efficient and accurate verification has become a crucial need for safety and cybersecurity. Formal verification of large software has remained an elusive target, riddled with problems of low accuracy and high computational complexity. The need for […]
ICSE 2015 – Security Toolbox for Detecting Novel and Sophisticated Android Malware
Abstract: This paper presents a demo of our Security Toolbox to detect novel malware in Android apps. This Toolbox is developed through our recent research project funded by the DARPA Automated Program Analysis for Cybersecurity (APAC) project. The adversarial challenge (“Red”) teams in the DARPA APAC program are tasked with designing sophisticated malware to test […]
ICSE 2014 – Atlas: A New Way to Explore Software, Build Analysis Tools
Abstract: Atlas is a new software analysis platform from EnSoft Corp. Atlas decouples the domain-specific analysis goal from its underlying mechanism by splitting analysis into two distinct phases. In the first phase, polynomial-time static analyzers index the software AST, building a rich graph database. In the second phase, users can explore the graph directly or […]