MRG Project Logo

Mobile Resource Guarantees
(MRG, project IST-2001-33149)

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.

Related Projects

Related Projects

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:

DART Dynamic Assembly, Reconfiguration and Type-Checking
Mikado Mobile Calculi based on Domains
MyThS Models and Types for Security in Mobile Distributed Systems
PROFUNDIS Proofs of Functionality for Mobile Distributed Systems
SECURE Secure Environments for Collaboration among Ubiquitous Roaming Entities

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.

See also the PCC home page and Necula's bibliography.


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: SafetyNet

See 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.

Kestrel Institure, Coglio et al: High-Assurance Java Virtual Machine

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

We study problems in computer security, especially mobile code systems such as Java, ActiveX, and JavaScript. We try to understand how security breaks down, and to develop technology to address the underlying causes of security problems."

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).

See: Compagnoni's home page

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.

See: TINMAN paper and project page at Austin

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.

Valid HTML 4.01!
Validate this page