Over the last decades, dynamic symbolic execution (symbex) emerged as one of promising automated approaches to software testing and analysis. It has been applied to automatically test system-level software, software patches, network stack, verify functional equivalence, and more. Tools based on flavors of symbex were even successfully used to test Microsoft Office and in the prestigious DARPA’s Cyber Grand Challenge competition.
However, scalability limitations attributed to symbex, as well as the complex nature of the technique have been clipping its wings and limiting its wider adoption. At the same time, over the last decade fuzzing has been booming and became a de-facto standard for automated testing. Why has symbex not seen the success and widespread adoption similar to fuzzing? Why a technique with stronger guarantees and reasoning power is not the first choice for testing in industry?
In this keynote we share some thoughts and lessons learned on how to help symbolic execution SOAR by making it Selective, Open-source, Approachable and Real-world. We showcase several research projects in which we enhanced symbex to achieve greater scalability and fitness for the purpose. Furthermore, we discuss how different perspectives in academia and industry affect the way techniques are developed, evaluated and used. Finally we try to estimate where symbex stands on the road to becoming commonplace.
Tomasz Kuchta is a computer scientist striving to make computer systems reliable and secure. He is a member of Samsung’s Mobile Security Team in Warsaw where he works on research, development of automation tools and security assessment of the latest flagship devices. In the past, Tomasz helped secure mobile products at Qualcomm and built base stations control software at Motorola. He holds a PhD in computing from Imperial College London. His research spans novel applications of symbolic execution, software reliability and easier testing of complex software systems.
Mon 15 AprDisplayed time zone: Lisbon change
16:00 - 17:30 | Binary Analysis & KeynoteKLEE at Maria Helena Vieira da Silva Chair(s): Daniel Schemmel Imperial College London | ||
16:00 22mTalk | What’s Up from Below? An Overview of Recent Advances in BINSEC KLEE | ||
16:22 22mTalk | Symbolic Execution of Binary Code based on Formal ISA Semantics KLEE P: Sören Tempel University of Bremen, Tobias Brandt Independent, Christoph Lüth University of Bremen / DFKI GmbH, Rolf Drechsler University of Bremen / DFKI GmbH | ||
16:44 46mKeynote | Let's help symbolic execution SOAR! KLEE Tomasz Kuchta Samsung Electronics |