Blog Archives

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 […]

Categories: Papers

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 […]

Categories: Papers

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 […]

Categories: Papers

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 […]

Categories: Papers

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 […]

Categories: Papers