Talk Abstracts

Title: SuSi - A Machine-learning Approach for Classifying and Categorizing Android Sources and Sinks (NDSS'14)

Presenter: Eric Bodden, Fraunhofer SIT & Technische Universität Darmstadt, Germany

Abstract: Today’s smartphone users face a security dilemma: many apps they install operate on privacy-sensitive data, although they might originate from developers whose trustworthiness is hard to judge. Researchers have addressed the problem with more and more sophisticated static and dynamic analysis tools as an aid to assess how apps use private user data. Those tools, however, rely on the manual configuration of lists of sources of sensitive data as well as sinks which might leak data to untrusted observers. Such lists are hard to come by.

We thus propose SUSI, a novel machine-learning guided approach for identifying sources and sinks directly from the code of any Android API. Given a training set of hand-annotated sources and sinks, SUSI identifies other sources and sinks in the entire API. To provide more fine-grained information, SUSI further categorizes the sources (e.g., unique identifier, location information, etc.) and sinks (e.g., network, file, etc.).

For Android 4.2, SUSI identifies hundreds of sources and sinks with over 92% accuracy, many of which are missed by current information-flow tracking tools. An evaluation of about 11,000 malware samples confirms that many of these sources and sinks are indeed used. We furthermore show that SUSI can reliably classify sources and sinks even in new, previously unseen Android versions and components like Google Glass or the Chromecast API.

Bio: Eric Bodden is department head for Secure Software Engineering (SSE) at the Fraunhofer Institute for Secure Information Technology (SIT) as well as Professor for Secure Software Engineering at Technische Universität Darmstadt. The focus of his research group is on developing methods and largely automated tools for securing large software systems early during the development process. The SSE group is well known for publishing high-quality research tools such as the inter-procedural analysis framework Heros, the Android taint-analysis tool FlowDroid or - now new - the tool SuSi that will be presented in this talk.

Title: Safe Software Updates via Multi-version Execution

Presenter: Cristian Cadar, Imperial College London, UK

Abstract: Software systems are constantly evolving, with new versions and patches being released on a continuous basis. Unfortunately, software updates present a high risk, with many releases introducing new bugs and security vulnerabilities. We tackle this problem using a simple but effective multi-version based approach. Whenever a new update becomes available, instead of upgrading the software to the new version, we run the new version in parallel with the old one; by carefully coordinating their executions and selecting the behavior of the more reliable version when they diverge, we create a more secure and dependable multi-version application. We implemented this technique in Mx, a system targeting Linux applications running on multi-core processors, and show that it can be applied successfully to several real applications, such as Lighttpd and Redis.

Bio: Cristian Cadar leads the Software Reliability Group (http://srg.doc.ic.ac.uk) in the Department of Computing at Imperial College London. His research interests span the areas of software engineering, computer systems and security, with an emphasis on designing practical techniques for improving the reliability and security of software systems. Cristian received a PhD in Computer Science from Stanford University, and undergraduate and Master's degrees from the Massachusetts Institute of Technology.

Title: Testing Software Product Lines with Incomplete Feature Models

Presenter: Marcelo d'Amorim, Federal University of Pernambuco, Brazil

Abstract: A software product line is a family of programs that are differentiated by features -- increments in functionality. Systematically testing a product line is challenging because it requires running a test suite against a combinatorial number of programs. Feature models capture dependencies among features and can (1) reduce the space of programs to test and (2) enable accurate categorization of failing tests as failures of programs or the tests themselves, not as failures due to invalid combinations of features. In practice, unfortunately, feature models are not always available. We introduce SPLif, the first approach for testing software product lines that does not require a priori availability of feature models. Our insight is to use a profile of passing and failing test runs to quickly identify failures caused by real faults in the program under test, distinguishing them from faults caused by invalid combination of features. Experimental results on five software product lines demonstrate the effectiveness of our approach

Bio: Marcelo d'Amorim holds a PhD in Computer Science from the University of Illinois at Urbana-Champaign. He is an Assistant Professor at the Federal University of Pernambuco (UFPE) since 2009. His research goal is to improve software quality through program analysis and systematic testing. He wants to make existing techniques more accurate, more automated, more user-friendly, and, when needed, more efficient.

Talk title: In Memory Yet Green

Presenter: Jaco Geldenhuys, Stellenbosch University, South Africa

Abstract: The Green system reduces, recycles, and reuses results by factorizing queries and representing them in a canonical form, and storing the results of previous queries for future use. In essence, it is a cache for constraint satisfiability checking that operates across runs, programs, and tools. This talk describes the Green architecture and discusses some of its applications and results.

Bio: Jaco Geldenhuys is an Associate Professor at Stellenbosch University in South Africa. He obtained his PhD in 2011 from Tampere University of Technology in Finland under the supervision of Antti Valmari. His main research interest are in Software Engineering, specifically formal methods (model checking and process algebra), static analysis, testing, and open source software.

Title: Dynamic Program Verification

Speaker: Patrice Godefroid, Microsoft Research, USA

Abstract: I plan to informally discuss several new results. I will start with a brief update on SAGE, our whitebox fuzzing tool for security testing. SAGE has now been running for over 500 machine-years (in the Windows and Office security testing/fuzzing labs) and found many new security vulnerabilities in Microsoft code since 2007.

In 2013, for the first time, we were able to prove attacker memory safety of an entire operating-system image parser, namely the ANI Windows image parser, in only three months of work using compositional exhaustive testing (implemented in SAGE), i.e., no static analysis whatsoever. However, several key verification steps were performed manually, and our verification results depend on assumptions regarding input-dependent loop bounds, fixing a few buffer-overflow bugs, and excluding some code parts that are not memory safe by design.

Finally, my main current project is MicroX, a Virtual Machine (VM) for test isolation and generation purposes. MicroX can execute arbitrary code without any user-provided test driver or input data. It catches all memory operations *before* they occur, allocates memory on-the-fly in order to perform those read/write memory operations, and provides input values (generated randomly, with SAGE, etc.) according to a customizable memory policy, which defines what read memory accesses should be treated as inputs. MicroX is 100% dynamic, yet provides the locality and efficiency of static program analysis with the precision of dynamic analysis. I plan to present briefly this new project, strengths and limitations, and discuss applications.

Bio: Patrice Godefroid is a Principal Researcher at Microsoft Research. He received a B.S. degree in Electrical Engineering (Computer Science elective) and a Ph.D. degree in Computer Science from the University of Liege, Belgium, in 1989 and 1994 respectively. From 1994 to 2006, he worked at Bell Laboratories (part of Lucent Technologies), where he was promoted to "distinguished member of technical staff" in 2001. His research interests include program (mostly software) specification, analysis, testing and verification.

Title: MUSE: Mutation-based Precise Fault Localization Technique

Presenter: Moonzoo Kim, Korea Advanced Institute of Science and Technology, South Korea

Abstract: We present MUSE (MUtation-baSEd fault localization technique), a new fault localization technique based on mutation analysis. A key idea of MUSE is to identify a faulty statement by utilizing different characteristics of two groups of mutants–one that mutates a faulty statement and the other that mutates a correct statement. The empirical evaluation using 14 faulty versions of the five real-world programs shows that MUSE localizes a fault after reviewing 7.4 statements on average, which is about 25 times more precise than the state-of-the-art SBFL technique Op2.

Bio: Moonzoo Kim is an associate professor at the CS dept. KAIST, South Korea. His research focuses on the practical applications of software model checking, concolic testing, fault localization and concurrent program analysis techniques to detect/fix software bugs automatically. In addition, he has closely collaborated with Samsung Electronics to apply advanced testing techniques to embedded systems such as flash memory and smartphone platforms.

Title: Automatic System Testing of GUI-Based Applications

Presenter: Leonardo Mariani, University of Milano Bicocca, Italy

Abstract: Testing GUI-based applications is hard and time-consuming because it requires exploring a potentially huge execution space by interacting with the graphical interface of the applications. Manual testing can cover only a small subset of the functionality provided by applications with complex interfaces, and thus automatic techniques are necessary to extensively validate GUI-based systems. This paper presents AutoBlackTest, a technique to automatically generate test cases at the system level. AutoBlackTest uses reinforcement learning, in particular Q-Learning, to learn how to interact with the application under test and stimulate its functionalities. The empirical results show that AutoBlackTest can reveal previously unknown problems by working at the system level and interacting only through the graphical user interface

Bio: Leonardo Mariani is a researcher at the University of Milano Bicocca. He obtained his PhD from the same university and he has been visiting professor at University of Paderborn. His main research interests are in the scope of software engineering with specific focus on software testing, program analysis, inference of behavioral models, and design of self-healing solutions. Leonardo Mariani worked on several national and international research projects, including the FP7 PINCETTE project about static, dynamic and hybrid analysis techniques and the FP6 Shadows project about software self-healing. Leonardo Mariani published several papers at leading software engineering conferences and journals. He is regularly involved in the organization of leading software engineering conferences. For instance, he served in the program committees of ICSE, FSE, ISSTA and ICST and he has been co-chair of several tracks including the ICSE Doctoral Symposium.

Title: On the Probabilistic Symbolic Analysis of Software

Presenter: Corina Pasareanu, CMU/NASA Ames Research Center, USA

Abstract: Recently we have proposed symbolic execution techniques for the probabilistic analysis of programs. These techniques seek to quantify the likelihood of reaching program events of interest, e.g., assert violations. We describe recent advances in probabilistic symbolic analysis including handling of multi-threading and of complex floating point constraints and statistical techniques for increased scalability.

Bio: Corina Pasareanu is a researcher in software engineering at NASA Ames, in the Robust Software Engineering group. She is employed by Carnegie Mellon University, at the Silicon Valley campus. She is conducting research on symbolic execution and automated compositional verification with the goal of improving the reliability and safety of software developed for critical applications. Her most recent interests are in probabilistic and statistical analysis techniques for software implementations.