Research Interests
I study programming languages and computer security. Most recently,
my work has focused on two research directions: (1) memory safety of
low-level software, and (2) Coq verification of LLVM program
transformations. I have also spent a lot of time thinking about
language-based enforcement of information-flow policies,
understanding dynamic security policies, and authorization
logic. I am also interested in secure concurrent and distributed
computing, functional programming languages, type theory, linear and
modal logics, theorem proving and mechanized metatheory. More
information about my research can be found in this (out of date) research statement.
Conferences and News
Current Research Projects and Activities
|
PL Club
Penn's programming languages research group, run jointly with Benjamin Pierce and Stephanie Weirich. We
meet weekly with students and post-docs to discuss current research topics.
|
|
Vellvm
The verified LLVM project is developing operational semantics
for the LLVM intermediate
representation using the interactive theorem prover Coq. The resulting tools let us
create highly-reliable program transformation passes and optimizations.
|
|
SoftBound + CETS
This project is developing software instrumentation techniques to
achieve complete memory safety for C programs, while requiring
minimal changes to the source programs.
|
|
Security-Oriented
Languages
This research seeks to develop programming language abstractions
and analyses that let developers create programs that are secure by
construction.
|
- Programming Languages and Techniques I (CIS 120)
2011,
2010
- Compilers (CIS 341)
2011
, 2008
- Software and Compiler Verification (CIS 700)
2005
- Computer and Network Security (CIS 551)
2012
,
2009
,
2008
,
2007
,
2006
,
2005
- Introduction to Networks and Security (CSE 331)
2006
,
2004
,
2003
,
2002
- π-Calculus and Foundations of
Concurrent Systems (CIS 700)
2004
- Advanced Topics in PL: Safety and Security (CIS 670)
2003
Students
Current Ph.D. Students and Post Docs
Former Ph.D. Students and Post Docs
-
Jeff Vaughan
(Ph.D. 2009, now a post doc at UCLA)
-
Limin Jia, Ph.D.
(post doc 2007-2009, now at CMU)
-
Peng Li
(Ph.D. 2008, now at Google)
-
Stephen Tse
(Ph.D. 2007, now at a startup)
Awards and Honors
- Alfred P. Sloan Fellow, 2009-2010
- NSF CAREER award, 2004
- Best Paper award at SOSP, 2001
- Intel Foundation Graduate Fellowship, 2001
- Best Paper award at ICFP, 1999
- NSF Graduate Student Fellowship, 1996
Funding
My research has been supported in part by the following grants. Any
opinions, findings, and conclusions or recommendations expressed in
this material are those of the author(s) and do not necessarily
reflect the views of the National Science Foundation.
- NSF: Dynamic Security Policies
- NSF: CAREER: Language-based Distributed
System Security
- ONR: TIME-DC
- NSF: Resource-guided Implementation
of Secure Embedded Software
- NSF:
Flexible, Decentralized Infomation-flow Control
for Dynamic Environments
- NSF CRI: Machine Assistance for
Programming Language Research
- NSF CCF: Unifying Events and Threads:
Language Support for Network Services
- NSF CT-T: Collaborative Research: Manifest
Security
- DARPA: Machine-checked Metatheory for Security-oriented Languages
- ONR: Networks Opposing Botnets
- NSF SHF: Practical Linear Types for Safe Protocols
- NSF CCF: Validating Program Transformations in a Mechanized
LLVM
- ONR: Ironclad C/C++: Enforcing Memory Safety to Prevent
Low-level Security Vulnerabilities
- NSF TC: WATCHDOG: Hardware-Assisted Prevention of All Use-After-Free Security Vulnerabilities
|