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

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:

Internationally, there are several other projects related to MRG research. The rest of this page summarises a number of these:

• Carnegie Mellon University: ConCert
• Necula and Lee: Proof-Carrying Code
• VerifiCard
• St Andrews University: HUME
• University of Sussex: SafetyNet
• Imperial College: SecSafe, SLURP
• UPenn: PLAN
• Kestrel Institure: High-Assurance Java Virtual Machine
• Princeton: Secure Internet Programming
• Compagnoni: Formally Verified Environment
• University of Texas: TINMAN

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.

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

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.

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

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.

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

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