Blog Archives

APSEC 2017 – Intelligence Amplifying Loop Characterizations for Detecting Algorithmic Complexity Vulnerabilities

Abstract: Algorithmic complexity vulnerabilities (ACVs) can be exploited to cause denial-of-service. Detecting ACVs is hard because of the numerous kinds of loop complexities that cause ACVs. This renders automatic detection intractable for ACVs. State-of-the-art loop analyses aim to obtain precise loop iteration bounds automatically; they can do so for relatively simple loops. This research focuses […]

Categories: Papers, Upcoming

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

NIT Patna – Learn to Understand, Analyze, and Verify Large Software

Abstract: Massive software systems are being built the way Egyptians were building pyramids, with the sheer force of human labor. Agile development, programming languages, component libraries, and integrated development environments, help but they have not brought down the cost of developing and maintaining software. Software projects continue to run over projected budgets and schedule. The […]

Categories: Short Courses

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

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