*********************************
There is now a CONTENT FREEZE for Mercury while we switch to a new platform. It began on Friday, March 10 at 6pm and will end on Wednesday, March 15 at noon. No new content can be created during this time, but all material in the system as of the beginning of the freeze will be migrated to the new platform, including users and groups. Functionally the new site is identical to the old one. webteam@gatech.edu
*********************************
Title: Finding Race Conditions in Kernels: the Symbolic Way and the Fuzzy Way
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.