ITU

Effective Bug Finding in C Programs with Shape and Effect Abstractions

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

View graph of relations

Software projects tend to suffer from conceptually simple resource manipulation bugs, such as accessing a de-allocated memory region, or acquiring a non-reentrant lock twice. Static code scanners are used extensively to remove these bugs from projects like the Linux kernel. Yet, when the manipulation of the resource spans multiple functions, efficiently finding these bugs is a challenge. We present a shape-and-effect inference system for C, that enables efficient and scalable inter-procedural reasoning about resource manipulation. The inference system is used to build a program abstraction: a control-flow graph decorated with alias relationships and observable effects. Bugs are found by model checking this control-flow graph, matching undesirable sequences of operations. We evaluate a prototype implementation of our approach (EBA) and run it on a collection of historical double-lock bugs from the Linux kernel. Our results show that our tool is more effective at finding bugs than similar code-scanning tools. EBA analyzes the drivers/ directory of Linux (nine thousand files) in less than thirty minutes, and uncovers a handful previously unknown double-lock bugs in various drivers.

Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation : 18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings
PublisherSpringer
Publication date2017
Pages34-54
ISBN (Print)978-3-319-52233-3
ISBN (Electronic)978-3-319-52234-0
DOIs
Publication statusPublished - 2017
Event18th International Conference on Verification, Model Checking, and Abstract Interpretation - The Jussieu campus of Université Pierre et Marie Curie, Paris, France
Duration: 15 Jan 201717 Jan 2017
Conference number: 18
http://conf.researchr.org/home/VMCAI-2017

Conference

Conference18th International Conference on Verification, Model Checking, and Abstract Interpretation
Nummer18
LocationThe Jussieu campus of Université Pierre et Marie Curie
LandFrance
ByParis
Periode15/01/201717/01/2017
Internetadresse
SeriesLecture Notes in Computer Science
Volume10145
ISSN0302-9743
Close

    Research areas

  • Type and effects, Bug finding, C, Type inference, Model checking, Linux, Double lock

Downloads

No data available

ID: 81606585