Andrzej Wąsowski (IT University of Copenhagen)
Andrzej Wasowski works with design and use of technologies that improve the quality of software, including issues such as correctness and maintainability. He has worked extensively with software product line methods—ways to develop software for similar products at lower cost but with higher quality. He has collaborated with open source projects (the Linux kernel among others) and industry (for example with Danfoss). Currently, he is working on technical solutions to support software modernization, studying how old software can be moved to new platforms and how to restructure software without losing its properties. He is also investigating quality assurance methods for robotics platforms, in the H2020 project ROSIN.
Andrzej Wasowski is a professor of Software Engineering at IT University in Copenhagen (ITU). He holds an MSc degree from Warsaw University of Technology and a Ph.D. degree from ITU. He has previously held visiting positions at Aalborg University (Denmark), INRIA Rennes (France) and University of Waterloo (Canada). He is general chair of MODELS’2018 conference, program chair of ECMFA’16 and FASE’16 and a member of the editorial board of the SoSyM journal. He is a recipient of the Sapere Aude research leadership award from The Danish Council for Independent Research (2012).
Keynote Title: Finding Resource Manipulation Bugs in Linux Code
Abstract: Software projects suffer from conceptually simple resource manipulation bugs, such as accessing a deallocated memory region, or acquiring a non-reentrant lock twice. The VBDB bug database contains entries for 100 such real bugs from several open source projects, including the Linux Kernel project. These historical bugs have been collected with the aim of giving concrete well understood and documented cases to program analysis researchers, in order to boost program verification research. I will discuss simplicity and complexity of real software manipulation bugs on examples selected from VBDB. One way to reduce the amount of such bugs is to use code scanners such as Smatch or Coccinelle. Unfortunately, while very efficient, code scanners are typically based on syntactic pattern matching, which is insufficient for identifying problems that span multiple functions and involve dynamically allocated memory. We have developed a shape-and-effect inference system for C that constructs a lightweight semantic abstraction, more analyzable than syntax. A model checker is then used to match semantic bug patterns over the control flow graph decorated with the shape-and-effect abstractions. Experiments run with our prototype analyzer (EBA) shows better precision and effectiveness than with syntactic bug scanners. We have been so far able to identify 10 previously unknown locking bugs in the Linux kernel. The bugs are confirmed as real by the Kernel developers, and five of them have been already fixed in response to our reports. I will conclude, sketching how we combine EBA with another tool, RECONFIGURATOR, to massively scan Linux kernel code for bugs in atypical source configurations.
