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

ICISS 2015 – FlowMiner: Automatic Summarization of Library Data-Flow for Malware Analysis

Abstract: FlowMiner is a tool for automatically mining expressive, fine-grained data-flow summaries from Java library bytecode. FlowMiner captures enough information to enable context, type, field, object and flow-sensitive partial program analysis of applications using the library. FlowMiner’s summaries are compact- flow details of a library that are non-critical for future partial program analysis of applications are elided into simple […]

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

SMC 2014 – A “Human-in-the-loop” Approach for Resolving Complex Software Anomalies

Abstract: Automated static analysis tools are widely used in identifying software anomalies, such as memory leak, unsafe thread synchronization and malicious behaviors in smartphone applications. Such anomaly-prone scenarios can be bifurcated into: “ordinary” (analysis requires relatively simple automation) and “complex” (analysis poses extraordinary automation challenges). While automated static analysis tools can resolve ordinary scenarios with […]

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