|
I am a professor in the Computer
Science Department and UMIACS at the University of Maryland,
College Park. With David Van Horn
I direct PLUM,
the lab for Programming Languages research at the
University of Maryland. I am also affiliated
with the Maryland
Cybersecurity Center (MC2), and was formerly its
Director (see our
video!). You may find it interesting to read about how we manage
PLUM.
Here is my current vita and a list
of my publications,
organized by year and by category.
I received my Ph.D. in Computer and
Information Science from the University of Pennsylvania
in August 2001, and I spent one year as a post-doctoral
associate affiliated with the Information
Assurance Institute of the Computer Science
Department at Cornell University. During academic
2008 - 2009, I was on sabbatical in Cambridge, England.
From September to November I was at Microsoft
Research and from December to August 2009 I was at
the University of
Cambridge Computer Laboratory. I was the director of
MC2 from October 2011 to 2013. During the Summer of 2015 I
visited Microsoft Research in Redmond.
How fast
can you type? (My best so far is 108 wpm.)
Research
My primary research interest is to develop and evaluate
techniques to improve software availability, reliability,
and security. I am currently working on a number of
projects.
Secure programming - How do we build
software that is secure? We have been
developing a contest, called build-it,
break-it, fix-it whose aim to
test how well students can build software
securely. We have now offered the contest several
times (including many times in classes at UMD and
elsewhere) and have some interesting
data analysis of what strategies work and
don't work for building and breaking. We are
working on a more
in-depth analysis of contest data, and plan
controlled studies to further test hypotheses. One
clear outcome, previously known but confirmed by
the contest, is that programming in C and C++ is
risky. I have been working with Microsoft on Checked
C, an extension to C aimed to provide
safety. Checked
C is specifically designed to ease the porting
of legacy code.
|
| Protecting against information
leakage - How do we avoid leaking
information via observable behavior? We are
developing novel static
analyses and tools
to identify when a program might be leaking
sensitive information via its direct outputs,
running time, space usage, address/IO trace, and
more. We have recently developed LWeb,
a novel Haskell-based framework for preventing
leaks in web applications. We are also exploring
the use of fuzz
testing. Finally, we have implemented
approaches using probabilistic
abstract interpretation for enforcing
quantitative knowledge-based policies that
protect static and time-varying
secrets, and have recently looked at uses
of sampling to improve precision. |
Quantum computation programming languages
- means to develop reliable and efficient
quantum programs on near-term devices. We
are looking at the challenge of developing
high-quality quantum
programs despite limited, noisy resources on
quantum computers available in the near term. We
are applying ideas from program verification and approximate
computing.
|
| Blending programming languages
and cryptography - means of implementing
privacy-preserving or integrity-assuring
computation through the combination of
programming languages and cryptographic
techniques. I have looked at languages and
analyses for secure multiparty computation,
most notably a new programming language called Wysteria,
and a follow-on language Wys*
for proving properties of multi-party
computations. I have also developed novel
mechanisms for cloud-based computations involving
general-purpose authenticated
data structures and compiler-optimized
oblivious RAM. |
| Dynamic software updating
(DSU) - means to safely, efficiently, and
flexibly update running code. We have
developed general-purpose methods for updating C
and Java programs, and are currently considering
means to update controllers in software-defined
networks. Our system for dynamically updating C
code is called Kitsune
and our system for Java is called Rubah;
the code and benchmarks for both are freely
available. I have recently considered DSU for key-value
stores and software-defined
networks. I have also worked to improve
the reliability of dynamic updates through
application of multi-version execution.
Earlier work and papers are described here.
|
Previously, I was involved in the following projects:
- Adapton,
a library for incremental computation --- the idea is to
write an algorithm largely as usual, but then to derive
a version that can incrementally update the output
following a small changes to its input.
- Expositor,
a library for writing dynamic analyses to assist in
debugging, taking advantage of record/replay support.
- Diamondback
Ruby, static and hybrid static/dynamic type system
for the Ruby scripting language.
- Otter,
a symbolic executor for C programs.
- LockSmith,
a static analysis tool for proving the absence of race
conditions in C programs.
- Path
Projection, a browser-based UI toolkit for
presenting, navigating, and querying paths
emitted as static analysis results; we applied it to
Locksmith.
- Cyclone,
a safe dialect of C. Cyclone's system for manual memory
management was influential in the development of Rust.
- I have also looked at means for customized,
language-enforced security policies, implemented in a
web programming language, SELinks,
and automatically inserted by a compiler called Coco.
- MGRP,
for measurement-aware data transport and
kernel-based rootkit detection.
Links to all past projects may be found on the PLUM home
page.
Research Group
Current students and postdocs:
Previous students and postdocs:
| Andrew
Ruef |
Tools
and Experiments for Software Security
Researcher at IDA/CCS
since February 2019 |
| Chang
Liu**** |
Trace
Oblivious Program Execution
Post-doc at UC Berkeley, 2016-2018;
researcher at Citadel Securities since 2019
|
| Shiyi Wei
(postdoc) |
Assistant Professor, University of
Texas at Dallas, since August 2017 |
| Aseem
Rastogi |
Language-based
Techniques for Practical and Trustworthy
Secure Multi-Party Computations
Researcher at Microsoft
Research India since June 2016
|
| Matthew
Hammer (postdoc) |
Research scientist at DFinity since
January 2019; previously Assistant Professor, University
of Colorado, Boulder, August 2015-January
2019
|
| Luís Pina*** |
Practical
Dynamic Software Updating (for Java)
Assistant Professor at University of Illinois,
Chicago, starting Fall'19; previously post-doc
at George Mason (Aug 2017-19) and Imperial
College, London (Mar 2015-Aug 2017)
|
| Karla Saur* |
Dynamic
Upgrades for High Availability Systems
Senior Software Engineer at
Microsoft since October 2018; previously
researcher at Intel
Labs September 2015-2018
|
| Piotr
Mardziel |
Modeling,
Measuring, and Limiting Adversary Knowledge
Systems Scientist at CMU
(previously, post-doc) since June 2016; post-doc
at UMD Jan'15 - Jun'16
|
| James Parker
(MS) |
LMonad:
Information Flow Control for Haskell Web
Applications
Research programmer at UMD
January 2015-2019, now PhD student at UMD,
part-time software research engineer, Galois
|
Nate
Parsons (MS)
|
Implementing and Typing a
Core Calculus for Mixed-mode Secure
Multi-party Computations (scholarly paper)
Missions software engineer at Planet since
2013; previously, engineer at JHUAPL
|
| Khoo
Yit Phang* |
User-centered
Program Analysis Tools
Principal Software Engineer at MathWorks
since August 2013
|
| Nataliya
Guts (postdoc) |
|
| Chris
Hayden* |
Clear,
Correct, and Efficient Dynamic Software
Updates
Software Engineer at SocialCode
since Dec. 2015 (at WaPo Labs/Trove
2012-2015)
|
| Ted
Smith (undergrad)* |
Insight
Deliveryperson, Bloomberg LP, since 2019;
Software Engineer, Google, 2016-2018; grad
student at UMass Amherst 2013-2016
|
| Stephen
Magill (postdoc) |
Principal scientist, Galois, since
2014 (at IDA/CCS, 2012-2014) |
| Justin
McCann |
Automating
Performance Diagnosis in Networked Systems
Avere
Systems since July 2012
|
| Martin
Ma* |
Improving Program Testing and Understanding
via Symbolic Execution
Software Engineer at Google since
2013 (previously at Amazon)
|
| Saurabh
Srivastava* |
Satisfiability-based
Program Reasoning and Program Synthesis
Founder, Synthetic
Minds, since 2017; founder, 20n, 2013-2017;
post-doc at Berkeley 2012-2014
|
| Pavlos
Papageorgiou |
The
Measurement Manager: Modular and Efficient
End-to-end Measurement Services
Software Engineer, Google (AI),
since December 2008
|
| Iulian
Neamtiu |
Practical
Dynamic Software Updating
Assoc. Prof, NJIT, since
Fall 2015 (at UC
Riverside, 2008-2015).
|
| Manuel
Oriol (postdoc) |
Principal Scientist, R&D
manager at ABB Switzerland Ltd. since Fall 2011;
Senior Lecturer, University of
York (UK), 2008-2014 |
| Polyvios
Pratikakis* |
Sound,
precise, and efficient static race detection
for multithreaded programs
Assistant professor in CS, University
of Crete, since 2014; researcher, Institute of
Computer Science, FORTH, 2010-2014;
post-doc at CNRS/VERIMAG 2008-2009
|
| Nikhil
Swamy |
Language-based
Enforcement of User-defined Security
Policies as Applied to Multi-tier Web
Applications
Senior Researcher, Microsoft
Research, Redmond, since Fall 2008
|
| Nick
L.
Petroni** |
Property-based
Integrity Monitoring of Operating System
Kernels
Chief scientist, Volexity,
since 2015; research scientist, IDA/CCS
2008-2015
|
|
I have also worked closely with Niki Vazou
(postdoc supervised by David Van Horn), David Darais
(advised by David
Van Horn), Andrew Miller
(co-advised with Jon Katz and Elaine Shi), Avik Chaudhuri,
Mike Furr, David An,
and Elnatan Reisner (advised by Jeff Foster),
Adam Bender
(advised by Bobby Bhattacharjee), Jaime Spacco
(advised by Bill Pugh), and Suriya
Subramanian (advised by Kathryn
McKinley while at UT Austin). I have previously
advised Willem Wyndham, Jonathan Turpie (now at Amazon), Brian Corcoran
(now at Palantir), Eric Hardisty,
and James Rose (now at Google). I've also worked with
post-grad Patrick Jenkins, undergrad Jeff Meister,
and high school students, Ted Smith (from Walt Whitman
High), and George Kleses, Matt McCutchen, and
Cody
Burton (from Montgomery Blair). Both Ted and Matt
later became undergraduate students in our Department and
Ted, Matt, and Cody all went to graduate school (at UMass,
MIT CSAIL, and MIT Physics, respectively).
Teaching
- CMSC 330 (Organization of Programming Languages) Spring
2019, Spring
2018, Spring
2017, Fall
2015, Spring
2015, Spring
2013, Spring
2010
- CMSC 631 (Program Analysis and Understanding) Fall
2017, Spring
2013, Fall
2011, Fall
2009, Fall
2007 and Fall
2006
- CMSC
396H, Honors Research Seminar, Fall 2016
- CMSC 838G Mechanized
Proof and Verified Software, Spring 2016
- Software
Security, hosted by Coursera, since late Fall 2014
- CMSC 838G (Software Security)
Spring 2014 and Spring 2011
- CMSC 433 (Programming Language Technologies and
Paradigms) Fall
2014, Fall
2013, Fall
2010, Spring
2006, Fall
2003, Fall
2002
- CMSC
498L (Cybersecurity Lab), Fall 2012
- CMSC
498B (Secure Maryland - pen testing), Spring 2012
- CMSC 412 (Operating Systems) Spring
2007, Fall
2005, Fall
2004
- CMSC
838Z
(Language-Based Security) Spring 2005
- CMSC
838Z
(Tools and Techniques for Software Dependability)
Spring 2004
- CMSC
838Y
(Agile and Adaptive Programming Systems) Spring
2003
Professional Activities
I am the past Chair of ACM
SIGPLAN (served July 2015-2018); I was an Associate
Editor for TOPLAS
from 2012-2016; and I have served (or am serving) on the
following committees
| 2019 |
POPL
SRC, ASPLOS
(ERC), SNAPL,
CCS
(AC), SecDev
|
| 2018 |
POST,
S&P
(AC), SecDev
|
| 2017 |
S&P,
ESSoS, CCS,
USENIX
ASE, SecDev
|
| 2016 |
PLDI,
CSF
(PC co-chair), USENIX
ASE, SecDev
(PC chair), CSAW
judge
|
| 2015 |
S&P, CSF (PC
co-chair), SNAPL |
| 2014 |
OBT,
CSF, OOPSLA/SPLASH |
| 2013 |
POPL
(ERC), PLDI |
| 2012 |
POPL
(program chair), HotSWUp
|
| 2011 |
TLDI,
HotSWUp
(co-organizer), OOPSLA |
| 2010 |
ESOP,
PLDI
(ERC and tutorials chair), ICFP (PC
and local arrangements), PASTE |
| 2009 |
POPL,
S&P,
PLDI
SRC |
| 2008 |
CCS,
CATARS,
COORDINATION,
ISMM
(ERC) |
| 2007 |
PLAS
(general and program chair), OOPSLA,
COORDINATION,
PLDI |
| 2006 |
FTfJP,
PLAS,
SPACE,
OOPS
(part of SAC
2006) |
| 2005 |
SCOOL,
VEE
|
| 2004 |
IWAN,
ICPP,
FUSE
|
| 2003 |
IWAN,
USE
|
| 2002 |
IWAN,
USE
|
| 2001 |
IWAN |
|
|
|
|