Purpose:

A significant problem associated with mobile computation is the crossing of administrative domains. Mobile programs need to be able to navigate in a hierarchy of domains obtaining authorization to cross differents barriers. A related problem is that of security. Type systems restrict possible operations in a way that is relevant to security.

Approach:

We will study the applications of type systems to the solution of such problems using, among others, the approach of code which carries its own proof of (type) correctness. Using this approach one could package a module or program to be transmitted over a network together with a proof that certain errors will not occur when executed. In the way, the receiver of the package could automatically and independently check that the software is security-error-free, authorization-error-free running it.

Status:

Related Publications: