|The ConCert Project
is concerned with making grid computing available to arbitrary
developers without undermining the integrity or security
of grid hosts. The ConCert framework exploits code certification
to allow developers to certify compliance of application
code with host policies. Certification takes the form of
a machine-checkable proof that the application code complies
with the host policy. The purpose of this project is to
enhance the ConCert certification mechanism, and to deploy
it for wide use in the "real world".
The current ConCert framework uses Typed Assembly
Language (TAL-x86) as a code certification mechanism. While
suitable as a proof of concept, the TAL-x86 formalism is
not very flexible as a target language for certifying compilers.
The project has developed, but not yet deployed, a much
more general formalism, called TALT, that supports a much
richer range of compilation and certification techniques.
One goal of the proposed work is to integrate TALT into
the ConCert framework.
A full-scale prototype of the
ConCert grid computing framework has been built, and is
now ready for deployment. Our plan is to deploy the framework
first within the Computer Science Department on the scale
of a few dozen machines. The next step is to deploy the
framework on several thousand machines, which are being
made available for use by the Pittsburgh Public School System.
A full-scale deployment will require developing more sophisticated
methods for controlling network usage (to avert denial of
service attacks) and to permit simple installation by unsophisticated
users. Another goal of the proposed work is to implement
these extensions and to deploy the ConCert grid framework
in the "real world".