Description

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.

To demonstrate the utility of trustless software dissemination, the project develops an infrastructure for building applications that exploit the computational resources of a network of computers. The infrastructure consists of a "steward" running on host computers that accepts and verifies certified binaries before installing and executing them, and certifying compilers that generate certified binaries for distribution on the network.

For more information, please see the complete project description.

Talks

Distributed Control Flow with Classical Modal Logic.
Tom Murphy VII.
CSL 2005, Oxford, UK, August 2005.
Flash.
A Symmetric Modal Lambda Calculus for Distributed Computing.
Tom Murphy VII.
LICS 2004, Turku, Finland, July 2004.
Flash.
Hemlock and the ConCert v2 Framework.
Tom Murphy VII.
Carnegie Mellon University, August 2003.
Flash.
Trustless Grid Computing in ConCert (Progress Report).
Robert Harper.
Foundations of Global Computing, Eindhoven, June 2003.
Powerpoint.
Trustless Grid Computing in ConCert.
Tom Murphy VII.
GRID 2002, Baltimore, November 2002.
Powerpoint.
The ConCert Project: Trustless Grid Computing.
Robert Harper.
Carnegie Mellon Univeristy, May 2002.
PostScript, PDF, Powerpoint.
An Introduction to Typed Assembly Language.
David Walker.
Carnegie Mellon Univeristy, October 2001.
PostScript.

Publications

A Separate Compilation Extension to Standard ML (Revised and Expanded Technical Report)
Dave Swasey and Tom Murphy VII and Karl Crary and Robert Harper
Technical report CMU-CS-06-133.
Abstract, PDF.
Automated and Certified Conformance to Responsiveness Policies
Joseph C. Vanderwaart and Karl Crary
In Proceedings of the ACM SIGPLAN Workshop on Types in Language Design and Implementation, 2005. pages 79-90, Long Beach, California, January 2005.
Abstract, PDF, PostScript.
Distributed Control Flow with Classical Modal Logic
Tom Murphy VII, Karl Crary, Robert Harper
CSL 2005
Abstract, PDF.
A Symmetric Modal Lambda Calculus for Distributed Computing
Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning
LICS 2004
Abstract, PDF.
A Symmetric Modal Lambda Calculus for Distributed Computing (Extended)
Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning
CMU-CS-04-105, 2004
Abstract, PDF, PostScript.
Towards a Functional Library for Fault-Tolerant Grid Computing
Bor-Yuh Evan Chang, Margaret DeLap, Jason Liszka, Tom Murphy VII, Karl Crary, Robert Harper, and Frank Pfenning
Unpublished Work-in-Progress Report, 2002
Abstract, DVI, PDF, PostScript.
Trustless Grid Computing in ConCert
Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, and Frank Pfenning
Proceedings of the GRID 2002 Workshop, Springer-Verlag LNCS 2536
Abstract, DVI, PDF, PostScript.
Implementing a Framework for Certified Grid Computing
Margaret DeLap
Senior Honors Thesis, 2002
CMU-CS-02-151
Abstract, PostScript,
Iktara in ConCert: Realizing a Certified Grid Computing Framework from a Programmer's Perspective
Bor-Yuh Evan Chang
Senior Honors Thesis, 2002
CMU-CS-02-150
Abstract, DVI, PDF, PostScript.
Stack-Based Typed Assembly Language.
Greg Morrisett, David Walker, Karl Crary, and Neal Glew.
To appear in the Journal of Functional Programming. An earlier version appeared in Proceedings of the Workshop on Types in Compilation, X. Leroy and A. Ohori, editors, Springer-Verlag LNCS 1473, March 1998.
Related paper.
Logical Frameworks
Frank Pfenning. Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov, editors, Chapter 16, pp. 977-1061, Elsevier Science and MIT Press, 2001.
PDF, PostScript, Twelf code.
A Certifying Compiler for Java.
Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, and Kenneth Cline.
In Proceedings of the Conference on Programming Language Design and Implementation, pages 95-107, Vancouver, Canada, June 2000. ACM Press.
Available electronically.
Resource Bound Certification.
Karl Crary and Stephanie Weirich.
In Proceedings of the Symposium on Principles of Programming Languages, pages 184-198, Boston Massachusetts, January 2000.
Abstract, DVI, PostScript.
Type Structure for Low-Level Programming Langauges.
Karl Crary and Greg Morrisett.
In Proceedings of the International Colloquium on Automata, Languages, and Programming, pages 40-54, Prague, Czech Republic, July 1999.
Abstract, DVI, PostScript.
From System F to Typed Assembly Language.
Greg Morrisett, David Walker, Karl Crary and Neal Glew.
ACM Transactions on Programming Languages and Systems, 21(3):527-568, May 1999.
Abstract, DVI, PDF, PostScript.
Compiling with Proofs.
George C. Necula.
PhD thesis, Carnegie Mellon University, October 1998. Available as Technical Report CMU-CS-98-154.
Abstract, Postscript, PDF.
Safe, Untrusted Agents using Proof-Carrying Code.
George C. Necula and Peter Lee.
In Giovanni Vigna, editor, Mobile Agents and Security, pages 61-91. Springer-Verlag LNCS 1419, August 1998.
Available electronically.
Safe Kernel Extensions Without Run-Time Checking.
George C. Necula and Peter Lee.
In Proceedings of the Symposium on Operating System Design and Implementation, pages 229-243, Seattle, Washington, October 1996.
Abstract, HTML, Postscript.
A Framework for Defining Logics.
Robert Harper, Furio Honsell, and Gordon Plotkin. Journal of the Association for Computing Machinery, 40(1):143-184, January 1993.
PDF, PostScript.

Software

The prototype ConCert framework, simulator, and sample applications are available from our Software page.

Principal Investigators

Support

The ConCert Project is supported by the National Science Foundation under grant number 0121633: "ITR/SY+SI: Language Technology for Trustless Software Dissemination".