Sandboxing in ocaml

Sandboxing in ocaml

[Christian Szegedy]

Hello,

Is this possible in ocaml to dynamically load some (bytcode) OCaml file 
and run it in a safe environment, that is only using a small subset of 
selected functions instead of the whole Pervasives?

Re: [Caml-list] Sandboxing in ocaml

[Jacques Garrigue]

> Is this possible in ocaml to dynamically load some (bytcode) OCaml file 
> and run it in a safe environment, that is only using a small subset of 
> selected functions instead of the whole Pervasives?

This is the intent of Dynlink.allow_only.
Not however that allowing is done on a unit base, so if you want to
allow only some functions in a unit, you must create a new one
containing only those, and compile your file against those (otherwise you
won't be able to load it).
This is the way MMM applets are made safe.

Also, there is no bytecode verifier. That is, a hand-crafted bytecode
file could break the above safety. In this respect, the bytecode
interpreter does not provide real sandboxing. If you want to protect
yourself, you have to use other ways, like a certified signature
scheme. The following paper explains this strategy to safety:
 Xavier Leroy and Francois Rouaix. Security properties of typed
 applets. In J. Vitek and C. Jensen, editors, Secure Internet
 Programming - Security issues for Mobile and Distributed Objects,
 volume 1603 of  Lecture Notes in Computer Science, pages
 147-182. Springer-Verlag, 1999. 

Jacques Garrigue

Re: [Caml-list] Sandboxing in ocaml

[Christian Szegedy]

Jacques Garrigue wrote:

>>Is this possible in ocaml to dynamically load some (bytcode) OCaml file 
>>and run it in a safe environment, that is only using a small subset of 
>>selected functions instead of the whole Pervasives?
>>    
>>
>
>This is the intent of Dynlink.allow_only.
>Not however that allowing is done on a unit base, so if you want to
>allow only some functions in a unit, you must create a new one
>containing only those, and compile your file against those (otherwise you
>won't be able to load it).
>This is the way MMM applets are made safe.
>  
>
Excellent! This sounds exactly what I want. Can I forbid
the Pervasives unit while linking the applet?

Thanks a lot, Christian

Re: [Caml-list] Sandboxing in ocaml

[Jacques Garrigue]

From: Christian Szegedy <szegedy@t-online.de>
> >This is the intent of Dynlink.allow_only.
> >Not however that allowing is done on a unit base, so if you want to
> >allow only some functions in a unit, you must create a new one
> >containing only those, and compile your file against those (otherwise you
> >won't be able to load it).
> >This is the way MMM applets are made safe.

> Excellent! This sounds exactly what I want. Can I forbid
> the Pervasives unit while linking the applet?

Sure: just omit it from the allowed units.
The applet should then be compiled with the -nopervasives option.

Jacques Garrigue