Greg Morrisett is the Dean of Computing and Information Sciences (CIS) at Cornell University, which houses the departments of Computer Science, Information Science, and Statistical Sciences. Previously, he held the Allen B. Cutting Chair in Computer Science at Harvard University from 2004-2015. At Harvard, he also served as the Associate Dean for Computer Science and Electrical Engineering and as the Director of the Center for Research on Computation and Society. Before Harvard, Morrisett spent eight years on the faculty of Cornell's Computer Science Department. He received his bachelor's degree from the University of Richmond and both his Master's and Doctorate degrees from Carnegie Mellon University.
Professor Morrisett's research focuses on the application of programming language technology for building secure, reliable, and high-performance software systems. A common theme is the focus on systems-level languages and tools that can help detect or prevent common vulnerabilities in software. Past examples include typed assembly language, proof-carrying code, software fault isolation, and control-flow isolation. Recently, his research focuses on building provably correct and secure software, including a focus on cryptographic schemes, machine learning, and compilers.
Morrisett is a Fellow of the ACM and 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, 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, Information Processing Letters, and The Journal of the ACM. He currently serves 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, The Max Planck Institute for Software Systems Advisory Board, the Computing Research Association Board, Microsoft Research's Technical Advisory Board, Microsoft's Trusthworthy Computing Academic Advisory Board, and the Fortify Technical Advisory Board.
Current Professional Activities
- Computing Research Association Board (Secretary) (CRA)
- Co-Chair of the Editorial Board for Research Highlights of Communications of the ACM.
- Computing Community Consortium
- A national academy study on Future Research Goals and Directions for Foundational Science in Cybersecurity
Current Research Projects
The CertiCoq project aims to build a proven-correct compiler for dependently-typed, functional languages, such as Gallina--the core language of the Coq proof assistant. A proved-correct compiler consists of a high-level functional specification, machine-verified proofs of important properties, such as safety and correctness, and a mechanism to transport those proofs to the generated machine code. The project exposes both engineering challenges and foundational questions about compilers for dependently-typed languages.
Some Previous Research Projects
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
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
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.
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.
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.
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
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.
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 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
including region-based types, wrapped libraries, and link-time checking
to achieve these goals.
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
(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
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
Current Post Docs
Former Post Docs
- Amal Ahmed (now at Northeastern)
- Adam Chlipala (now at MIT)
- Mike Hicks (now at Univ. of Maryland)
- Aleksandar Nanevski (now at IMDEA)
- Matthieu Sozeau (now at INRIA Paris)
- Jean-Baptiste Tristan (now at Oracle Labs)
- Jesse Tov (now at Northeastern)
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 Google)
- Paul Govereau (now at Potamus Trading LLC)
- Dan Grossman (now at Univ. of Washington)
- Kevin Hamlen (now at UT Dallas)
- Daniel Huang (now a postdoc at Berkeley)
- Geoff Mainland (now at Drexel)
- Gregory Malecha (now at Target)
- Adam Petcher (now at Oracle)
- Avi Shinnar (now at IBM Research)
- Frederick Smith (now at Mathworks)
- David Walker (now at Princeton)
- Stephanie Weirich (now at Univ. of Pennsylvania)
- Ryan Wisnesky (now at Categorical Informatics)