Greg Morrisett
Allen B. Cutting Professor of Computer Science
|
|
Research Interests
My research focuses on the application of programming language technology for building secure and reliable software systems. In particular, I am interested in applications of advanced type systems, model checkers, certifying compilers, proof-carrying code, and inlined reference monitors for building efficient and provably secure systems. I am also interested in the design and application of high-level languages for new or emerging domains, such as sensor networks and robotics.
Current Professional Activities
- Director of Harvard's Center for Research on Computation and Society
- Computing Research Association Board (CRA)
- Editorial Board for the Journal of the ACM
- Chair of the Editorial Board for Research Highlights of Communications of the ACM.
- Microsoft Research Technical Advisory Board
- Microsoft Trustworthy Computing Academic Advisory Board
- Max Planck Institute for Software Systems Scientific Advisory Board
- ACM International Conference on Functional Programming (ICFP'13) General Chair
- National Research Council's Study on Future Research Goals and Directions for Foundational Science in Cybersecurity
- Chair of the Harvard FAS Standing Committee on IT
- Advisory Board of the Intel/Berkeley Science and Technology Center for Secure Computing (SCRUB)
Current Research Projects
|
CHILI:
An IARPA-sponsored joint project between Cornell, Harvard, and
the University of Illinois where we are focused on the STONESOUP
agenda: Securely Taking on New Executable Software of Unknown
Provenance. Our project is utilizing LLVM and its Secure Virtual
Architecture, coupled with information flow analysis, dynamic
rewriting, and compiler verification. |
|
DHOSA:
Defending Against Hostile Operating Systems. This MURI
project combines researchers from Berkeley, Virginia,
Illinois, Stony Brook and Harvard to address new approaches
and techniques for building applications that can be secure
in spite of a faulty or even malicious operating system. |
|
CRASH-SAFE:
This DARPA-funded project is focused on a clean slate design
for resiliant and secure systems. A joint project between
researchers at BAE, Penn, Northeastern, and Harvard, we are
designing new hardware, new languages, and new systems
services oriented towards security. A key distinguishing
element is our pervasive use of formal methods, and strong
emphasis on hardware-software co-design. |
|
RoboBees:
Inspired by the biology of a bee and the insect's hive behavior, we
aim to push advances in miniature robotics and the design of compact
high-energy power sources; spur innovations in ultra-low-power
computing and electronic "smart" sensors; and refine
coordination algorithms to manage multiple, independent
machines. |
|
GoNative:
This project is a joint effort with researchers at Lehigh and Harvard,
and focuses on low-overhead techniques for providing security
guarantees to software systems in which type-safe languages
such as Java interoperate with native C, C++, and assembly
code. |
Some Previous Research Projects
|
Ynot:
The goal of the Ynot project is to explore the design, implementation,
and use of next-generation type systems. In particular, we are focusing
on the integration of powerful program logics into the type system of
an ML-like, higher-order, imperative programming language,
making it possible to specify the desired effects of programs and
prove correctness. |
|
LLVMmd:
We are building a translation validator which automatically
verifies that compiler optimizations are correct. Our tools
work by analysing two LLVM programs and then tries to construct
a proof they have the same meaning. Our tools do not require any
integration with the optimizer to work, and can also be used on
hand-optimized code. The work is focused around scaling this
technique to a real-world compiler such as LLVM. |
|
NoBot:
We address the problem of threats to networked systems from
botnets. Our approach is to design a programmable
platform for innovation, the NoBot Programming Environment
(NOPE),which may reside on a variety of nodes that are operated by network
providers such as commercial ISPs or DISA. NOPE provides
facilities for data collection, data analysis and policy
distribution, creating a coordinated set of nodes which
collaborate to overcome the botnet threat. |
|
Cyclone:
Cyclone is a type-safe dialect of C that
provides good control over data representations and memory management
without sacrificing safety. It uses a combination of novel
technologies,
including region-based types, wrapped libraries, and link-time checking
to achieve these goals. |
|
Macroprogramming Sensors:
We are investigating high-level languages for
programming diverse, distributed networks of inexpensive sensors.
Our goal is to greatly simplify sensor network application design by providing
high-level programming abstractions, and primitives that automatically
compile down to the complex, low-level operations implemented by each
sensor node. |
![]() |
PittSFIeld:
Stephen McCamant
(MIT) and I developed an efficient software-based fault isolation (SFI)
tool for Intel x86 code. The tool can be used to restrict a process
from reading, writing, or executing addresses outside a specified range
without the need for hardware-based process isolation. Google adopted
the ideas behind this technology for their NativeClient plugin
framework. |
|
Typed Assembly Language:
A type system for the Intel x86 assembly language. The TAL type system is rich
enough that we can efficiently encode a number of high-level language constructs, yet it
is still possible to statically verify that the machine code
will respect type safety when executed. The latest release (2.0) of
the TAL tools can be found
here. |
Teaching
- Sp 2013: CS51, Introduction to Computer Science II
- Fa 2012: CS252r, Advanced Functional Language Implementation
- Sp 2012: CS51, Introduction to Computer Science II
- Fa 2011: CS153, Compilers
- Fa 2011: CS252r, Advanced Topics in Programming Languages
- Sp 2011: CS51, Introduction to Computer Science II
- Sp 2010: CS51, Introduction to Computer Science II
- Fa 2009: CS153,
Compilers
- Sp 2009: CS51, Introduction to Computer Science II
- Fa 2008: CS252, Advanced Programming Languages
- Sp 2008: CS152,
Programming Languages
- Fa 2007: CS153,
Compilers
- Sp 2007: CS250r, Topics
in Programming Language Design and Implementation
- Fa 2006: CS153,
Compilers.
- Sp 2006: CS256, Programming
Languages and Semantics.
- Fa 2005: CS153,
Compilers.
- Sp 2005: CS256,
Programming Languages and Semantics.
- Fa 2004: CS153, Compilers.
- Sp 2004: CS255, Topics in Language-Based Security.
Researchers
- Randy Pollack (Senior Research Fellow)
Current Post Docs
Current PhD Students
- David Darais
- Daniel Huang
- Gregory Malecha
- Adam Petcher
- Ryan Wisnesky
Current Undergraduate Research Assistants
- Edward Gan
- Brian Plancher
- Joseph Tassarotti
Former Post Docs
- Amal Ahmed (now at Northeastern)
- Adam Chlipala (now at MIT)
- Mike Hicks (now at Univ. of Maryland)
- Aleksander Nanevski (now at IMDEA)
- Matthieu Sozeau (now at INRIA Paris)
- Jean-Baptiste Tristan (now at Oracle Labs)
- Jeff Vaughan (now post doc at UCLA)
Former Phd Students
- James Cheney (now at University of Edinburgh)
- Karl Crary (now at Carnegie Mellon)
- Úlfar Erlingsson (now at Google)
- Matthew Fluet (now at Rochester Institute of Technology)
- Neal Glew (now at Intel Research)
- Paul Govereau
- Dan Grossman (now at Univ. of Washington)
- Kevin Hamlen (now at UT Dallas)
- Geoff Mainland (now at Microsoft Research)
- Avi Shinnar (now at IBM Research)
- Frederick Smith (now at Mathworks)
- David Walker (now at Princeton)
- Stephanie Weirich (now at Univ. of Pennsylvania)
Brief bio
Greg Morrisett received his B.S. in Mathematics and Computer Science
from the University of Richmond in 1989, and his Ph.D. from Carnegie
Mellon in 1995. In 1996, he took an assistant professor position in
the Computer Science Department of Cornell University, where he was
promoted to associate professor with tenure in 2002. In the 2003-04 academic
year, he took a sabbatical and visited the Microsoft European Research
Laboratory. In 2004, he moved to Harvard as the Allen B. Cutting
Professor of Computer Science, and served in the position of Associate
Dean for Computer Science and Engineering from 2007-2010. He currently
heads the Harvard Center for Research on Computation and Society.
Morrisett has received a number of awards for his research on
programming languages, type systems, and software security, including
a Presidential Early Career Award for Scientists and Engineers
(presented at the White House in 2000), an IBM Faculty Fellowship, an
NSF Career Award, and an Alfred P. Sloan Fellowship.
He served as Chief Editor for the Journal of Functional
Programming and as an associate editor for ACM Transactions on
Programming Languages and Systems and Information Processing Letters. He currently serves on the
editorial board for The Journal of the ACM and as co-editor-in-chief
for the Research Highlights column of Communications of the ACM.
In
addition, Morrisett has served on the DARPA Information Science and
Technology Study (ISAT) Group, the NSF Computer and Information
Science and Engineering (CISE) Advisory Council, Microsoft Research's
Technical Advisory Board, Microsoft's
Trusthworthy Computing Academic Advisory Board, and the Fortify
Technical Advisory Board.





