Currrent Teaching

  • Spring 2018

    18-732: Secure Software Systems

    Poor software design and engineering are the root causes of most security vulnerabilities in deployed systems today. This course will examine approaches, mechanisms, and tools used to make software systems more secure. We will motivate the study by discussing common software security threats (e.g., buffer overflow attacks and cross-site scripting). The majority of the course will be divided into four main modules: run-time enforcement of security policies (e.g., dynamic taint analysis); architectural approaches to building secure software (e.g., confinement, virtual machines, trusted computing); software analysis (e.g., static analysis and testing, model checking); and language-based approaches to building secure software (e.g., type systems, proof-carrying code). Time permitting, the course also covers topics such as the importance of usability to building secure software systems.

Thesis Committees

  • Samee Zahur, University of Virginia. Defended April, 2016.
  • Srinath Setty, University of Texas, Austin. Defended August, 2014.
  • Yinqian Zhang, University of North Carolina. Defended June, 2014.

Teaching History

  • Spring 2017

    15-811: Verifying Complex Systems

    As the world increasingly depends on software, to control our finances, drive our cars, and manage our medical devices, how can we tell whether that software will be correct, secure, or reliable? Testing for such properties is notoriously difficult and ineffective. Software verification can, in principle, provide such guarantees, but verification has historically been difficult to apply at scale. A recent series of results, however, suggests we may be at an inflection point, as various research groups have successfully proven rigorous properties about critical software components, including OS kernels, compilers, cryptographic libraries, and distributed systems.

    15-811 focuses on these recent research results, though it also covers fundamentals of verification and includes a “bootcamp” tour of multiple verification tools.

  • Spring 2016

    CSE 599W: Systems Verification

    CSE 599W was a special topics course on systems verification at the University of Washington. We examined research papers on applying formal verification techniques to building provably correct software, such as compilers, operating systems, Web browsers, and distributed systems. Co-taught with Zach Tatlock and Xi Wang.

  • Summer 2001

    English as a Second Language (ESL)

    Taught via Chester County OIC. Developed and implemented an English curriculum for a class of recent immigrants from Mexico, adapting instruction to accommodate a wide range of skill levels.