Sandbox environment inside Python?

[Robert'); DROP TABLE *;]

I'm trying to build a web application with Python and Flask, and I've realized that I need a scripting language of some sort to run inside the app. Obviously, I could use Python's eval itself with a restricted environment, but I think even that is rather dangerous. (Not to mention rather syntax heavy for what I want to do.) Keeping in mind that I might let users write scripts for the app, does anyone have any suggestions for what I might use? I don't really want to roll my own, but I also don't know of anything lightweight enough for what I want to do. (which is limited to basically what C can do without any external libraries.)

Also, I have another question, but it's somewhat secondary to the above: I'd like for the script to be guaranteed to halt, but without having to make the environment radically different from what ordinary programming is like. Is there any way to do that? (e.g. by replacing while loops with a similar, but easier to calculate, construct)

[WarDaft]

Just use plain inductive for-loops, that is, a doNTimes operation with the option to break. Lets you implement any primitive recursive function, simple in concept, and guaranteed to halt. There are lots of things it can't do, but really, you can emulate general iteration well enough to be effectively indistinguishable within our universe. Do note that your computer has a finite amount of memory; the appearance of the ability to perform general recursion is a total illusion anyway.

[thoughtfully]

You might consider Lua. It's made for embedding, and is far more lightweight than Python. I'm not sure about running it in a restricted environment, but I wouldn't be surprised if there's a straightforward way.

I don't know how rigorous you need to be, but a really secure restricted environment is generally tricky to achieve short of an embedded virtual machine or carefully designed kernel support. chroot isn't especially secure, for instance. I'm not really familiar with Java, but I think I've read that their restricted environment is better than most. Maybe you should try Jython?

[WarDaft]

Also, I don't know what of this you can do in Python, but the type system in Haskell lets you build tools so that the same program can simultaneously read local data unrestricted, transmit data to any website unrestricted, and still be provably incapable of actually sending out any of your private information to a 3rd party. You can even give it the ability to create files in essentially arbitrary locations quite safely. Basically, you have a Client monad and a Server monad, and runClient and runServer functions, which take types Client () and Server (), and executes them, but in such a way that information cannot escape from them.

Overly simple example, not even using any monadic properties because I'm lazy and sleepy:

Code: Select all

 module Buh where
import Nar

main = runNar $ evil `andThen` fiendish (++"!") `andThen` moreEvil

Code: Select all

module Nar (runNar, evil, moreEvil, andThen, fiendish) where

newtype Nar a = Nar {run :: IO a}

runNar a = run a :: IO ()

evil = Nar $ readFile "secretdata.txt"

fiendish fn = Nar . (>>= return . fn) . run

moreEvil = Nar . \x -> getLine >>= flip writeFile x

andThen a b = Nar $ run a >>= (run . b)

There's nothing module "Buh" can do with the information obtained from evil except for applying pure functions with fiendish, and piping it to moreEvil, which will write the data anywhere the user (well, technically, the program input, in a more complicated example you could make it explicitly a user prompt) tells it to. The program doesn't even have any say in where to put it.
We're ignoring here that Prelude imports readFile and writeFile, which are the functions we're actually trying to hide away securely, but that's not entirely terrible because we can simply check for their use.
If the module contains no readFile or writeFile actions, and imports only Nar, then we have pretty much shown it to be secure as far as the actions hidden by Nar are concerned. If all of the actions you want your script to perform are properly wrapped up like so, and you prove the library secure, then a simple mechanical check is enough to ensure the script is safe not just to interpret in a restricted environment, but compile and run right on the hardware.

[jareds]

Also, I have another question, but it's somewhat secondary to the above: I'd like for the script to be guaranteed to halt, but without having to make the environment radically different from what ordinary programming is like. Is there any way to do that? (e.g. by replacing while loops with a similar, but easier to calculate, construct)

In any sort of reality, you want to set a fixed limit on the CPU time (and probably also memory) that is used. Limiting it to things that are guaranteed to halt doesn't do jack: evaluating the Ackermann function on any input is guaranteed to halt. Similarly, a primitive recursive function might take quadruply exponential time. It should be possible to set up such fixed limits within your sandbox environment. On Linux, if all else fails, you can use "ulimit" on the sandbox itself. Probably other operating systems also have such functionality.