Thomas E. Hart :: Projects
Home

Toronto Weather Toronto.com

The Hunger Site

Research
  Projects
  Publications
  Masters Thesis

School
  Education
  Teaching

Personal
  Blog
  Pictures
  Links

Research Interests

My main research interest is the application of program analysis techniques to computer security; specifically, using these techniques to both find vulnerabilities and prove their absence. These techniques enhance security without relying on expensive or ad-hoc runtime checking. I'm also interested in issues related to concurrency and synchronization, notably lockless algorithms, and in operating systems.

Current Work

I am currently working on proving the absence of buffer overflows in open source software, under the supervision of David Lie and Marsha Chechik. Our first contribution is the Verisec suite, a benchmark for detecting buffer overflows and verifying their absence with CEGAR-based software model checkers. The examples are taken from real CVE entries, and are broken down into variable-complexity examples.

Our experience with the Verisec suite has led us to believe that finding paths to out-of-bounds writes can be very complex, in-bounds buffer accesses are often safe for very simple reasons which can be captured by proof templates. Our work on adding proof templates for array bounds checking to CEGAR software model checkers appears at ASE'08.

Masters Thesis

My Masters thesis investigated the performance of three memory reclamation schemes that can be used with lock-free and concurrently-readable algorithms. In a nutshell, I examined current research with non-blocking synchronization and read-copy update, and tried to set out how it all relates to one another, how we can mix-and-match the techniques, and what the consequences are. I describe this more formally on a separate page.

This research resulted in a paper which won a Best Paper award at IPDPS 2006. The paper thoroughly analyzed the performance tradeoffs between quiescent-state-based reclamation, hazard pointers, and epoch-based reclamation.

I was supervised during my Masters work by Angela Demke Brown. Paul McKenney was a close collaborator. Others are acknowledged in the text of my thesis.

Other Research Projects

I worked with Andres Lagar Cavilla, Gerard Baron, Lionel Litty, and Eyal de Lara on a project to create a model to accurately simulate ad hoc networking protocols with users moving indoors.

Back at Brandon University, I worked on messy broadcasting with Hovhannes Harutyunyan. I later worked with Chenkuan Li on an average-case analysis of messy broadcasting. I've got some old pages describing (theoretical) broadcasting in general here.

Both projects resulted in some publications.

Other Projects

Also while at Brandon University, I worked for Gerald Dueck on a database for the Manitoba Agricultural Museum.

I'm a co-author of the GNU/Hurd User's Guide. The Hurd helped kindle my interest in microkernel research and novel operating system designs.

last update on Fri Jul 25 11:52:18 2008 University of Toronto :: Department of Computer Science