Symbolic Execution

Multimodal Seminar in Symbolic Execution

Symbolic execution is a powerful program analysis technique based on the idea to execute a program with symbolic placeholders instead of concrete inputs. Since this principle enables exploring many program paths at once, it has been used for intensive software testing and full program proving. The most significant obstacles symbolic execution is facing are path explosion (a new program path is spawned at every case distinction) and the overhead due to constraint solving. In the focus of the seminar are the basic principles of symbolic execution and approaches for mitigating the aforementioned problems.

Only five students can participate in this intensive seminar.

Registration: To register, use the central system of the CS department.

Organization

This seminar consists of ten regular sessions held during the semester and a final block session. Each regular session is either a lecture, paper, or lab session.

In lecture sessions, the students are given an introduction into general topics (giving talks) and the specific course topic (symbolic execution).

In paper sessions, one or two students present different papers on the topic of symbolic execution. These presentations only take five minutes and are not graded. The purpose of this is to reflect on presentation style and to provide a high-level overview for kickstarting the upcoming lab session(s). In advance of each paper session, each student (regardless of whether or not they present a paper in that session) is requested to submit a brief summary of the paper.

Lab sessions aim to solidify the gained theoretical knowledge by practical application. Each student is supposed to solve an appropriately sized programming exercise related to the topic of the lab session (and the preceding paper session) in advance of the session. In the session itself, one student presents their solution and the gained insights in a short presentation; afterward, a discussion of the implemented technique follows. After the regular sessions, each student will have presented one paper and one lab session in brief talks, and will have submitted summaries for up to five (but no less than four) papers.

Finally, each student presents theoretical and practical aspects of one symbolic execution topic in a final block session. The topics are those of the papers discussed in the regular sessions; but each student shall present a different topic than the one they have already presented.

Grading

The grade is built from the final talk (50%) and all submitted lab solutions (50%, i.e., 10% for each submitted solution). Each student has one “joker” for the lab solutions: The worst individual grade for a lab solution (including missed submissions) is replaced by the best obtained such grade. To pass the seminar, it is mandatory to (1) attend all seminar sessions, unless a student is absent due to illness, (2) submit at least four short summaries, (3) give one short talk on a paper and one on a lab topic, (3) submit at least four lab solutions, (4) give a final presentation, and (5) obtain at least 50% of the maximum number of points that can be achieved in the final talk and the lab solutions.

Requirements

While not a formal prerequisite, a relatively solid knowledge of Python is highly recommended for the lab sessions, or otherwise should be acquired until one week before the first lab session.

Registration

Please register via the central seminar assignment page: https://seminars.cs.uni-saarland.de/seminars22

Preliminary Course Plan

1. [Lecture] How to Give a Research Talk (Andreas)
2. [Lecture] Introduction to Symbolic Execution & Constructing a Symbolic Interpreter [Lab Kick-Off] Warm-Up: Extending the Symbolic Interpreter
3. [Lab Discussion/Paper/Lab Kick-Off] Concolic Execution [3]
4. [Lab Discussion/Paper/Lab Kick-Off] Selective Symbolic Execution [1]
5. [Lab Discussion/Paper/Lab Kick-Off] Compositional SE [2]
6. [Lab Discussion/Paper/Lab Kick-Off] SE by Compilation [4]
7. [Lab Discussion/Paper/Lab Kick-Off] Hybrid Fuzzing [5]
8. Final Discussions

Finals: One long presentation about a different topic than in the previous presentation, involving aspects from the paper and insights from the implementation.

Papers

1. Vitaly Chipounov, Volodymyr Kuznetsov, and George Candea. 2011. S2E: A Platform for In-Vivo Multi-Path Analysis of Software Systems. In Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2011, Newport Beach, CA, USA, March 5-11, 2011, ACM, 265–278. DOI:https://doi.org/10.1145/1950365.1950396
2. Patrice Godefroid. 2007. Compositional Dynamic Test Generation. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, ACM, 47–54. DOI:https://doi.org/10.1145/1190216.1190226
3. Patrice Godefroid, Michael Y. Levin, and David A. Molnar. 2008. Automated Whitebox Fuzz Testing. In Proceedings of the Network and Distributed System Security Symposium, NDSS 2008, San Diego, California, USA, 10th February - 13th February 2008, The Internet Society. Retrieved from https://www.ndss-symposium.org/ndss2008/automated-whitebox-fuzz-testing/
4. Sebastian Poeplau and Aurélien Francillon. 2020. Symbolic execution with SymCC: Don’t interpret, compile! In 29th USENIX Security Symposium, USENIX Security 2020, August 12-14, 2020, USENIX Association, 181–198. Retrieved from https://www.usenix.org/conference/usenixsecurity20/presentation/poeplau
5. Nick Stephens, John Grosen, Christopher Salls, Andrew Dutcher, Ruoyu Wang, Jacopo Corbetta, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna. 2016. Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In 23rd Annual Network and Distributed System Security Symposium, NDSS 2016, San Diego, California, USA, February 21-24, 2016, The Internet Society. Retrieved from https://sites.cs.ucsb.edu/~vigna/publications/2016_NDSS_Driller.pdf