The Augmented Reality of Model Counting
In this talk we will show that by augmenting symbolic execution with model counting some interesting insights can be gained into the power of well known testing techniques. For example, why random test generation often achieves good structural coverage, but can still miss bugs. Why mutations might be representative of real bugs, but could be too easy to kill. We will also consider methods for determining how close two programs are to being the same (or the dual of how much they are different).
About the speaker
Willem Visser is a professor in the Division of Computer Science at Stellenbosch University (from 2009 till 2013 he was the Head of the Division). His research is mostly focussed around finding bugs in software. More specifically he works on testing, program analysis, symbolic execution, probabilistic symbolic execution and model checking. He is probably most well known for his work on Java PathFinder (JPF) and Symbolic PathFinder (SPF). He previously worked at NASA Ames Research Center, and SEVEN Networks.
String Analysis for Vulnerability Detection and Repair
String manipulation errors in input validation and sanitization code are a common source for security vulnerabilities in web applications. In this talk, I will discuss the string analysis techniques we developed that can automatically identify and repair such vulnerabilities. Our approach (1) extracts client- and server-side input validation and sanitization functions, (2) models them as deterministic finite automata (DFAs) using symbolic fixpoint computations, and (3) identifies errors in input validation and sanitization code by either checking them with respect to manually specified attack patterns, or by identifying inconsistencies in input validation and sanitization operations at the client and server-side. Furthermore, we developed automated repair techniques that strengthen the input validation and sanitization checks in order to eliminate identified vulnerabilities. We implemented these techniques in two tools: Stranger (STRing AutomatoN GEneratoR) and SemRep (SEMantic differential REPair), which are available at: http://www.cs.ucsb.edu/~vlab/tools.html. Our evaluation demonstrates that these techniques are very promising: when applied to a set of real-world web applications, our techniques are able to automatically identify a large number of security vulnerabilities and repair them.
About the speaker
Tevfik Bultan is a Professor in the Department of Computer Science at the University of California, Santa Barbara (UCSB). His current research interests are in dependability of web software and services, automated verification, string analysis, and data model specification and analysis. He co-chaired the program committees of the 9th International Symposium on Automated Technology for Verification and Analysis (ATVA 2011), the 20th International Symposium on the Foundations of Software Engineering (FSE 2012) which is the flagship conference of ACM SIGSOFT, and the 28th IEEE/ACM International Conference on Automated Software Engineering (ASE 2013). He has served as the vice chair of the Department of Computer Science at UCSB from 2005 to 2009. He received a NATO Science Fellowship from the Scientific and Technical Research Council of Turkey (TUBITAK) in 1993, a Regents' Junior Faculty Fellowship from the University of California, Santa Barbara in 1999, a Faculty Early Career Development (CAREER) Award from the National Science Foundation in 2000, the ACM SIGSOFT Distinguished Paper Award in 2005 and 2014, and the Best Paper Award at the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE 2005).
CBMC: Bounded Model Checking of Concurrent C Programs
CBMC implements bit-precise bounded model checking for C programs and has been developed and maintained for more than ten years. Only recently support for efficiently checking concurrent programs, including support for weak memory models, has been added. CBMC verifies the absence of violated assertions under a given loop unwinding bound by reducing the problem to a Boolean formula. The formula is passed to a SAT solver, which returns a model if and only if the property is violated.
In the tutorial I will provide an overview of the key components of CBMC, underlining its straightforward pipeline. Then a number of examples will be presented, including floating point and concurrent programs. I will then move on full software systems, such as analysing a SAT solver and my recent work of applying CBMC across the entire Debian/GNU Linux distribution.
Participants are asked to bring a laptop and encouraged to install CBMC (by downloading from http://www.cprover.org/cbmc/ or using the Linux package manager). Installation is generally straightforward, but extra software may be required on Windows (Visual Studio) or OS X (XCode Command Line Tools) – both of these requirements are detailed on the web site.
About the speaker
Michael Tautschnig is a lecturer at Queen Mary University of London. He obtained his PhD from Vienna University of Technology developing an efficient, systematic, and automatic test input generation technique for C programs. Prior to his appointment as lecturer he was a post-doctoral research at the University of Oxford. His current and recent research focusses automating verification for real-world software at large scale, and efficient software verification techniques for concurrent, shared-memory systems with relaxed memory models.