Even more bare baremodule

Sandboxes are useful for defining smaller teaching languages (see Racket and the HTDP2e book) and, if they can be made secure, for evaluating untrusted code in a capability programming paradigm.

Here’s my attempt at building a sandbox with the currently available tools. Big thanks to Mason (who wrote the first version) and Thautwarm (who wrote MLStyle.jl).

Executing this code should dump you in a Sandbox REPL where the only literals available are true and false and the only function is nand(a, b). You are invited to build your own computer from there :wink:

It’s just a proof of concept, so don’t mind the slightly strange design decisions.

# With thanks to Mason Protter and Thautwarm :)

using ReplMaker, MLStyle

baremodule Sandbox end
@eval Sandbox nand(x, y) = $(!)($(&)(x, y))


name_shadow_dict = let 
    # ccall isn't in Core, it's a special-cased thing that appears in the AST
    # as a regular function call. I think it's the only one but idk.
    forbidden_names = setdiff([:ccall, names(Core; all=true, imported=true)...],
                              names(Sandbox; all=true, imported=true))
    Dict(n => gensym() for n in forbidden_names)
end
inverse_name_shadow_dict = Dict(reverse.(collect(name_shadow_dict)))


function sandbox_eval_expr(ex)
    filterer(ex) = @match ex begin
        x::Bool => x

        x::LineNumberNode => x

        # Ban everything.
        # Edit anything you want to allow.

        # It's a bit complicated to work out when a symbol is being used as a
        # reference and what scope it is in. I think the JuliaVariables people
        # have maybe done something with that?
        #
        # Anyway, we can keep it simple and just shadow all symbols accessible
        # in a baremodule.
        s::Symbol => get(name_shadow_dict, s, s)

        # Not allowed to import stuff
        Expr(:using, _...) ||
        Expr(:import, _...) => error("Imports are not permitted in the sandbox: $ex")

        # Julia literals, these are mostly or entirely harmless (I think)
        # but you might want to omit them or rewrite them to something else or whatever.
        ::Bool ||
        ::Number ||
        ::String ||
        Expr(:string, _...) || # string interpolation
        ::QuoteNode ||
        Expr(:quote, _...) ||
        Expr(:ref, _...) || # a[i], but also Int[]
        Expr(:typed_vcat, _...) ||
        Expr(:typed_hcat, _...) ||
        Expr(:vect, _...) ||
        Expr(:vcat, _...) ||
        Expr(:hcat, _...) ||
        Expr(:tuple, _...) || # also covers named tuples
        Expr(:comprehension, _...) ||
        Expr(:typed_comprehension, _...) ||
        Expr(:generator, _...) => error("This literal is not permitted in the sandbox: $ex")

        # Recurse
        Expr(head, args...) => Expr(head, filterer.(args)...)

        x => error("Unknown node type: $x")
    end
    # The try-catch is just fixing up error messages, you can ignore it.
    :(
        try
            (@eval Sandbox $(filterer(ex)))
        catch e
            if e isa UndefVarError && haskey(inverse_name_shadow_dict, e.var)
                rethrow(UndefVarError(inverse_name_shadow_dict[e.var]))
            else
                rethrow()
            end
        end
    )
end


function sandbox_parser(s::String)
    ex = Meta.parse(s)
    sandbox_eval_expr(ex)
end


function valid_julia(s)
    input = String(take!(copy(ReplMaker.LineEdit.buffer(s))))
    ex = Meta.parse(input)
    !(ex isa Expr && ex.head == :incomplete)
end


sandbox_mode = initrepl(sandbox_parser;
                        prompt_text="Sandbox> ",
                        prompt_color = :yellow,
                        startup_text = false,
                        mode_name = :sandbox,
                        valid_input_checker = valid_julia)


enter_mode!(sandbox_mode)

Edit: you can also escape this with module X end; X.eval(...), but that’s trivial to ban.

6 Likes