Blog Archives

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

Categories: Papers, Upcoming

APSEC 2016 – Projected Control Graph for Accurate and Efficient Analysis of Safety and Security Vulnerabilities

Abstract: The goal of path-sensitive analysis (PSA) is to achieve accuracy by accounting precisely for the execution behavior along each path of a control flow graph (CFG). A practical adoption of PSA is hampered by two roadblocks: (a) the exponential growth of the number of CFG paths, and (b) the exponential complexity of a path […]

Categories: Papers

FVPE 2016 – Insights for Practicing Engineers from a Formal Verification Study of the Linux Kernel

Abstract: Formal verification of large software has been an illusive target, riddled with the problem of scalability. Even if the obstacle of scale may be cleared, major challenges remain to adopt formal verification in practice. This paper presents an empirical study using a top-rated formal verification tool for Linux, and draws insights from the study […]

Categories: Papers

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

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