Bachelor Thesis: A Sandboxing Infrastructure for Alice ML

Context

The essence of open programming is the ability to import code at runtime, in order to allow applications to adapt their behaviour and functionality dynamically. However, when code is acquired from untrusted sources – e.g. some remote Internet domain – security concerns arise. Untrusted code should not be given unrestricted access to local resources. A well-known solution is to run untrusted code in a sandbox, a software environment which dynamically checks all critical operations performed by the code according to some configurable security policy. Java is the most popular language employing this approach.

Alice ML is a dialect of Standard ML that has been specifically designed to support type-safe open programming. It provides a generic and strongly-typed import/export facility (pickling), which allows processes to exchange or make persistent almost arbitrary language-level data structures and code. For security reasons, resources are precluded from pickling. Instead, it is left to the target site to supply them explicitly to imported code. A flexible notion of component allows respective abstractions to be programmed conveniently.

Task Description

The pickling and component mechanisms of Alice ML form a suitable basis for implementing sandboxing as a library. Loading of components is always delegated to a component manager, which is inherited along import chains. A sandbox can hence be installed simply by creating a custom component manager that controls access to critical system components.

The task of this thesis is to survey existing approaches to sandboxing, and examine ways to adapt them to an ML-like language. Based on this, design a suitable infrastructure for sandboxing in Alice ML in form of library support for creating and configuring custom component managers with security policies. This design has to be implemented in the existing Alice system.

References

• Li Gong. Secure Java Class Loading. IEEE Internet Computing, 2(6):56–61, 1998.
• Xavier Leroy. Computer Security from a Programming Language and Static Analysis Perspective. 12th European Symposium on Programming, Lecture Notes in Computer Science, 2618:1–9, 2003.
• Xavier Leroy. Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning, 30(3–4):235–269, 2003.
• Andreas Rossberg. The Missing Link – Dynamic Components for ML. Submitted, April 2006.
• Peter Sewell and Jan Vitek. Secure Composition of Insecure Components. 12th Computer Security Foundations Workshop, IEEE Computer Society Press, 1999.

Downloads

You can download the slides for my introductory talk at the PS chair, as well as the slides for my final talk.
The actual thesis paper, A Sandboxing Infrastructure for Alice ML, is of course also available.

Last change: Sat, 2006-11-25