Greg Morrisett
Bio:
Greg Morrisett received his B.S. in Mathematics and Computer Science
from the University of Richmond
(1989) and his Ph.D. in Computer Science from Carnegie
Mellon University
(1995). He spent about seven years on the faculty of the Computer
Science Department at Cornell
University. In the
2002-03 academic year, he took a
sabbatical at Microsoft's
Cambridge Research Laboratory.
In January of 2004, he moved
to Harvard
University.
Links to some of my publications appear on another page.
My current research interests are in the applications of programming language technology for building secure and reliable 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.
Research projects:
| Triforce: The
Programming Language and Compiler Research group is composed of faculty
and students at Harvard who are interested in problems related to
programming language foundations, design, and implementation. We
have weekly meetings (Wednesdays at 4 in MD319) where students and
faculty get together to discuss a range of recent research topics from
type systems, to language design, from compilation and runtime issues,
to security and semantics. |
|
| A next generation functional programming language. The focus of this project is a synthesis of good ideas from the ML, Haskell, Scheme, and LF communities. In particular, we are designing a language that like ML and Scheme, is primarily call-by-value, but like Haskell, provides good support for laziness. As in Haskell and FX, we are attempting to isolate effects and reflect them in the types. As in Haskell, O'Caml, and LF, we are trying to push the boundaries of type systems and type inference to the next level. Currently, I am working with Amal Ahmed and Mathew Fluet on issues involving state and effects. | |
| The
Cyclone Safe-C Project:
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. The source code for Cyclone is freely
available.
Currently, we are working
on making the analyses in Cyclone extensible
and certified. |
|
| Language-Based
Security for Malicious Mobile Code: In this project, we
are aiming to develop and refine new security enforcement mechanisms
that are well suited for networked information systems built with
extensible components. The technologies we are utilizing include
in-lined reference monitors, type-based enforcement of difficult
policies such as information flow, typed assembly language,
proof-carrying code, and certifying compilers. Currently, I am
working with Kevin Hamlen and Fred Schneider to develop a certifying
rewriter for inlined reference monitors. |
|
|
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. Currently, I am working with Matt Welsh, Geoff
Mainland, and Ryan Newton on the design and implementation of our
macro-level programming language. |
|
| Typed Assembly Language: For the past few years, my research group has focused on advanced type systems for low-level, mobile code. One of the by-products of our research is a type system for the Intel x86 assembly language called TAL (typed 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. We have produced a number of tools, including efficient and scalable type- and link-checkers for verifying the safety of the machine code, as well as a compiler that produces TAL from a type-safe variant of C. The latest release (2.0) of the TAL tools can be found here. |