Sciweavers

JALC
2006

A Confinement Criterion for Securely Executing Mobile Code

13 years 3 months ago
A Confinement Criterion for Securely Executing Mobile Code
Mobile programs, like applets, are not only ubiquitous, but also potentially malicious. We study the case where mobile programs are executed by a host system in a secured environment, in order to control all accesses from mobile programs to local resources. The article deals with the following question: how to ensure that the local environment is secure? We answer by giving a confinement criterion: if the type of the local environment satisfies it, then no mobile program can directly access to a local resource. The criterion, which is typebased and hence decidable, is valid for a functional language with references. By proving its validity, we solve a conjecture stated by Leroy and Rouaix at POPL '98; moreover, we show that the criterion is optimal. The article mainly presents the proof method, based on a language annotation which keeps track of code origin and thus enables studying the interaction frontier between the local code and the mobile code, and it finally discusses the ...
Hervé Grall
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JALC
Authors Hervé Grall
Comments (0)