Keynotes

Abstract: Dynamic Symbolic Execution emerged in the mid-2000 and was rapidly adopted by the research community as a tool of choice for bug hunting. In this talk, we will focus on security concerns and binary-level vulnerability issues. We will show some challenges symbolic execution faces in this field of application, and report on several results and achievements carried out within the BINSEC group to adapt symbolic execution to these challenges.

Bio: Sébastien Bardin is a full-time senior researcher at CEA LIST, where he has initiated and now leads the binary-level security analysis group. His research interests lay at the crossroad of formal methods, program analysis, automated reasoning, software engineering and security. For a few years now, Sébastien has been interested in automating binary-level security analysis by lifting formal methods developed for the safety-critical industry. More especially, he focuses on binary-level formal methods, vulnerability detection & assessment and malware analysis. He is the main designer of the (open-source) BINSEC platform for binary-level code analysis. He regularly publishes articles in top-ranked international conferences in Security, Formal Methods, Software Engineering and Automated Reasoning. Sébastien holds a PhD from Ecole Normale Supérieure de Cachan (2005). He is an ACM Senior Member and a CEA Fellow.

Abstract: In 2022, the Competition on Software Verification (SV-COMP) was for the first time dominated by a tool based on symbolic execution. The tool is called Symbiotic and uses symbolic executors KLEE and SlowBeast as crucial components. In the first part of the talk, we describe the architecture and workflow of Symbiotic. The second part of the talk focuses on methods implemented in SlowBeast, in particular backward symbolic execution (and its relation to k-induction) and loop folding.

Bio: Jan Strejček is an associated professor at Masaryk university (Brno, Czech Republic). He contributes to research in three areas of formal methods, namely automata over infinite words, SMT-solving, and automated program analysis. Students under his supervision developed recognized tools for automata handling (LTL3BA and Seminator), SMT-solving of bitvector logic (Q3B), DQBF-solving (DQBDD), program slicing (DG), software verification and test generation (Symbiotic, SlowBeast).

Abstract: S2E is a platform for in-vivo analysis of software systems that combines a virtual machine with symbolic execution. Users install and run in S2E an unmodified software stack, including programs, libraries, the OS kernel, and drivers. Symbolic execution then automatically explores thousands of paths through the system, allowing users to check desired properties in corner-case situations and at any level of the software stack. S2E works on unmodified binaries, does not require writing code in special languages, or model the environment. In this talk, we will reflect on what S2E achieved since its inception twelve years ago and present future development plans. We will dive into the challenges that we faced at Cyberhaven turning a research prototype into production-quality software. We will show how we built an automated exploit generator to compete in the DARPA CyberGrandChallenge. Then, how we implemented an office document malware detector that scanned over a million e-mail attachments and found threats missed by all other antiviruses. We will explain how we tried to commercialize these technologies and how the lessons learned inspired our current product that protects enterprises against IP theft and insider threats.

Bio: Vitaly Chipounov is co-founder and chief architect at Cyberhaven, where he is building a novel security product that keeps enterprise data safe from IP theft and insider threats. He got his MSc and PhD at EPFL, Switzerland, at the Dependable Systems Laboratory led by Prof. George Candea. During his PhD, he built S2E - a platform for multi-path analysis of software systems - currently used by researchers and companies around the world to build tools that find bugs and security vulnerabilities in computer systems.

Abstract: Symbolic execution can be a sophisticated bug-finding methodology, or an elaborate way of burning AWS credits. Knowing which is not always possible at the outset. That clever change to your state exploration strategy could make or break your budget. The solution, however, might just be staring back at you in the mirror! There is an under-appreciated source of “oracle-level knowledge” in symbolic execution research: human experts. Humans have an uncanny ability to identify bugs, be it via their big brains and/or the determined application of mutually-incompatible tools. The necessity of human bug-finders is also what makes working with their bugs challenging: human-found bugs don’t always fit the mould of easy-to-evaluate binary predicates like “crashes program” or “causes integer overflow.” It’s a paradox: what human bug-finders are looking for isn’t knowable until it has already been found. This paradox elucidates a tautology: symbolic executors only know how to find what they are looking for. Bridging this gap will require the work of multiple PhDs and may be impossible. In the meantime though, industry accepts the need for human bug-finders. How then are we as symbolic execution researchers making human bug-finders more productive?

Bio: Peter Goodman is a Staff Engineer in the Research and Engineering practice at Trail of Bits, where he leads all de/compilation efforts. He is the creator of various static and dynamic program analysis tools, ranging from the Remill library for lifting machine code into LLVM bitcode, to the GRR snapshot/record/replay-based fuzzer. When Peter isn’t writing code, he’s mentoring a fleet of interns to push the envelope. Peter holds a Master’s in Computer Science from the University of Toronto.