Alice Project

The Sandbox structure

________ Synopsis ____________________________________________________

    signature SANDBOX
    structure Sandbox : SANDBOX

This structure realises an experimental sandbox infrastructure for executing untrusted components. To this end, it provides a means to create component managers which can be customised over a set of policy rules.

Sandboxing relies on the fact that resources cannot be pickled. A component can acquire relevant capabalities solely by means of linking suitable system components. In a sandbox, link requests to such components are redirected to safe wrappers that implement runtime tests to enforce the configured policy.

Note: The sandboxing mechanism should be understood as a proof-of-concept implementation, since some of the safety assumptions it makes about the runtime system are not vindicated in the current Alice system.

See also: POLICY, Component, ComponentManager

________ Import ______________________________________________________

    import signature SANDBOX from "x-alice:/lib/system/SANDBOX-sig"
    import structure Sandbox from "x-alice:/lib/system/Sandbox"

________ Interface ___________________________________________________

    signature SANDBOX =
        exception Security of string
        functor MkManager (Policy : POLICY) : COMPONENT_MANAGER

________ Description _________________________________________________

exception Security of string

Raised whenever a component performs an operation that violates the policy rules established by its component manager for realising a sandbox. The string either carries the name of the system function that was rejected, or a generic error message.

functor MkManager (Policy : POLICY) : COMPONENT_MANAGER

Enables creation of custom component managers to realise a sandbox. The Policy structure controls the rules governing access to capabilities inside the sandbox.

Note that an arbitrary number of independent sandboxes can be created. By creating a separate Policy structure for each sandbox, they may implement different policies.

A sandbox is said to be nested if it is created inside another sandbox. Note that a nested sandbox cannot grant more capabilities than its enclosing sandboxes, because the latter limits the capabilities the nested sandbox has and thus can provide itself.

________ Example _____________________________________________________

Assume that we want to link a component from a site that we do not trust, and hence we want to restrict its write access to the file system. We can do so by creating a sandbox component manager and evaluating the component through it.

First, we have to create a suitable Policy structure. This can be accomplished simply by applying the appropriate functor from the MkPolicy component:

    structure Policy = MkReadOnlyPolicy()

From this structure we create the sandbox manager:

    structure Safe = Sandbox.MkManager Policy

The structure Safe will have the full interface of a component manager. In particular, we can use the function to load the untrusted component:

    open unpack "http:/") : SIG

To make the example more concrete, let us create a component ourselves:

    val component =
            import structure TextIO : TEXT_IO from "x-alice:/lib/system/TextIO"
            val run : unit -> string
            fun run() =
               val file = TextIO.openOut "message.txt"
               TextIO.output(file, "Imperative programming rules!\n");
               TextIO.closeOut file;
               "Functional programming is nice."

We cannot allow our file system to be spammed with such heretic messages behind our backs, so it is a good choice to evaluate the component inside the sandbox:

    open unpack Safe.eval(Url.fromString "local", component) : (val run : unit -> string)
    val s = run()

Evaluating the call to run will fail due to its attempt to invoke TextIO.openOut, which causes a Security exception to be raised.

Note: The URL we choose here guides how relative imports performed by the component are resolved. In this case the component does not have relative imports, such that the choice is arbitrary.

But hey, maybe we have our noble, pluralistic day, and allow components to spread their word as long as they keep it to the /tmp directory. No problem, we just have to customize the policy accordingly, by defining a new rule for the "writeFile" capability (see the list of capabilities):

    fun tempOnly path =
	case OS.Path.fromString (OS.Path.mkCanonical path) of
        | {isAbs=true, arcs="tmp"::_, ...} => Policy.ACCEPT path
        | {isAbs=false, arcs=[name], vol} =>  (*) redirect!
	     Policy.ACCEPT(OS.Path.toString{isAbs=true, arcs=["tmp",name], vol})
	| _ => Policy.REJECT

    do Policy.File.rule("writeFile", tempOnly)

This rule does three things: (1) it freely allows opening files for writing in the /tmp directory, (2) it redirects files opened without specifying a directory to /tmp, and (3) it prohibits all other file write access. Note that it is important to make the path canonical, in order to avoid exploits with paths like /tmp/../home/user/. After setting this policy rule, our component above can be evaluated successfully, and leaves its message in the file /tmp/message.txt, where it should not cause any harm.

What if our policy was violated not during a call, but during evaluation of the component itself? For example, consider the following variation:

    val component =
            import structure TextIO : TEXT_IO from "x-alice:/lib/system/TextIO"
            val run : unit -> string
            val file = TextIO.openOut "/message.txt"
            do TextIO.output(file, "Imperative programming rules!\n")
            do TextIO.closeOut file
            fun run() = "Functional programming is nice."

In this case, the Security exception would already be raised during Safe.eval, which evaluates the component body. (And the exception will be raised despite our relaxed policy, because the component now tries to create the file in the root directory.)

Controlling imports

A more radical way to prevent write access is to prevent the system components that enable it from being imported at all. A rule for the capability can be set for this purpose:

    fun noIOCom url =
        case Url.toString url of
        | "x-alice:/lib/system/TextIO"
        | "x-alice:/lib/system/BinIO" => REJECT
        | _ => PASS

    do Policy.Url.rule("componentLoad", noIOCom)

This rule implements a form of black-listing of components. When it is active, any attempt to import one of the listed components will immediately raise a Security exception. Note that this also applies to imports performed by the Alice ML import declaration syntax, because that ultimately is mapped to the Component.load function. We only show this for presentational purposes. This approach is very restrictive, because it does not only disable write access, but actually any kind of I/O (at least through these components). Another major disadvantage of black-listing is that it is fragile: should the sandbox run on a version of Alice that provides additional components that enable write access then the policy is no longer safe.

A more realistic use of the "componentLoad" capability hence would be for white-listing external domains from which components may be imported:

    fun limitUrl url =
        case (Url.getScheme url, Url.getAuthority url) of
        | (NONE | SOME("file"|"x-alice"), _) => PASS
        | (SOME "http", ""|"") => PASS
        | _ => REJECT

    do Policy.Url.rule("componentLoad", limitUrl)

Instead of outright rejecting some components, a sandbox may also redirect the imports to other URLs, which carry safe substitutes, for example. This is precisely the approach taken by the predefined policy functors to handle system components: they redirect imports of these components to safe wrappers that check capabilities for individual operations. For this reason, the action taken for white-listed URLs should be PASS like above, not ACCEPT, since accepted URLs still have to be rewritten and delegated to the parent component manager, which is performed by the initial rules already set by the functors.

last modified 2007/Mar/30 17:10