Greg Morrisett

Allen B. Cutting Professor of Computer Science
School of Engineering and Applied Sciences
Harvard University

33 Oxford Street
151 Maxwell Dworkin Hall
Cambridge, MA 02138

Assistant: Susan Welby
Maxwell Dworkin 239
                         Office phone: +1 (617) 495-9526
Fax: +1 (617) 495-2498


Susan's phone: +1 (617) 496-7592

Photo: Greg Morrisett

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


Current Research Projects

Crash 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.
Robobee 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 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

CHILI 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 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.
Ynot 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 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 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: 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.
Sensor Mote 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 Police
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.
Types Inside 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


Researchers

Current Post Docs

Current PhD Students

Former Post Docs

Former Phd Students


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.

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 was recently made a Fellow of the ACM.

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.