Finding Resource Manipulation Bugs in Linux Code

Finding Resource Manipulation Bugs In Linux Code with Type-And-Effect Abstraction — Andrzej W ˛asowski @AndrzejWasowski joint work with (lexicographically) Iago Abal Claus Brabrand Alexandru F. Iosif Lazar Aleksandar Dimovski Jean Melo Marcio Ribeiro Ahmad Salim Al-Sibahi Stefan Stanciulescu c Andrzej W ˛asowski, IT University of Copenhagen 1

Contributions related to all aspects of modeling, modeling languages and model-driven engineering are cordially invited to the 21st edition of MODELS, in Copenhagen, Denmark, October 14th -19th 2018. MODELS is the premier conference series for model-driven software and systems engineering. Since 1998, MODELS has covered all aspects of modeling, from languages and methods, to tools and applications. Attendees of MODELS come from diverse backgrounds, including researchers, academics, engineers and industrial professionals. MODELS 2018 is a forum for participants to exchange cutting-edge research results and innovative practical experiences around modeling and model-driven software and systems. This year’s edition will provide an opportunity for the modeling community to further advance the foundations of modeling, and come up with innovative applications of modeling in emerging areas of cyber-physical systems, embedded systems, socio-technical systems, cloud computing, big data, security, open source, and sustainability. We invite you to join us at MODELS 2018, Copenhagen, Denmark and to help shape the modelling methods and technologies of the future! Tracks MODELS 2018 has two distinct paper tracks: Foundations Track, and Practice and Innovation Track. The Foundations Track includes both Technical Papers describing innovative research in modelling and model-driven engineering and New Ideas and Vision Papers describing non-conventional but well-defined research positions or approaches that depart from standard practice. The Practice and Innovation Track fills the gap between foundational research in modelling and model-driven engineering and industrial needs. It includes original papers on innovative application of model-driven engineering in industrial, govermental or open-source settings, and development of engineering solutions that enable modelling in such contexts. Submission Process Papers must be submitted electronically through the MODELS 2018 EasyChair submission web page: https://easychair.org/conferences/?conf=models2018 Review Process The MODELS 2018 review process will use two phases in order to provide high quality reviews. The reviewing and discussion process is monitored by one or two Program Board members assigned to each paper. In the first phase, all papers that conform to the submission guidelines will be peer-reviewed by at least three members of the Program Committee (PC). The most viable papers identified by the PC will advance to the second phase, where the paper authors may be given the opportunity to respond to questions posed by PC members in their review. The Program Board will then consider the recommendations and online discussion of the Program Committee, as well as the author response, and select the papers to be notified for acceptance to the conference. Artifact Evaluation Authors of accepted papers will be invited to submit their accompanying artifacts to the optional Artifact Evaluation process. The process is run by a separate committee, and papers succesfully completing the process will get a seal of approval. General Chair Andrzej Wąsowski Important Dates Abstract Submission 27th April 2018 Paper Submission 4th May 2018 First Notification 12th June 2018 Author Response 12th -14th June 2018 Final Notification 3rd July 2018 Camera Ready 21st July 2018 ACM/IEEE 21st International Conference on Model Driven Engineering Languages and Systems October 14th -19th 2018, Copenhagen, Denmark www.modelsconference.org Richard Paige Øystein Haugen We look forward to your submission, your Program Chairs Mermaid Silhouette based on a photography licensed CC-BY 2.0 Miguel Mendez. Cøpenhagen is an artistic combination of the English and Danish names for the city “Copenhagen” and “København”. c Andrzej W ˛asowski, IT University of Copenhagen 2

AGENDA Bugs in the kernel (VBDB) Finding bugs with Shapes and Effects (EBA) Handling #ifdefs (Reconﬁgurator) c Andrzej W ˛asowski, IT University of Copenhagen 3

Let’s look at a bug Dereferencing uninitialized pointer causes Kernel crash 1 #ifdef CONFIG_DEVPTS_MULTIPLE_INSTANCES 2 if (inode->i_sb->s_magic == ... ) . . . 3 #endif void pts_sb_from_inode(struct inode * inode) 4 #ifdef CONFIG_UNIX98_PTYS 5 pts_sb_from_inode (tty->driver_data); 6 #endif void pty_close(struct tty_struct * tty) 7 tty = kzalloc(sizeof (*tty), GFP_KERNEL); 8 pty_close (tty) · · · Domain knowledge Data ﬂow Inter-procedural data-ﬂow Pointers Nested structs [real bug] cross compilation unit and subsystem [real bug] function pointers (pty_close) c Andrzej W ˛asowski, IT University of Copenhagen 4 Bug 7acf6cd, see http://vbdb.itu.dk/#bug/linux/7acf6cd Iago Abal, Claus Brabrand, Andrzej Wasowski. 42 variability bugs in the Linux kernel: a qualitative analysis. ASE 2014: 421-432 + journal submission

Let’s look at another bug Control-flow Unsafe casts help generic programing of data structures Type casts, pointers to ints; Do not loose shapes and aliasing info Function pointers used heavily (OO) Inter-procedural data-flow not possible without control-flow [elsewhere] conditional struct components (with incompatible casts) c Andrzej W ˛asowski, IT University of Copenhagen 5 Bug 657e964e74

Hunting bugs in software Is for tough warriors Not for those of faint heart It’s not (only) about λ-calculus or the tiny term grammar in Fig. 2, your paper c Andrzej W ˛asowski, IT University of Copenhagen 6

Warning: You may need to get dirty c Andrzej W ˛asowski, IT University of Copenhagen 7

Let’s have a look at a bug c Andrzej W ˛asowski, IT University of Copenhagen 8 See http://git.kernel.org/cgit/linux/kernel/git/stable/linux-stable.git/commit/?id= 7acf6cd80b201f77371a5374a786144153629be8

c Andrzej W ˛asowski, IT University of Copenhagen 9 See http://vbdb.itu.dk/, and add your own bugs

Subject Systems As of December 2015 System Domain LOC #Features #Commits Marlin 3D-printer ﬁrmware 0.04M 821 2,783 BusyBox UNIX utilities 0.2M 551 13,878 Apache Web Server 0.2M 681 27,677 Linux kernel Operating system 14M 16,490 521,276 c Andrzej W ˛asowski, IT University of Copenhagen 10 Iago Abal. Jean Melo. Stefan St˘anciulescu. Claus Brabrand. Márcio Ribeiro. Andrzej W ˛asowski. Variability Bugs in Highly-Conﬁgurable Systems: A Qualitative Analysis. Accepted for TOSEM

Lesson 1 Other researchers will be glad if you help them avoiding dirt. You will help research quality in your ﬁeld. c Andrzej W ˛asowski, IT University of Copenhagen 11

Bug Hunting Is for tough warriors, But even warriors need the right weapons c Andrzej W ˛asowski, IT University of Copenhagen 13

What do we see? Diversity! 15 memory errors CWE ID 4 null pointer dereference 476 3 buffer overflow 120 3 read out of bounds 125 2 insufficient memory - 1 memory leak 401 1 use after free 416 1 write on read only - 8 compiler warnings CWE ID 5 uninitialized variable 457 1 unused function (dead code) 598 1 unused variable 563 1 void pointer dereference - 7 type errors CWE ID 5 undefined symbol - 1 undeclared identifier - 1 wrong number of args to function - 7 assertion violations CWE ID 5 fatal assertion violation 617 2 non-fatal assertion violation 617 2 API violations CWE ID 1 Linux API contract violation - 1 double lock 764 1 arithmetic errors CWE ID 1 numeric truncation 197 Linux 4 memory errors: CWE ID 2 null pointer dereference 476 1 memory leak 401 1 use after free 416 6 compiler warnings: CWE ID 3 unused variable 563 2 uninitialized variable 457 1 incompatible types 843 5 type errors: CWE ID 3 undefined symbol - 2 undeclared identifier - 3 logic errors: CWE ID 3 behavior violation 440 BusyBox c Andrzej W ˛asowski, IT University of Copenhagen 14

Welcome to EBA! Effect-Based Analyzer For this to work we need to know about effects And about memory objects (to detect aliasing) c Andrzej W ˛asowski, IT University of Copenhagen 15 See http://eba.wikit.itu.dk/

0xCAFE 0xC0DE mem. addr. shape ρ ref 42 ⊥ ref ρ'0xCAFE ptr Shape term: refρ ptr refρ ⊥ c Andrzej W ˛asowski, IT University of Copenhagen 16

Inference of Shapes & Effects : Env × Exp × Shape × Effect Formalized and implemented for entire C Including spec. of selected kernel functions, e.g: c Andrzej W ˛asowski, IT University of Copenhagen 17

Bug Pattern Deﬁnitions Formalize bug patterns in CTL with nominals over effects A simple reachability checker ﬁnds paths matching a formula E.g. double lock = lock, then take same lock again without unlocking c Andrzej W ˛asowski, IT University of Copenhagen 18

Does this work? Precision (false positives), new bugs Nine thousand files in drivers analyzed (you do get dirty!) 9 reports for 9K lines is not a lot of noise Each reported bug classified as either a true or a false positive. Still a lot of work to filter out false positives (you get dirty!) You talk to devs: they want you to fix bugs! (you may get dirty!) We right now have 7 new bugs confirmed and 5 fixed in the Linux kernel projects (some in the main tree already) c Andrzej W ˛asowski, IT University of Copenhagen 19

Does this work? Experimental Evaluation, time in seconds, recall on historical bugs hash ID depth E S C 1173ff0 0 0.6 1.3 0.1 149a051 0 0.7 0.6 0.3 16da4b1 0 0.4 0.8 0.1 344e3c7 0 0.7 1.3 0.1 2904207 0 5.8 2.0 2.8 59a1264 0 0.2 0.6 0.1 5ad8b7d 0 0.6 3.4 0.1 8860168 0 0.7 1.0 0.1 a7eef88 0 0.6 1.2 0.2 b838396 0 3.3 2.8 1.1 ca9fe15 0 0.4 0.7 1.8 e1db4ce 0 0.4 1.1 0.2 e50fb58 0 0.5 0.9 0.1 023160b 0 1.0 2.6 0.1 09dc3cf 0 1.2 1.4 0.1 0adb237 0 1.1 1.5 0.2 0e6f989 0 0.4 1.0 0.3 (17 historical bugs, intra-proc, double-lock, in Linux kernel, biased against EBA) Bug depth E S C 00dfff7 2 5.0 1.5 0.1 5c51543 2 2.3 1.5 0.3 b383141 2 6.1 2.9 0.3 1c81557 1 5.0 1.9 0.6 328be39 1 8.9 1.7 0.2 5a276fa 1 0.9 1.2 0.2 80edb72 1 6.3 2.1 0.7 872c782 1 1.7 2.8 1.9 d7e9711 1 21 1.3 2.7 (9 historical bugs, inter-proc, double-lock, in Linux kernel, biased against EBA) c Andrzej W ˛asowski, IT University of Copenhagen 20

Lesson 2 After all, lambdas, types, and model checking are useful for solving real problems. (but we wouldn’t know without trying on real problems) c Andrzej W ˛asowski, IT University of Copenhagen 21

Adding Variability with Reconfigurator variational program lifted analysis derive abstract lifted analysis apply abstraction abstracted variational program reconfigure derive One simplistic reconfigurator for data-flow and Java One simplistic reconfigurator for model-checking and (f)Promela Developing a full-blown reconfigurator for C c Andrzej W ˛asowski, IT University of Copenhagen 23 Jan Midtgaard, Aleksandar S. Dimovski, Claus Brabrand, Andrzej Wasowski: Systematic derivation of correct variability-aware program analyses. Sci. Comput. Program. 105: 145-170 (2015) Aleksandar S. Dimovski, Claus Brabrand, Andrzej Wasowski. Variability Abstractions: Trading Precision for Speed in Family-Based Analyses. ECOOP 2015

Let’s look at a bug Dereferencing uninitialized pointer causes Kernel crash 1 #ifdef CONFIG_DEVPTS_MULTIPLE_INSTANCES 2 if (inode->i_sb->s_magic == ... ) . . . 3 #endif void pts_sb_from_inode(struct inode * inode) 4 #ifdef CONFIG_UNIX98_PTYS 5 pts_sb_from_inode (tty->driver_data); 6 #endif void pty_close(struct tty_struct * tty) 7 tty = kzalloc(sizeof (*tty), GFP_KERNEL); 8 pty_close (tty) · · · Domain knowledge Data ﬂow Inter-procedural data-ﬂow Pointers Nested structs [real bug] cross compilation unit and subsystem [real bug] function pointers (pty_close) c Andrzej W ˛asowski, IT University of Copenhagen 24 Bug 7acf6cd, see http://vbdb.itu.dk/#bug/linux/7acf6cd Iago Abal, Claus Brabrand, Andrzej Wasowski. 42 variability bugs in the Linux kernel: a qualitative analysis. ASE 2014: 421-432 + journal submission

Replace Variability by Non-determinism Dereferencing uninitialized pointer causes Kernel crash 1 if (CONFIG_DEVPTS_MULTIPLE_INSTANCES) {if (*) { 2 if (inode->i_sb->s_magic == ... ) . . . 3 } void pts_sb_from_inode(struct inode * inode) 4 if (CONFIG_UNIX98_PTYS) {if (*) { 5 pts_sb_from_inode (tty->driver_data); 6 } void pty_close(struct tty_struct * tty) 7 tty = kzalloc(sizeof (*tty), GFP_KERNEL); 8 pty_close (tty) · · · In reality much harder: Handle issues with parsing, conditional macros, types, struct components, initializers, function prototypes, etc. But if only allowed at statement level c Andrzej W ˛asowski, IT University of Copenhagen 25

Conclusion Bug Hunting Is for tough warriors, But even warriors need the right weapons c Andrzej W ˛asowski, IT University of Copenhagen 10 Lesson 1 Other researchers will be glad if you help them avoiding dirt. You will help research quality in your ﬁeld. c Andrzej W ˛asowski, IT University of Copenhagen 9 Lesson 2 After all, lambdas, types, and model checking are useful for solving real problems. (but we wouldn’t know without trying on real problems) c Andrzej W ˛asowski, IT University of Copenhagen 19 Computer Science Software Engineering Practice Theory c Andrzej W ˛asowski, IT University of Copenhagen 26

Finding Resource Manipulation Bugs In Linux Code with Type-And-Effect Abstraction — Andrzej W ˛asowski @AndrzejWasowski joint work with (lexicographically) Iago Abal Claus Brabrand Alexandru F. Iosif Lazar Aleksandar Dimovski Jean Melo Marcio Ribeiro Ahmad Salim Al-Sibahi Stefan Stanciulescu c Andrzej W ˛asowski, IT University of Copenhagen 27

Another Bug: double lock 1 @@ 2 expression E; 3 @@ 4 * spin_lock(E); 5 ... when != spin_unlock(E); 6 * spin_lock(E); Coccinelle matches patterns over traces Supports CPP, efﬁcient, Integrated into the kernel build system Intra procedural, unaware of aliasing c Andrzej W ˛asowski, IT University of Copenhagen 28 See http://coccinelle.lip6.fr/ by Julia Lawall, Rene Rydhof Hansen, and many others

Finding Resource Manipulation Bugs in Linux Code

More Related Content

Similar to Finding Resource Manipulation Bugs in Linux Code

Recently uploaded

Finding Resource Manipulation Bugs in Linux Code