Research Projects

I am currently involved with two main research projects:

  1. Manifest Security. This project is a collaboration with the University of Pennsylvania, supported by the National Science Foundation CyberTrust program, under grant number CNS-0716469.
  2. Integrating Types and Verification. This project is a collaboration with Harvard University, supported by the National Science Foundation Computing Processes and Artifacts (CPA) program, under grant number 0702381.

I was previously a co-principal investigator on the ConCert Project, the Triple Project, the PSciCo Project, and the Fox Project.

Manifest Security Project

Manifest Security project is a collaborative research program including faculty, students, and post-doctoral researchers at the University of Pennsylvania and Carnegie Mellon University.

This project proposes manifest security as a new architectural principle for secure extensible systems. Its research objectives are to develop the theoretical foundations for manifestly secure software and to demonstrate its feasibility in practice.

Manifest security applies to extensible software platforms -- software systems that can be customized by installing third-party extensions. The goal of manifest security is to address two fundamental problems in this domain, both stemming from the need to protect the platform from untrusted and potentially malicious extensions. Useful software extensions often require access to system resources or sensitive information, yet permitting unrestricted access opens the possibility for abuse. It is therefore necessary, first, to specify policies about what resources an extension may use and how it can handle sensitive data; second, the platform must also include an effective mechanism for enforcing such policies. The critical components missing from existing architectures are thus (1) a general, practical means for users to specify security policies about how extensions are permitted to behave, and (2) a way of determining whether a given extension (which may be malicious) actually meets the desired policy. Manifest security addresses both of these issues.

Integrating Types and Verification

This project is investigating the integration of types and specifications in a programming language. The key to the integration is to employ dependent types, which permit precise behavioral specifications of computations, with monadic types to segregate effect-free computations from those that may have effects on storage.

The ConCert Project: Trustless Grid Computing

The ConCert Project investigates the theoretical and engineering basis for the trustless dissemination of software in an untrusted environment. To make this possible the project investigates machine-checkable certificates of compliance with security, integrity, and privacy requirements. Such checkable certificates allow participants to verify the intrinsic properties of disseminated software, rather than extrinsic properties such as the software's point of origin.

To obtain checkable certificates the project develops certifying compilers that equip their object code with formal representations of proofs of properties of the code. Specifically, the project investigates the use of proof-carrying code, typed intermediate languages, and typed assembly languages for this purpose. In each case certificate verification is reduced to type-checking in a suitable type system.

For a brief summary of the project, please see the one-page abstract. For further information, please see the full proposal, in either Postscript or PDF format.

The Triple Project: Type Refinement in Programming Languages

The goal of the Triple Project is to enrich conventional type systems to support specification and verification of programmer-defined invariants governing values of a given type. For example, it may be useful to state and check that a function whose type is int->int in fact maps positive integers to positive integers, zero to zero, and negative integers to negative integers. To take another example, it may be useful to specify that the insertion function for a balanced binary search tree returns a balanced tree if its argument is balanced. These are examples of persistent refinements, properties that hold irrespective of any change of state that may occur in the program. These are to be contrasted with ephemeral refinements that express properties whose truth depends on the changeable state of the program. For example, we may wish to state that a given function assumes that a given lock is held, and returns with that lock free, or vice versa. The Triple Project is exploring the use of such specifications in a practical programming language. We are using Standard ML as the basis for our investigations because it supports both effect-free and effect-ful computation, and has a richly expressive module system. One goal of our research is to enrich the interface language of the ML module system to support specification of type refinements that are checked whenever an interface is ascribed to a module. There is a fundamental tension between what is stateable and what is mechanically checkable. In general as the expressiveness of a system of refinements increases, so does the difficulty of checking that a program respects a stated refinement property. But it is clear that we can significantly enrich the expressive power of type systems without compromising mechanical checkability. One goal of the project is to explore how far we can extend these ideas without embarking on a full-scale theorem proving project.

The Fox Project

The goal of the Fox Project is to apply advanced language technology to software development. The work of the project proceeds on three fronts:

The Fox Project is distinguished by an active and vital interplay between theory and practice --- we prove theorems and report performance numbers!

Here are some significant accomplishments of the project:

The PSciCo Project

The goal of the PSciCo Project is to explore the use of advanced language technology for scientific computing. There is at present a sharp division between prototyping languages, such as Mathematica and MatLab, and production languages, such as C and Fortran, for scientific computing. Prototyping languages are convenient to use interactively, support symbolic and numeric computation, but tend to be quite inefficient and semantically suspect. Production languages are batch-oriented, provide little or no support for symbolic computation, but tend to produce very efficient code.

The goal of the Fox Project is to develop the language and compiler technology to eliminate this distinction. We are investigating the use of purely functional languages based on Standard ML and NESL for scientific computing. Standard ML offers strong support for symbolic computation and a rich module system for building programs from off-the-shelf components. NESL demonstrated the use of pure, call-by-value functional programming for implicit data parallel computation on numbers and arrays. Our contention is that by combining Standard ML and NESL we can achieve acceptable efficiency on stock hardware with unprecedented expressive power and convenience.

Like the Fox Project, the work of the project proceeds on three fronts:

Note: The phrase "scientific computing" is sometimes used as a euphemism for "nuclear bomb simulation". We are not doing nuclear bomb simulation!

Last modified: Thu Mar 24 14:45:51 EST 2005