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

Standard

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 chapterArticle in proceedingsResearchpeer-review

Harvard

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

APA

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 (pp. 34-54). Springer. Lecture Notes in Computer Science Vol. 10145 https://doi.org/10.1007/978-3-319-52234-0_3

Vancouver

Abal I, Brabrand C, Wasowski A. 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. 2017. p. 34-54. (Lecture Notes in Computer Science, Vol. 10145). https://doi.org/10.1007/978-3-319-52234-0_3

Author

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

Bibtex

@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",

}

RIS

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 -

ID: 81606585