search

usethesource / rascal

The implementation of the Rascal meta-programming language (including interpreter, type checker, parser generator, compiler and JVM based run-time system)
http://www.rascal-mpl.org
Other
406 stars 78 forks source link

Rascal in a Sandbox #19

Closed DavyLandman closed 8 years ago

DavyLandman commented 12 years ago

Goal

For various ideas (tutor/rascal on the web, automatic judging of results) we want to have a sandbox for Rascal. This page describes our proposal for creating this mode for rascal.

We aim for a low-maintenance solution with minimal impact on our current system.

Setting (attack vector)

The external user is allowed to submit Rascal expressions, Rascal files or non-executable data files. A timeout can be used to limit the possibility of a DOS. Data files can be used in two ways:

  1. The submitted Rascal program can read example data that is part of the Rascal library. It is convenient to have some standard data sets available.
  2. The submitter can add his/her own data.

    Proposed solution

Our solution is threefold.

  1. Disable the @java annotations on non- library functions. (eg., white list the library functions).
  2. Blacklist insecure Rascal functions (such as util::ShellExec).
  3. Whitelist locations which can be resolved for either reading or writing.

    Implementation

An evaluator is either started in sandbox mode or not, from a Rascal program this cannot be changed. The descriptions below describe the cases when an evaluator is started in sandbox mode.

Disabling @java annotations on non-library functions

During import of a module, we check in case of a @java annotation if the current module is on a white listed path (containing the library paths).

Blacklisting insecure Rascal functions

We introduce a new annotation @insecure (or a better name?) which is checked during overload resolution, and if it is called in sandbox mode, we raise a security exception.

Whitelist locations which can be resolved

The Location resolvers are extended such that when they create an InputStream or an OutputStream they call our own SandboxInputStreams or SandboxOutputStream instead. These will check if you try to read or write outside your current path or the loaded eclipse projects.

So our question to you is, are we forgetting an attack vector or is this a secure sandbox?

PaulKlint commented 12 years ago

This nicely summarizes our discussion. Some attack vectors we should worry about (and against which we try to defend in the above proposal) are:

  1. Calling functions that can read/write arbitrary files.
  2. Infinite loops (should be taken care of outside Rascal when calling the submitted program.
  3. Unmonitored modifications of the Rascal libraries or Rascal interpreter.
  4. ... and other we did not yet think about.
jurgenvinju commented 12 years ago

Notes:

mahills commented 12 years ago

Assuming that users cannot add their own @java functions, the first two parts of the solution seem to be the same thing. I think it's much better to whitelist functions that can be used than the blacklist them -- it would be too easy for something to slip through, for instance if someone forgets to add an @unsecure annotation.

Davy Landman wrote:

Goal

For various ideas (tutor/rascal on the web, automatic judging of results) we want to have a sandbox for rascal. This page describes our proposal of creating this mode for rascal.

We aim for a low-maintenance solution with minimal impact on our current system.

Setting (attack vector)

The external user is allow to submit rascal expressions or rascal files. A timeout can be used to limit the possibility of a DOS.

Proposed solution

Our solution is threefold.

  1. Disable the |@java| annotations on non library functions. (eg. white list the library functions).
  2. Blacklist unsecure rascal functions (such as |util::ShellExec|).

  3. Whitelist location which can be resolved for either reading or writing.

    Implementation

An evaluator is either started in sandbox mode or not, from rascal this cannot be changed. The descriptions below describe the cases when an evaluator is started in sandbox mode.

  Disabling |@java| annotations on non library functions

During importing of a module, we check in case of a |@java| annotation if the current module is on a white listed path (containing the library paths).

  Blacklisting unsecure rascal functions

We introduce a new annotation |@unsecure| (or a better name?) which is checked during the overload resolution, and if it is called in sandbox mode, we raise a security exception.

  Whitelist locations which can be resolved

The Location resolvers are extended such that when they create a |InputStream| or an |OutputStream| they call our own |SandboxInputStreams| or |SandboxOutputStream| instead. These will check if you try to read or write outside your current path or the loaded eclipse projects.

So our question to you is, are we forgetting a attack vector or is this a secure sandbox?

— Reply to this email directly or view it on GitHub https://github.com/cwi-swat/rascal/issues/19.

DavyLandman commented 12 years ago

@jurgenvinju I agree, but since the file interaction ends up in either Input or Output stream, I thought we could check the path there (and indeed always check an absolute path)

@mahills well, now users can add their own @java functions, so we have to disable this. The blacklisting approach seems more maintainable. I suspect the risk of adding a @unsecure annotation is just as high as someone automatically adding a function to the whitelist.

jurgenvinju commented 12 years ago

davylandman I think if you want security than maintainability is not the

priority.

On Wed, Nov 14, 2012 at 4:05 PM, Davy Landman notifications@github.comwrote:

@jurgenvinju https://github.com/jurgenvinju I agree, but since the file interaction ends up in either Input or Output stream, I thought we could check the path there (and indeed always check an absolute path)

@mahills https://github.com/mahills well, now users can add their own @java functions, so we have to disable this. The blacklisting approach seems more maintainable. I suspect the risk of adding a @unsecureannotation is just as high as someone automatically adding a function to the whitelist.

— Reply to this email directly or view it on GitHubhttps://github.com/cwi-swat/rascal/issues/19#issuecomment-10369093.

Jurgen Vinju

DavyLandman commented 12 years ago

@jurgenvinju yes, it is always a trade-off, I'm thinking that there is only a small set of escape hatches in the current rascal, and marking them as unsafe is simpeler than frequent maintenance of the whitelist.

Apart from the way to allow/disallow methods, are their actual holes in our proposal?

jurgenvinju commented 12 years ago

I don't know. It looks quite thorough. Is there a way to find out? We should search in the Rascal code on all uses of Java I/O facilities.

On Wed, Nov 14, 2012 at 4:28 PM, Davy Landman notifications@github.comwrote:

@jurgenvinju https://github.com/jurgenvinju yes, it is always a trade-off, I'm thinking that there is only a small set of escape hatches in the current rascal, and marking them as unsafe is simpeler than frequent maintenance of the whitelist.

Apart from the way to allow/disallow methods, are their actual holes in our proposal?

— Reply to this email directly or view it on GitHubhttps://github.com/cwi-swat/rascal/issues/19#issuecomment-10370040.

Jurgen Vinju

mahills commented 12 years ago

@jurgenvinju I smell a type and effect system coming

@DavyLandman What is the context for when we want the sandboxing? If the desire is just that a user can submit their own expressions, then I assume they cannot also provide their own Rascal modules with backing Java class files.

jurgenvinju commented 12 years ago

The issue is that you could write a function that binds to an existing unsafe library function:

@javaClass{points.to.unsafeClass} public java int myNewFunction();

On Thu, Nov 15, 2012 at 10:59 AM, mahills notifications@github.com wrote:

@jurgenvinju https://github.com/jurgenvinju I smell a type and effect system coming

@DavyLandman https://github.com/DavyLandman What is the context for when we want the sandboxing? If the desire is just that a user can submit their own expressions, then I assume they cannot also provide their own Rascal modules with backing Java class files.

— Reply to this email directly or view it on GitHubhttps://github.com/cwi-swat/rascal/issues/19#issuecomment-10403062.

Jurgen Vinju

DavyLandman commented 12 years ago

@mahills correct, the user can submit their own expressions, or even full rascal files. but they are not allowed to use @javaClass annotations in their own modules. This is both to protect against @jurgenvinju 's point, and any other kind of java code which the user could then write.