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.
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
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
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
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,
Lionel Litty, and
Eyal de Lara on a project to
create a model to accurately simulate ad hoc networking protocols with users
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
Both projects resulted in some
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.