IO sandboxing to prevent access to arbitrary I/O during evaluation

[pchiusano]

This needs design, but we want to be able to evaluate expressions without giving them access to arbitrary IO. This will get used for making sure docs can’t do I/O even if the user subverts the typechecker, and it’ll also be used by the compute node server.

Here’s a sketch:

handlePure blah
with someHandler

I’m imagining that to typecheck blah in a handlePure block, we remove {IO} from the ambient abilities.

And then also at runtime, handlePure disables calling any (certain?) IO functions within blah - it can still make other kinds of requests, and someHandler may do IO on behalf of blah, but that’s what we want - this lets us create more limited abilities that have access to safer subsets of IO.

Alternately, maybe just a new builtin function:

IO.sandbox : (Request {g} a ->{g2} r) -> ‘{g} a ->{g2} r

Runtime support would be the same.

Phase 1 of this is just a design discussion with @dolio

[dolio]

Here's an alternate idea we discussed.

If the concern is just remotely loaded code, we could keep track of which definitions transitively reference primitive IO functions. Then, just refuse to deserialize (or serialize) anything that includes one of those operations (throw an exception). Now remote code can only have IO effects via an intermediate API that the server executing the code knows how to fulfill.

A possible downside is that this relies more on correctness of builtins and compilation. The actual code representation that is sent remotely uses variables, so you can't just arbitrarily craft bad stack references to try to access forbidden things. But, improperly wrapped builtins or compiler bugs could introduce bad stack references, so that is a conceivable attack vector. I'm unsure if the sandboxing wrapper would be completely immune to something like that or not.

[pchiusano]

Thanks for the writeup. It seems like you could also (or instead?) have a builtin, validatePure : a -> Boolean which just checks if any transitive dependencies of the input calls a forbidden function. This would be more useful for the doc evaluation case where you don't really want to have to serialize the example embedded in the doc just to check that it's okay to evaluate.

The validation approach seems pretty good, and easy to implement, so I'm tempted to say let's do it. But it also seems a little backwards - like we're populating the environment with a bunch of forbidden operations and then validating that a block of code doesn't use anything forbidden. I feel like it'd be easier to convince ourselves of correctness if we avoided putting the forbidden stuff in the environment in the first place. You'd need like an extra level of indirection, and maybe that's more complicated. Like I think you have an array of MCode as your environment, but that could instead be a stack of MCode arrays which you could push and pop from in handlePure.

[pchiusano]

Just discussed the following:

io.validateSandboxed : [Link.Term] -> a -> Boolean

It should ensure that any of the transitive dependencies that do IO are in the list. validateSandboxed [] will ensure the value is pure. But you might say validateSandboxed [termLink atomically] to allow STM stuff.