Quick links

Grid Computing and Foundational Certified Code

Date and Time
Friday, April 16, 2004 - 2:00pm to 3:30pm
Friend Center 013
Karl Crary, from Carnegie Mellon University
Andrew Appel
Grid computing seeks to harness idle computing power on the Internet to create a huge supercomputer available to the public. Many obstacles exist to making this vision a reality; a primary obstacle is the understandable reluctance of computer owners to execute code from sources they do not trust. This obstacle limits participation in the grid to the small number who can afford to cultivate pre-arranged trust relationships for their applications.

The ConCert project seeks to make the grid universally usable by eliminating the need for trust when disseminating applications. This is achieved using certified code to ensure that grid applications comply with a safety policy. However, certified code can raise other obstacles to universal usability. In particular, if a safety policy is overly specific, it may unnecessarily limit the number of applications that can comply, and therefore limit the number that can use the grid.

This talk discusses our work to resolve this issue through foundational certified code, wherein the safety policy is as general as possible. Foundational certified code has been infamously difficult to work with, as its certificates must include complete (and typically complicated) safety arguments to the level of the concrete architecture that tend. We discuss our system, called TALT, which employs a unique methodology based in metalogic and operational semantics that ameliorates these difficulties.

(This is joint work with Susmit Sarkar.)

Follow us: Facebook Twitter Linkedin