Mobile Resource Guarantees
|The MRG project was funded in 2002-2005 under the Global Computing pro-active initiative of the Future and Emerging Technologies part of the Information Society Technologies programme of the European Commission's Fifth Framework Programme.
MRG is one of 12 projects funded by the Fifth Framework Global Computing proactive initiative. The Global Computing website gives a list of projects with links to factsheets and slide presentations of each one.
Within the initiative, MRG is linked to five other projects; making up a cluster of activities on Analysis of Systems and Security:
Internationally, there are several other projects related to MRG research. The rest of this page summarises a number of these:
Carnegie Mellon University: ConCert
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. ... 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.Especially relevant to MRG is work on resource bounds and proof compression. See the ConCert webpages. Principal investigators are Karl Crary, Robert Harper, Peter Lee, Frank Pfenning.
Necula and Lee: Proof-Carrying Code
"Proof-Carrying Code (PCC) is a technique for safe execution of untrusted code. The basic idea is to require the code producer to generate a formal proof that the code meets the safety requirements set by the code receiver. The code receiver can easily check the proof by using a simple and easy-to-trust proof checker. Due to the separation of the difficult task of verifying the code from the easy task of validating the proof of verification, PCC can be used efficiently even for optimized assembly language."
They have built a compiler called Touchstone which invokes a "certifying theorem prover" (a grand name for a theorem prover that outputs proof objects, including objects for proofs generated by decision procedures).
Necula has also worked on a translation validation architecture for compilers, where individual (optimizing) translations are validated within the compiler, instead of attempting to verify the whole compiler (originally proposed by Pneuli, Siegel, and Singerman). Roughly, the strategy is to construct simulation relations between basic blocks in the original program and its translation.
The VerifiCard project aims to provide methods and tools for the complete specification and verification of JavaCard applets. The project is developing a formalization of the JavaCard source language and the JavaCard Virtual Machine, certified tools for the development of JavaCard programs, and methods and tools for the specification and verification of applets. See the VerifiCard webpages.
St Andrews University: HUME
Hume (Higher-order Unified Meta-Environment) is a strongly typed, mostly-functional language with an integrated tool set for developing, proving and assessing concurrent, safety-critical systems. Hume aims to extend the frontiers of language design for resource-limited systems, including real-time embedded and safety-critical systems, by introducing new levels of abstraction and provability.See the Hume webpages.
University of Sussex: SafetyNetSee the SafetyNet webpages.
Imperial College et al: SecSafe, SLURP
The IST project SecSafe (Secure and Safe Systems based on Static Analysis) involves Imperial College (coordinator), Trusted Logic, the University of Aarhus, Denmark and INRIA, Rennes, France.
There is also work at Imperial on formalizing Java by Drossopoulou and others in the SLURP group
UPenn, Gunter et al: PLAN
Research on active networks, including the PLAN project shares the idea of having a functional programming language for guaranteeing resource bounds: a bounded amount of CPU, memory, and bandwidth resource.
PLAN (Packet Language for Active Networks) is a new language for programs that form the packets of a programmable network. ... PLAN is based on the simply typed lambda calculus and provides a restricted set of primitives and datatypes. PLAN defines a special construct called a chunk used to describe the remote execution of PLAN programs on other nodes. Primitive operations on chunks are used to provide basic data transport in the network and to support layering of protocols. Remote execution can make debugging difficult, so PLAN provides strong static guarantees to the programmer, such as type safety. A more novel property aimed at protecting network availability is a guarantee that PLAN programs use a bounded amount of network resources.
This project includes work on JVM formalization.
Our ultimate goal is to synthesize a high-assurance implementation of the JVM using Kestrel's Specware. This is achieved by (1) developing a mathematical specification of the JVM and (2) refining it to executable code that is provably correct with respect to the specification.
Princeton: Secure Internet Programming
Projects: Proof Carrying Code, Proof Carrying Authentication, Modularity and Secure Linking, Secure Applications for handheld Devices, Secure Runtime Support (GC, debugging), Value-Sensitive Design for Browser Security (interdisciplinary project).
People: Edward Felten, Andrew Appel, Roberto Virga and a large team of grad students.
See: project page at Princeton.
Compagnoni's Formally Verified Environment
Compagnoni has an NSF grant "A Formally Verified Environment for the Production of Secure Software" with Hofmann and Aspinall named as international collaborators. Her plan encompases work on TAL memory models; resource bounded versions of TAL (joint work with Aspinall, building on type systems of Hofmann); dependently typed intermediate languages, and work on a "verified compiler" which produces code certificates enforcing safety criteria as a result of the compilation (joint work with Elsa Gunter).
Apart from the direct link here, another relation might be the way Compagnoni proposes to equip programs with proofs as part of type-checking, rather than in a split-phase dialogue with the code-producer and a theorem prover (the PCC protocol).
University of Texas: TINMAN
The TINMAN is a security monitoring architecture to monitor system resource utilization. The goal of the project is to detect and prevent denial-of-serive(DoS) alike attacks. The current research includes resource utilization checking for mobile codes which could be malicous or buggy to consume inordinate system resource and make its service unavailable to legitimate users, and intrusion detection for potential DoS attacks.
These pages are hosted by the Informatics Groups server at the University of Edinburgh.
Site maintained by Robert Atkey. This page last updated on: 2005-10-11.
Validate this page