I am currently involved with two main research projects:
I was previously a co-principal investigator on the ConCert Project, the Triple Project, the PSciCo Project, and the Fox 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.
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 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 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 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 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!