Improving the scalability and effectiveness of symbolic execution
Prof. Emilio Coppa
Sapienza University, Rome
DEIB Seminar Room "N. Schiavoni" (Bld. 20)
October 19th, 2023
2.00 pm
Contacts:
Mario Polino
Research Line:
System architectures
Sapienza University, Rome
DEIB Seminar Room "N. Schiavoni" (Bld. 20)
October 19th, 2023
2.00 pm
Contacts:
Mario Polino
Research Line:
System architectures
Sommario
On October 19th, 2023 at 2.00 pm Emilio Coppa, Assistant Professor in the Department of Computer, Control, and Management Engineering at Sapienza University of Rome, will hold a seminar on "Improving the scalability and effectiveness of symbolic execution" in DEIB Seminar Room "Nicola Schiavoni" (Building 20).
Symbolic execution is a software testing technique for automatically exploring the paths of a program. Its dynamic twist is called concolic execution, which concretely runs the program while performing the analysis. This approach provides several practical benefits, including the possibility of analyzing large and complex applications, possibly exploiting their concrete state when the symbolic analysis struggles to model specific components in their code. However, concolic execution still comes with a large analysis overhead. In this talk, after briefly reviewing some contributions made in the context of symbolic execution and their use for practical reverse engineering tasks, we discuss some novel ideas recently proposed for improving the scalability and effectiveness of modern concolic executors. From one side, we tackle the problem of efficiently building symbolic expressions during an execution, exploiting a hybrid instrumentation approach. On the other side, we present an approximate SMT solver that can help reduce the query-solving time using techniques borrowed from the fuzzing domain. Finally, we discuss some open problems in the context of hybrid fuzzing that may benefit from novel ideas and practical improvements.
Symbolic execution is a software testing technique for automatically exploring the paths of a program. Its dynamic twist is called concolic execution, which concretely runs the program while performing the analysis. This approach provides several practical benefits, including the possibility of analyzing large and complex applications, possibly exploiting their concrete state when the symbolic analysis struggles to model specific components in their code. However, concolic execution still comes with a large analysis overhead. In this talk, after briefly reviewing some contributions made in the context of symbolic execution and their use for practical reverse engineering tasks, we discuss some novel ideas recently proposed for improving the scalability and effectiveness of modern concolic executors. From one side, we tackle the problem of efficiently building symbolic expressions during an execution, exploiting a hybrid instrumentation approach. On the other side, we present an approximate SMT solver that can help reduce the query-solving time using techniques borrowed from the fuzzing domain. Finally, we discuss some open problems in the context of hybrid fuzzing that may benefit from novel ideas and practical improvements.
Biografia
Emilio Coppa (https://ecoppa.github.io/) is an assistant professor (RTD-A) in the Department of Computer, Control, and Management Engineering at Sapienza University of Rome.
He obtained a Ph.D. in Computer Science at the same university in 2015 with a thesis focused on the use of dynamic analyses for studying complex systems, ranging from single machines to big data systems. During his Postdoc, he started to use software testing techniques, such as symbolic execution and software fuzzing, in the context of cybersecurity to find vulnerabilities in real-world programs or perform reverse engineering of malware. He has authored papers and articles in several well-renowned venues, such as ESORICS, ASIACCS, DSN, ISSTA, ICSE, ASE, TOCS, TSE, PLDI, CGO, EUROSEC, and others.
He obtained a Ph.D. in Computer Science at the same university in 2015 with a thesis focused on the use of dynamic analyses for studying complex systems, ranging from single machines to big data systems. During his Postdoc, he started to use software testing techniques, such as symbolic execution and software fuzzing, in the context of cybersecurity to find vulnerabilities in real-world programs or perform reverse engineering of malware. He has authored papers and articles in several well-renowned venues, such as ESORICS, ASIACCS, DSN, ISSTA, ICSE, ASE, TOCS, TSE, PLDI, CGO, EUROSEC, and others.
