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

• Type: Journal
• Year: 2006
• Where: JALC
• Authors: Hervé Grall
• Keywords: JALC 2006, Local Environment, Local Resource, Mobile Program