Meng Xu

Ph.D. Candidate

School of Computer Science

College of Computing

Georgia Institute of Technology

Date: Thursday, July 16th

Time: 1:30pm - 3:00pm (EST)

Location: https://bluejeans.com/199452819 (remote)

Committee:

Dr. Taesoo Kim (Advisor), School of Computer Science, Georgia Tech

Dr. Wenke Lee, School of Computer Science, Georgia Tech

Dr. Alessandro Orso, School of Computer Science, Georgia Tech

Dr. Brendan D. Saltaformaggio, School of Electrical and Computer Engineering and School of Computer Science, Georgia Tech

Dr. Marcus Peinado, Microsoft Research

Abstract:

The scale and pervasiveness of concurrent software pose challenges

for security researchers: race conditions are more prevalent than ever, and

the growing software complexity keeps exacerbating the situation --- expanding

the arms race between security practitioners and attackers beyond memory errors.

As a consequence, we need a new generation of bug hunting tools that not only

scale well with increasingly larger codebases but also catch up with the growing

importance of race conditions.

In this dissertation, I will present two complementary bug hunting frameworks that

might meet the scalability and agility requirements: focused symbolic checking

and multi-dimensional fuzz testing, and showcase their effectiveness in a

challenging arena: OS kernels. While symbolic execution can never scale up to

the whole kernel, complete checking may nevertheless be possible in carefully

constructed program slices. I will demonstrate how precise models for race

conditions can help build such slices and enable a jumpstart of symbolic

execution from the middle of a program. On the other hand, fuzz testing turns

bug finding into a probabilistic search, but current practices restrict

themselves to one dimension only (sequential executions). I will illustrate how

to explore the concurrency dimension and extend the bug scope beyond memory

errors to the broad spectrum of concurrency bugs.