When and where

Mon 10 Jul 2017, 9:00 am, at Bren Hall 1414.

Abstract

Recent years have seen dramatic improvements in our ability to synthesize non-trivial functions. These advances have been made possible by a combination of new algorithms and increased computing power. Just as important as these, however, has been a new appreciation for how synthesis capabilities can be brought to bear on relevant and challenging problems, some of which do not even look like synthesis problems at first sight.

This talk will summarize the current state of the art in program synthesis and highlight some of the open problems in the field and some of the applications currently being explored. The talk will focus on the work of the Computer Aided Programming group at MIT, but will also highlight some of the key results from other groups that have made recent progress possible.

Bio

Armando Solar-Lezama is an associate professor at MIT where he leads the Computer Aided Programming Group. His research interests include software synthesis and its applications in diverse areas such as high-performance computing, information flow security and probabilistic programming.

More info

https://conf.researchr.org/event/issta-2017/issta-2017-keynotes-keynote-talk-advances-and-challenges-in-program-synthesis

When and where

Tue 9 Jul 2017, 9:00 am, at Bren Hall 1414.

Abstract

Embedded devices have become ubiquitous, and they are used in a range of privacy-sensitive and security-critical applications. Most of these devices run proprietary software (firmware), and little documentation is available about the software’s inner workings. Firmware, like any piece of software, is susceptible to a wide range of errors. These include memory corruption bugs, command injection vulnerabilities, and application logic flaws. Embedded device vendors typically do not provide source code for their proprietary firmware. Hence, all analysis has to be performed directly on binary code. This is challenging because binary code lacks the high-level, semantically rich information about data structures and control constructs that are present in a program’s source code. To address the analysis challenges, we have developed angr. angr is an open-source binary analysis platform that implements many static analysis techniques and supports symbolic execution of binaries.

In this talk, we will discuss some of the inner workings and design choices in angr. A common limitation of many contemporary techniques to detect vulnerabilities in binary code is that they only find shallow bugs and struggle to exercise deeper code paths. To drive the analysis deeper into a program, we introduce novel techniques to improve the scalability of our system. These techniques frequently rely on interesting compositions of different analysis approaches, in a way that leverages the advantages of each individual approach while compensating for their respective limitations. We will also cover a novel detection model that allows us to identify authentication bypass vulnerabilities (or, less formally, backdoors), an important class of logic flaws. To automatically find backdoors, we introduce the concept of input determinism, which captures an attacker’s ability to determine the input necessary to execute privileged operations of the device. Finally, we will shed some light on angr as an integral component in the automated vulnerability finding, exploitation, and patching engine that participates in DARPA’s Cyber Grand Challenge (CGC), the first competition where autonomous programs participate in a capture-the-flag competition.

Bio

Christopher Kruegel is a Professor of Computer Science at UC Santa Barbara. He is also a co-founder of Lastline, a company that develops innovative solutions to detect and mitigate advanced malware (APTs) and targeted threats. Christopher’s research interests focus on computer and communications security, with an emphasis on malware analysis and detection, web security, and intrusion detection. He has published more than 100 peer-reviewed papers in top computer security conferences and has been the recipient of the NSF CAREER Award, MIT Technology Review TR35 Award for young innovators, IBM Faculty Award, and several best paper awards. He regularly serves on program committees of leading computer security conferences and speaks at industry venues such as BlackHat and RSAC.

More info

https://conf.researchr.org/event/issta-2017/issta-2017-keynotes-keynote-talk-finding-vulnerabilities-in-embedded-software

The following article, published in the ISSTA 2007 Proceedings, has been selected to receive the ISSTA 2017 Impact Paper Award:

• James Clause, Wanchun Li, and Alessandro Orso. Dytan: a generic dynamic taint analysis framework.

See the technical research program for more details.

The following papers have received the ACM SIGSOFT Distinguished Paper Award:

• Lisa Nguyen Quang Do, Karim Ali, Benjamin Livshits, Eric Bodden, Justin Smith and Emerson Murphy-Hill. Just-in-Time Static Analysis.

• Bo Wang, Yingfei Xiong, Yangqingwei Shi, Lu Zhang and Dan Hao. Faster Mutation Analysis via Equivalence Modulo States.

• Sonal Mahajan, Abdulmajeed Alameer, Phil McMinn and William G.J. Halfond. Automated Repair of Layout Cross Browser Issues Using Search-Based Techniques.

See more details in the research track program.

Abstract: Testing cyber-physical systems presents a unique set of testing challenges: heterogeneity, timing, and, especially, observability. In particular, some of the mechanisms that are designed to make embedded software robust are the same mechanisms that present challenges for automated testing techniques: e.g., rate limiting, fault masking, and debounce logic, which can lead to long lags between problematic inputs and their manifestation in system outputs. In addition, much of the control behavior of CPS is mathematically intensive more than “branchy”. For such systems, traditional coverage metrics, which focus on reaching program statements or mutants (as in weak mutation), rather than observing their affect on system outputs, are likely to lead to poor fault-finding in practice. I will describe some recent work in the area of test generation and code metrics that begins to address these issues.

I then argue that this mismatch will become significantly worse for when examining CPS systems that incorporate machine learning: the complexity of the non-linear mathematics used defeats all known symbolic techniques and the lack of a traditional branching structure renders traditional code coverage metrics fairly meaningless when using search-based testing. In fact, a recent paper abstract claims: “We propose a novel control flow obfuscation design based on the incomprehensibility of artificial neural networks to fight against reverse engineering tools including concolic testing.” Traditional testing of such systems has focused on checking their behavior against a large corpus of examples; unfortunately, it is known that such systems are often not robust against malicious inputs even after extensive training and testing. I hope to challenge participants to focus research into such mathematically intensive systems and to begin to create rigorous metrics that are applicable to such systems.

Biography: Dr. Michael Whalen is the Director of the University of Minnesota Software Engineering Center and the Director of Graduate Studies for the Masters of Science in Software Engineering (MSSE) program. He has more than 20 years of experience in software development and analysis, including 15 years of experience in Model-Based Development & safety-critical systems. Dr. Whalen has developed simulation, translation, testing, and formal analysis tools for Model-Based Development languages including Simulink, Stateflow, Lustre, and RSML-e. He has led successful large-scale formal verification projects on industrial avionics systems, including displays (Rockwell-Collins ADGS-2100 Window Manager, deployed on the Boeing 787), redundancy management and control allocation (AFRL CerTA FCS program) and autoland (AFRL CerTA CPD program). Dr. Whalen was the lead developer of the Rockwell-Collins Gryphon tool suite, which was used for compilation, test-case generation, and formal analysis of Simulink/Stateflow models. He is currently working on the AGREE tool suite for architectural analysis and testing in AADL, which was recently used to verify correct system behavior in the Boeing Little Bird autonomous helicopter as part of the DARPA HACMS project.

ISSTA registration is open! See the registration and accommodation info. Hope to see you in Santa Barbara in July!

Check out our week overview!

SPIN, ISSTA, and RERS registration is now open! Visit the ISSTA Registration site to register and reserve your accommodations. On-campus accommodations, both shared and private, are available, but limited in number. So hurry to book them! Nearby off-campus choices are also available.

SPIN will be held at the University of California, Santa Barbara. For information on the venue and travel to Santa Barbara, visit this ISSTA page.

This year we accepted 16 full and 5 short papers out of 46 submissions. You can find the list of accepted papers here.

We have extended the paper submission deadline by one week to Friday, February 17. We have also pushed back the author notification date to April 20, 2017. There is no change to the Camera Ready version deadline.

SPIN organizers will accommodate, via alternative means of presentation, the authors of accepted papers if they are affected by the recent travel restrictions to the USA.

Our organizational sponsor, Association of Computing Machinery (ACM), has provided a statement on this issue. You may view it here.