Effective Bug Finding in C Programs with Shape and Effect Abstractions

Iago Abal; Claus Brabrand; Andrzej Wasowski

doi:10.1007/978-3-319-52234-0_3

Effective Bug Finding in C Programs with Shape and Effect Abstractions

Iago Abal, Claus Brabrand, Andrzej Wasowski

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

Abstract

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 language	English
Title of host publication	Verification, Model Checking, and Abstract Interpretation : 18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings
Publisher	Springer
Publication date	2017
Pages	34-54
ISBN (Print)	978-3-319-52233-3
ISBN (Electronic)	978-3-319-52234-0
DOIs	https://doi.org/10.1007/978-3-319-52234-0_3
Publication status	Published - 2017
Event	18th International Conference on Verification, Model Checking, and Abstract Interpretation - The Jussieu campus of Université Pierre et Marie Curie, Paris, France Duration: 15 Jan 2017 → 17 Jan 2017 Conference number: 18 http://conf.researchr.org/home/VMCAI-2017

Conference

Conference	18th International Conference on Verification, Model Checking, and Abstract Interpretation
Number	18
Location	The Jussieu campus of Université Pierre et Marie Curie
Country/Territory	France
City	Paris
Period	15/01/2017 → 17/01/2017
Internet address	http://conf.researchr.org/home/VMCAI-2017

Series	Lecture Notes in Computer Science
Volume	10145
ISSN	0302-9743

Keywords

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

Access to Document

10.1007/978-3-319-52234-0_3

2017-vmcai-iago-ebaAccepted author manuscript, 428 KB

Cite this

@inproceedings{3d3d590d89b74776847b8da1ca104c45,

title = "Effective Bug Finding in C Programs with Shape and Effect Abstractions",

abstract = "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.",

keywords = "Type and effects, Bug finding, C, Type inference, Model checking, Linux, Double lock",

author = "Iago Abal and Claus Brabrand and Andrzej Wasowski",

year = "2017",

doi = "10.1007/978-3-319-52234-0_3",

language = "English",

isbn = "978-3-319-52233-3",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "34--54",

booktitle = "Verification, Model Checking, and Abstract Interpretation",

address = "Germany",

note = "18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017 ; Conference date: 15-01-2017 Through 17-01-2017",

url = "http://conf.researchr.org/home/VMCAI-2017",

}

Abal, I, Brabrand, C & Wasowski, A 2017, Effective Bug Finding in C Programs with Shape and Effect Abstractions. in Verification, Model Checking, and Abstract Interpretation: 18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings. Springer, Lecture Notes in Computer Science, vol. 10145, pp. 34-54, 18th International Conference on Verification, Model Checking, and Abstract Interpretation, Paris, France, 15/01/2017. https://doi.org/10.1007/978-3-319-52234-0_3

Effective Bug Finding in C Programs with Shape and Effect Abstractions. / Abal, Iago; Brabrand, Claus ; Wasowski, Andrzej.
Verification, Model Checking, and Abstract Interpretation: 18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings. Springer, 2017. p. 34-54 (Lecture Notes in Computer Science, Vol. 10145).

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - Effective Bug Finding in C Programs with Shape and Effect Abstractions

AU - Abal, Iago

AU - Brabrand, Claus

AU - Wasowski, Andrzej

N1 - Conference code: 18

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

KW - Type and effects

KW - Bug finding

KW - C

KW - Type inference

KW - Model checking

KW - Linux

KW - Double lock

U2 - 10.1007/978-3-319-52234-0_3

DO - 10.1007/978-3-319-52234-0_3

M3 - Article in proceedings

SN - 978-3-319-52233-3

T3 - Lecture Notes in Computer Science

SP - 34

EP - 54

BT - Verification, Model Checking, and Abstract Interpretation

PB - Springer

T2 - 18th International Conference on Verification, Model Checking, and Abstract Interpretation

Y2 - 15 January 2017 through 17 January 2017

ER -

Effective Bug Finding in C Programs with Shape and Effect Abstractions

Abstract

Conference

Keywords

Access to Document

Fingerprint

Cite this