Photo: Greg Morrisett

Greg Morrisett

Jack and Rilla Neafsey Dean and Vice Provost of Cornell Tech
Cornell University

2 West Loop Road
New York, New York 10044

Assistant: Lynette Jordan
Email: greg.morrisett@cornell.edu

Lynette's Email: lynette.jordan@cornell.edu

Greg Morrisett is the Dean and Vice Provost of Cornell Tech, a New York City-based campus focused on graduate education that integrates technology, business, law, and design in service of economic impact and societal good. Previously, Greg served as the Dean of Computing and Information Sciences (CIS) at Cornell University, which houses the departments of Computer Science, Information Science, and Statistical Sciences. Before this, 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.

Some Previous Research Projects

	CertiCoq: 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.
	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.
	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.
	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.
	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.
	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.