Blog Archives

MILCOM 2016 – Discovering Information Leakage Using Visual Program Models

Abstract:  This tutorial is about new genera of information leakage vulnerabilities, far more difficult to detect than the vulnerabilities that have previously dominated the software security landscape. We will survey attacks that have exploited information leakage vulnerabilities to steal sensitive information. We will show how to discover information leakage vulnerabilities using techniques and tools for […]

Categories: Tutorials

ISSRE 2016 – Mission-Critical Software Assurance Engineering ­Beyond Testing, Bug Finders, Metrics, Reliability Analysis, and Formal Verification

Abstract:  Today, mission-critical software assurance engineering must encompass both safety and cyber-security. Critical missions, whether in defense, government, banking, or healthcare depend on ensuring that a system meets safety requirements, and it does not fail under cyber attack. Mobile, cloud and Internet of Things (IoT) have made software assurance integral to our everyday lives, whether […]

Categories: Tutorials

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

IASTATE/ECPE 2016 – Euler, the 336 Million Dollar Software Patent, and Reflecting on How to Solve Hard Software Problems

Abstract:  The size and complexity of software, the labor cost of programming, and the dire consequences of software malfunctioning have made it a nightmare to maintain software-intensive cyber-physical systems. Agile development, programming languages, component libraries etc. help but they do not suffice to ensure correctness and cost-effective maintenance of complex software. The central question is: […]

Categories: Talks

SCAM 2016 – Statically-informed Dynamic Analysis Tools to Detect Algorithmic Complexity Vulnerabilities

Abstract:  Algorithmic Complexity (AC) vulnerabilities can be exploited to cause a denial of service attack. Specifically, an adversary can design an input to trigger excessive (space/time) resource consumption. It is not possible to build a fully automated tool to detect AC vulnerabilities. Since it is an open-ended problem, a human-in-loop exploration is required to find […]

Categories: Papers

GIAN 2016 – Managing Complexity, Security, and Safety of Large Software

Abstract: Software malfunctions can have catastrophic consequences and enormous costs. The error-prone and laborious manual practices of developing and maintaining large software must change to cope with ever increasing complexity of software, and the enormous safety and security challenges it poses. Formal verification is not a practical alternative for large software; it is riddled with problems […]

Categories: Short Courses

ASE 2016 – Learn to Build Automated Software Analysis Tools with Graph Paradigm and Interactive Visual Framework

Abstract: Software analysis has become complex enough to be intimidating to new students and professionals. It can be difficult to know where to start with over three decades of staggering research in data and control flow analyses and a plethora of analysis frameworks to choose from, ranging in maturity, support, and usability. While textbooks, surveys […]

Categories: Tutorials

SERIP 2016 – Software Engineering Research Lab to Airplanes, Orion and Beyond: One professor’s journey shaped by industry-university collaboration

Abstract: This paper is a short story of my adventures of the past 20 years trying to integrate academic research with software engineering problems in industry. I share the challenges I encountered on the way, my failures and successes, evolution of my research, and its adoption in industry. Though I faced many hardships, I feel […]

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