Combining research in programming languages, formal methods, and cyber security.

Dover is designing a security coprocessor that blocks most current cyberattacks and that supports advanced security policies such as information flow control, control flow integrity, multi-level security, and more.

Working on "Dover", an extension to the RISC-V open source architecture.Dover applies software-defined "micro-policies" on a per-instruction, per-word basis.Micro-policies can implement a wide array of security policies, including memory protection (no buffer overflows), control flow integrity (no ROP / code reuse attacks), and information flow secrecy and integrity.Each word in Dover is tagged with a pointer to metadata maintained and checked by the micro-policies. Hardware interlocks ensure that only micro-policy code has access to the metadata and that policy enforcement is not avoidable or subvertible.We have implemented Dover on a Xilinx FPGA, as an extension to RISC-V, and we are working on building out a SOC with networking and flash storage. We are writing policies and integrating them into existing operating systems, protecting conventional C codebases.

Applied research in software engineering, verification, computer security, planning.Principal investigator on DARPA PPAML OP3 project. We are creating probabilistic programming languages backed by formal semantics of "intensional properties" in order to optimally match probabilistic models plus queries with inference algorithms. October 2013-.Principal investigator on DARPA CRASH SAFE project (see http://crash-safe.org). SAFE is a clean slate redesign of the compute stack, including a novel tagged ISA, new programming languages for information flow control, a "zero kernel" operating system, and ambitious formal verification. SAFE is being prototyped on FPGAs, and will provide a secure computer system from the ground up. Work with University of Pennsylvania, Harvard University, and Northeastern University. Oct. 2010-.Principal investigator on DARPA AACE AESOP project. The AESOP project characterized hardware (e.g. cache performance) and then automatically parallelized C code to optimally use multiple cores. Work with Princeton University and the University of Maryland.Principal investigator on DARPA Application Communities project. The AC project addressed monoculture vulnerabilities by learning normal profiles, monitoring for anomalies, and then automatically devising, deploying, and evaluating patches when attacks are detected. Work with MIT.Local lead on DMT PAMS (DARPA, 2006-2010). Develop domain specific model-based software engineering tools for increased adaptability and robustness. Collaboration with Vanderbilt University.

Projects included: dynamic virtual machine, aspect-oriented programming, design patterns in dynamic languages, dynamic native optimization of interpreters, languages for model-based programming, and verification of model-based programs. Founded the Lightweight Languages Workshops. See ll3.ai.mit.edu, ll2.ai.mit.edu, ll1.ai.mit.edu

Working on compiler for Dylan, a dynamic object-oriented language.

Taught introductory "computer literacy" courses to business students.

Worked on Chrysalis reverse engineering tool suite.

Worked on CASE (Computer Aided Software Engineering) tools.