Running `attribute_goals/1` in a sandbox can generate error

SWIP 9.1.18, MacOS 10.14.6

Background info - trying to construct a version of pack(clpBNR) that runs in a sandbox, e.g., for a pengine. Here's a simplified version of attribute_goals/1:

attribute_goals(X) -->                     % constructs goals to build X
    {Goals = [X::real]
    },
    Goals.

This compiles to:

?- listing(clpBNR:attribute_goals).
attribute_goals(X, A, B) :-
    Goals=[X::real],
    C=A,
    phrase(Goals, C, B).

true.

But testing this for "safety" generates an exception:

?- safe_goal(clpBNR:attribute_goals(X,_,_)).
ERROR: Sandbox restriction!
ERROR: Could not derive which predicate may be called fromSearch space too large

presumably because:

[debug]  ?- safe_goal(phrase(Goals,C,B)).
ERROR: Arguments are not sufficiently instantiated
ERROR: In:
ERROR:   [17] throw(error(instantiation_error,_726))
ERROR:   [16] error:instantiation_error(_762) at /Applications/SWI-Prolog9.1.18.app/Contents/swipl/library/error.pl:152
ERROR:   [15] sandbox:expand_nt(_798,_800,_802,_804) at /Applications/SWI-Prolog9.1.18.app/Contents/swipl/library/sandbox.pl:939
ERROR:   [14] sandbox:safe_meta(phrase(_846,_848,_850),[_854]) at /Applications/SWI-Prolog9.1.18.app/Contents/swipl/library/sandbox.pl:895
ERROR:   [13] sandbox:safe_meta_call(phrase(_900,_902,_904),user,[_908]) at /Applications/SWI-Prolog9.1.18.app/Contents/swipl/library/sandbox.pl:962
ERROR:   [12] sandbox:safe(phrase(_958,_960,_962),user,[],t,_954) at /Applications/SWI-Prolog9.1.18.app/Contents/swipl/library/sandbox.pl:198
ERROR:   [11] catch(sandbox:safe(...,user,[],t,_1014),error(instantiation_error,context(_1024,_1026)),sandbox:true) at /Applications/SWI-Prolog9.1.18.app/Contents/swipl/boot/init.pl:563
ERROR:   [10] sandbox:safe_goal(user:phrase(_1078,_1080,_1082)) at /Applications/SWI-Prolog9.1.18.app/Contents/swipl/library/sandbox.pl:122
ERROR:    [9] toplevel_call(user:user:(...)) at /Applications/SWI-Prolog9.1.18.app/Contents/swipl/boot/toplevel.pl:1235
   Exception: (11) throw(error(instantiation_error, context(prolog_stack([frame(17, call(system:throw/1), throw(error(instantiation_error, _270))), frame(16, pred_line("instantiation_error/1", '/Applications/SWI-Prolog9.1.18.app/Contents/swipl/library/error.pl':152), error:instantiation_error(_306)), frame(15, pred_line("expand_nt/4", ... : ...), sandbox:expand_nt(..., ..., ..., ...)), frame(14, pred_line(..., ...), ... : ...), frame(..., ..., ...)|...]), _226))) ? leap

A workaround is to declare clpBNR:attribute_goals/3 a safe_meta but that seems contrary to the spirit of sandboxing. So is this behaviour a bug or a feature?

BTW, shouldn't safe_goal/1 itself be safe?

[debug]  ?- safe_goal(safe_goal(G)).
ERROR: No permission to call sandboxed `nb_linkval(_5598,_5600)'
ERROR: Reachable from:
ERROR:    sandbox:nb_setval(sandbox_last_error,A)
ERROR:    sandbox:safe(A,B,C,D,E)
ERROR:    catch(safe(_5696,user,[],_5702,_5704),_5690,true)
ERROR:    user:safe_goal(A)
   Exception: (11) throw(error(permission_error(call, sandboxed, nb_linkval(_5452, _5454)), sandbox('$syspreds':nb_linkval(_5452, _5454), [sandbox:nb_setval(sandbox_last_error, A), sandbox:safe(A, B, C, D, E), catch(safe(_5550, user, [], _5556, _5558), _5544, true), user:safe_goal(A)]))) ? leap

So is this behaviour a bug or a feature?

Depends :smile: The sandbox tries to establish the reachable call tree and, if necessary, the possible instantiations of variables to specific predicates if a predicate is safe for some instantiations and not for others. Especially when meta-calling is involved, this quickly gets untracktable, so proving safety has a time limit.

BTW, shouldn't safe_goal/1 itself be safe?

Why?

nb_linkval/2 is safe, but apparently missing in the declarations. Could be added, though it is mostly in the "hackers corner".

Anyway, big libraries like clp(fd), chr, s(CASP), etc. cannot be proven by the sandbox in most cases. You need to carefully evaluate the safety of the internals and then declare the API to be safe. Note that a safe predicate is assumed to be unable to make permanent changes to the Prolog system as well as external resources such as files. It should not be able to affect or peek into other modules (and the file system) except by using the public interface. Notably cross-module calls and assert/retract must be impossible. Changing existing flags is typically fine as the changes are local to the thread.

P.s. why not simply attribute_goals(X) --> [X::real]?

BTW, shouldn't safe_goal/1 itself be safe?

Why?

In my particular scenario, I would like to support user defined interval primitives. When they are compiled, I would like to check if they are meet the API requirements and they safe before adding them to the "constraint store". Right now I can check validity using clause or predicate_property (with appropriate sandbox declaration) but can't vouch for safety.

nb_linkval/2 is safe, but apparently missing in the declarations. Could be added, though it is mostly in the "hackers corner".

A couple of points. First I believe nb_linkval and relatives have a legitimate (i.e., non-hacker) application for operational measurements (e.g., count of virtual machine instructions) and for directed searches, e.g., for global optima.

Second, I'm not so sure the problem is with nb_linkval. It appears to me that somewhere in the safe reachability tests, the global variable name gets lost so the safe_global_variable test fails (it's a var). I have an internal wrapper predicate for nb_linkval:

g_assign(G,V)  :- nb_linkval(G,V).

Given a "safe" global name, it succeeds; given a variable name argument, it errors (as you would expect):

[debug]  ?- safe_goal(clpBNR:g_assign('clpBNR:thread_init_done',true)).
true.

[debug]  ?- safe_goal(clpBNR:g_assign(G,true)).
ERROR: Sandbox restriction!
ERROR: Could not derive which predicate may be called from
ERROR:    system:nb_linkval(C,true)
ERROR:    clpBNR:g_assign(A,true)
   Exception: (11) throw(error(instantiation_error, sandbox(_1292, [system:nb_linkval(_1310, true), clpBNR:g_assign(A, true)]))) ? leap

At the very least, the diagnostic information is misleading. And given that global variables are thread local, I'm not really sure why the names have to be safe_global_variable declared in any case.

Anyway, big libraries like clp(fd), chr, s(CASP), etc. cannot be proven by the sandbox in most cases. You need to carefully evaluate the safety of the internals and then declare the API to be safe.

I'm taking a different approach (for now) - add only necessary sandbox declarations for external predicates so that all exported predicates (and the initialization code) pass the safe_goal test. And I now have a version that does that. I think that's a more robust approach than trying to satisfy yourself that a blanket safety declaration at the API level is correct, although it certainly depends on the details.

A draft safe_module test:

:- module(safety, [safe_module/2]).
:- use_module(library(sandbox),[safe_goal/1]).

safe_module(M,InitGoal) :-
    findall(M:H,predicate_property(M:H,exported),Exported),
    safe_goals_([InitGoal|Exported]).

safe_goals_([]).
safe_goals_([Goal|Goals]) :-
    safe_goal(Goal),
    safe_goals_(Goals).

E.g.,

[debug]  ?- safe_module(clpBNR, clpBNR:init_clpBNR).
true.

Note that a safe predicate is assumed to be unable to make permanent changes to the Prolog system as well as external resources such as files. It should not be able to affect or peek into other modules (and the file system) except by using the public interface. Notably cross-module calls and assert/retract must be impossible. Changing existing flags is typically fine as the changes are local to the thread.

For the module in question, no need to access external resources and I generally avoid assert/retract as a matter of principle. I would like to create "local" flags (e.g., limits on fixed point iteration) for convenience, but that's more for historical reasons.

P.s. why not simply attribute_goals(X) --> [X::real]?

Because that was just a simple example to demonstrate the point. Actual code looks like:

attribute_goals(X) -->                     % constructs goals to build X
    {current_prolog_flag(clpBNR_verbose,Verbose),  % details depend on flag clpBNR_verbose
     % may be called from pce thread where global doesn't exist
     catch(g_read('clpBNR:bindings',Bindings),error(existence_error(variable, _),_Ctxt),Bindings=any),
     domain_goals_(Verbose,Bindings,X,Goals)
    },
    Goals.

where domain_goals/4 reverse compiles X's clpBNR attribute back to source constraints. The current workaround is to add:

sandbox:safe_meta(clpBNR:attribute_goals(X,A,B), []).

That's OK but I don't think it should be necessary.

For the record, it's not real clear to me why some sandbox declarations on external predicates work and some don't. E.g., given:

sandbox:safe_primitive(system:prolog_current_frame(F)).
sandbox:safe_primitive(system:prolog_frame_attribute(F,parent_goal,Goal)) :-
    functor(Goal,doNode,_).

The first declaration is accepted while the second results in:

ERROR:    No permission to declare safe_goal `system:prolog_frame_attribute(_4570,parent_goal,_4574)'

at load time.

Second, I'm not so sure the problem is with nb_linkval. It appears to me that somewhere in the safe reachability tests, the global variable name gets lost so the safe_global_variable test fails (it's a var). I have an internal wrapper predicate for nb_linkval:

Not really. Several libraries use global variables to store goals. The library may ensure the goal is safe, but once we can assign any global variable to anything we can write the variable and call verified APIs of the library to make it do whatever we want.

You could get away defining the global var sandbox_last_error as safe. You can misuse it to make safe_goal return misleading results, but that is about it as far as I can see. If it works for you, I'm happy to add that to the library.

attribute_goals(X) --> % constructs goals to build X {current_prolog_flag(clpBNR_verbose,Verbose), % details depend on flag clpBNR_verbose % may be called from pce thread where global doesn't exist catch(g_read('clpBNR:bindings',Bindings),error(existenceerror(variable, ),_Ctxt),Bindings=any), domaingoals(Verbose,Bindings,X,Goals) }, Goals.

The system would have to prove that Goals is a list. That may get rather hard. The way to do this is to use list(Goals) with list//1 defined as list([]) --> []. list[H|T]) --> [H], list(T).. That, b.t.w. is also a lot faster than calling phrase//1.

ERROR: No permission to declare safe_goal `system:prolog_frame_attribute(_4570,parent_goal,_4574)'

prolog_frame_attribute/3 is a meta predicate. They have their own safe declaration (and yes, the message could be better).

P.s. The safe_module test is interesting. Both for verifying libraries as for optimization in safe_goal/2. Well, it touches the idea that we should possibly cache and reuse proven safety of predicates that do not come from the SWISH query. That would allow more complex libraries to rely on the sandbox and indeed only define minimal parts of the code as `safe'.

P.s. prolog_frame_attribute/3 is not safe. It provides access to stacked goals and allows unifying variables in parent frames to anything we want. One of these variables could be in use as a goal in one of the parent predicates.

Not really. Several libraries use global variables to store goals. The library may ensure the goal is safe, but once we can assign any global variable to anything we can write the variable and call verified APIs of the library to make it do whatever we want.

Fair enough. Perhaps I'm missing something, but can't I wrap any any unsafe goal in a local predicate, declare it safe, and do pretty much anything I want? If so, the foundation is pretty shaky so is there any point in quibbling about the doorway? What would be helpful is a more formal definition of what is considered "safe".

You could get away defining the global var sandbox_last_error as safe. You can misuse it to make safe_goal return misleading results, but that is about it as far as I can see. If it works for you, I'm happy to add that to the library.

Yes (with respect to safe_goal), but then you just hit the next wall:

[debug]  ?- safe_goal(safe_goal(G)).
ERROR: No permission to call sandboxed `'$current_module'(_4486,_4488)'
ERROR: Reachable from:
ERROR:    sandbox:current_module(A)
ERROR:    sandbox:known_module(A:B,C)
ERROR:    sandbox:safe(A,B,C,D,E)
ERROR:    catch(safe(_4618,user,[],_4624,_4626),_4612,true)
ERROR:    user:safe_goal(A)
   Exception: (11) throw(error(permission_error(call, sandboxed, '$current_module'(_4306, _4308)), sandbox('$syspreds':'$current_module'(_4306, _4308), [sandbox:current_module(A), sandbox:known_module(A:B, C), sandbox:safe(A, B, C, D, E), catch(safe(_4438, user, [], _4444, _4446), _4432, true), user:safe_goal(...)]))) ? leap

Also, is maliciously generating "misleading results" considered "unsafe"? (See previous point about a formal definition). It is certainly highly undesirable (as are most "bugs").

The system would have to prove that Goals is a list. That may get rather hard. The way to do this is to use list(Goals) with list//1 defined as list([]) --> []. list[H|T]) --> [H], list(T).. That, b.t.w. is also a lot faster than calling phrase//1.

I generated this issue since I thought this pattern (output as variable Goals in a dcg clause) would be a not uncommon pattern and might be worth fixing in general. But this is a good solution, although perhaps not an obvious one, at least to me.

P.s. prolog_frame_attribute/3 is not safe. It provides access to stacked goals and allows unifying variables in parent frames to anything we want. One of these variables could be in use as a goal in one of the parent predicates.

This is a minor irritant. I only used it as an example where some system predicates can be declared safe while others can't and the reason for that isn't very clear. Note that in my particular case, the frame must match a parent goal in the same context (clpBNR) so I don't see that as unsafe.

P.s. The safe_module test is interesting. Both for verifying libraries as for optimization in safe_goal/2. Well, it touches the idea that we should possibly cache and reuse proven safety of predicates that do not come from the SWISH query. That would allow more complex libraries to rely on the sandbox and indeed only define minimal parts of the code as `safe'.

So my ultimate dream (probably a pipe dream) is to be able to run clpBNR on SWISH as a pack so I can create notebooks of small tutorials and allow users to experiment online, as well as providing an easily accessible alternate platform for testing. In the short term, the objective is to just ensure that the library can run on a pengine and identify any problem "features". That will generate a small list of sandbox additions, but I'll post that on discourse since it may be of wider interest.

I'm happy to close this issue as there is a good solution that doesn't rely an a sandbox declaration.

Perhaps I'm missing something, but can't I wrap any any unsafe goal in a local predicate, declare it safe, and do pretty much anything I want?

As someone who maintains the SWISH/Pengine server instance, yes. Not as a user though as you define something safe by adding rules to another module, which is considered unsafe.

But yes, it is not the best security. As you see, it is fairly complicated and bugs have been found several times. SWISH instances are supposed to run in an OS sandbox to limit the damage to the running process.

ERROR: sandbox:current_module(A)

We want to keep that unsafe, in part because the UUID module of other Pengines would allow you to steel connections. Also, as you work in just one (temporary) module, reasoning about modules has no purpose.

Also, is maliciously generating "misleading results" considered "unsafe"? (See previous point about a formal definition). It is certainly highly undesirable (as are most "bugs").

I don't think this is "unsafe". You can only trick your own safety checks and you can't trick them to consider something unsafe to be safe. You can only make safe_goal/2 consider something unsafe that is safe or report something unsafe for the wrong reason. You'll have to do that yourself, so I'd say "good luck with it" :smile:

I only used it as an example where some system predicates can be declared safe while others can't and the reason for that isn't very clear.

True. Error messages can be improved. Although I'm not too concerned with error messages from declarations, but more from user code.

Note that in my particular case, the frame must match a parent goal in the same context (clpBNR) so I don't see that as unsafe.

Your usage may be safe, but by adding this predicate as safe to the sandbox you open doors. You should either make only certain attributes safe (those that are safe, such as getting the depth of the frame) or you must make sure that the smallest component using these calls is safe and then declare it as safe. As you have seen from some of these examples, making sure code is safe is not trivial :cry:

I generated this issue since I thought this pattern (output as variable Goals in a dcg clause) would be a not uncommon pattern and might be worth fixing in general.

But, it it only safe if we know the generated term is a list or a safe goal. That is often hard to prove. As is, we typically try to prove the most general call to a predicate to be safe. If that works, all is pretty fast. If not, we must generate more instantiated goals, but this very quickly leads to a combinatorial explosion. Indeed it is a common pattern, but few people realize it triggers the relative expensive dynamic call to phrase/3 while they simply wish to emit a terminal (when sufficiently instantiated, calls to phrase/2,3 are rewritten to normal static calls by library(apply_macros)).

I'd welcome clpBNR in SWISH! I'm not aware of all the details. This type of library is typically doable though. Just about anything involving attributed variables will need help to get past the sandbox. Typically eliminating call/1 is a good thing. I see people binding X to true or false and than use ( X->...;...). Looks nice, but is harder to proof safe and X == true is safe and faster.

As someone who maintains the SWISH/Pengine server instance, yes. Not as a user though as you define something safe by adding rules to another module, which is considered unsafe.

I'm probably not understanding your point, but I interpret this to mean that the actual act of defining a safe primitive (or global, prolog flag, etc) is itself unsafe because it adds rules to the the sandbox module. Taken literally, this means there's no mechanism for defining safe code that goes beyond what the sandbox strictly defines (e.g., one that uses global variables) and therefore no point in defining the sandbox hooks, and I'm pretty sure that's not the intent here.

Just to be clear, I was suggesting if you wanted to use an unsafe primitive, e.g., current_module/1 in a module (or even exporting it), doesn't the following work:

:- module(my_module, [my_current_module/1]).

my_current_module(M) :- current_module(M).

sandbox:safe_primitive(my_module:my_current_module(_)).

And if this works for current_module/1, surely it will work for any code that the sandbox, by default, considers unsafe. Which is why I said the foundation looks rather shaky (i.e., not strictly enforceable).

As you have seen from some of these examples, making sure code is safe is not trivial 😢

Well it's not a trivial exercise, but once you have a basic grasp of what's going on, it's not too bad. The vast majority of the code in clpBNR is already safe, but there are a few "features", focused mainly on developer support tools, that raised some issues. Here's a current summary of what I had to do to pass my simple safe_module check (apologies for the lengthy details but thought you should have the opportunity to assess the "process"):

Declare module specific global variables and prolog flags to be safe (via safe_global_variable/1 and safe_prolog_flag/2.

Add the following to the sandbox white list (I put them in a separate module for testing purposes).


% candidates for whitelist
sandbox:safe_primitive(system:current_arithmetic_function(_)).
sandbox:safe_primitive(system:bounded_number(_,_,_)).
sandbox:safe_primitive(system:create_prolog_flag(Flag,Value,_)) :-
atom(Flag),
sandbox:safe_prolog_flag(Flag,Value).

sandbox:safe_primitive(prologdebug:debug()). % enable/disable debug topic sandbox:safe_primitive(prologdebug:nodebug()).

sandbox:safe_primitive(system:prolog_currentframe()). % for retrieving executing interval primitive for messages sandbox:safe_primitive(system:'$set_prologstack'(,,,_)). % for setting global min_free

I don't think these are particularly contentious but I can expand on the need if necessary.

3. In producing debug and trace (for the clpBNR fixed point iteration) messages (using prolog_debug:debug/3`) to retrieve the currently executing interval primitive operation from the execution stack. This requires the use of `prolog_frame_attribute/3` which is "unsafe" in general. In the spirit of:
> You should either make only certain attributes safe (those that are safe, such as getting the depth of the frame) or you must make sure that the smallest component using these calls is safe and then declare it as safe. 

I define a restricted usage predicate for safety:

clpBNR_doNodeop(parent_goal,Frame,Op,Args) :- prolog_frame_attribute(Frame,parentgoal,doNode(Args,Op,,,,,_)). clpBNR_doNodeop(goal,Frame,Op,Args) :- prolog_frameattribute(Frame,goal,Goal), Goal = clpBNR:doNode(Args,Op,,,,,_).

sandbox:safe_primitive(clpBNR:clpBNR_doNodeop(,,,)).


4. As mentioned previously, there is a hook for application code to define extensions to the pre-defined set interval primitives. I would like to check these are "safe" when the constraint is "compiled" prior to adding it to the constraint network. Ideally, I would like to use `safe_goal/1` to ensure its safety as well as conformance with the API. I don't know quite how to do that, so I'm currently using `'$syspreds':predicate_property/2` which is currently defined to be unsafe.  So the code looks something like:

    .
    .
Head =..[Prim,'$op',_,_,_],
predicate_property(Head, implementation_module(clpBNR)), 
    .
    .

sandbox:safe_primitive('$syspreds':predicate_property(UsrHead,implementation_module(clpBNR))).

% to invoke user defined primitive call_user_primitive(Prim, P, InArgs, OutArgs) :- call(clpBNR:Prim, '$op', InArgs, OutArgs, P).

sandbox:safe_meta(clpBNR:call_user_primitive(Prim, P, InArgs, OutArgs), []).

5. This one is pretty dubious and I suspect won't even work on a pengine. There's a developer feature that monitors any changes in an interval's value and will optionally invoke the debugger using `trace/0` on changes.  To declare safety:

sandbox:safe_primitive(clpBNR:monitoraction(trace, Update, Int)).

I suppose one approach is to detect when the execution is on a pengine (using `pengine_self/1`?) and only call `trace` when this fails, but I'd like to avoid specific runtime dependancies on pengines. What does happen if the interactive debugger gets called on a pengine? 

6. The clpBNR trace feature actually depends on having a functioning debugger running for the purposes "hooking" the main fixed point iteration predicate (`clpBNR:doNode_`, also see 3.) A `user:prolog_trace_interception/4` handler is used to implement the trace using the information provided by `clpBNR_doNode_op_/4` (again see 3.).  `spy/1` is (selectively) used to enable the trace mechanism, so:

spydoNode(true) :- spy(clpBNR:doNode_). spydoNode(false) :- nospy(clpBNR:doNode_).

sandbox:safe_primitive(clpBNR:spydoNode(B)).

I rather think this is a neat solution to implementing a trace feature with zero overhead when it's not being used - hackery at it's finest, IMHO.

7. The original clpBNR had a specific `print_interval(Term)` and `print_interval(Stream,Term)`for outputting terms containing intervals. They currently use `format` via:

printinterval(Stream, Out) :- % restricted use of streams for historical compatibility format(Stream,'~w',[Out]). % direct output

sandbox:safe_primitive(clpBNR:printinterval(Stream, Out)).

There are better ways of doing this in SWIP so the only reason for keeping them is backwards compatibility; open question as to if/how this should be supported going forward,

8. To support the public labelling predicates, there are two internal meta predicates that are declared safe (by inspection):

sandbox:safemeta(clpBNR:simplesolveall(Xs,Err), []).

sandbox:safe_meta(clpBNR:xpsolveeach(Xs,Us,Err), []).



So this took a few days to enable clpBNR to pass the `safe_module` test while I climbed the learning curve, but I think this could be done much quicker the next time. Having a few tools (like `safe_module/2`) certainly helps. And I think using limited sandbox hooks as done here helps to focus on the why, as well as the what, of any safety issues. 

> I'd welcome clpBNR in SWISH! I'm not aware of all the details. This type of library is typically doable though. 

That's encouraging. Hopefully the lengthy description above will give you a sense of the details. I think the current implementation is fairly sanitary - no C code or database mods, a few (essential) meta predicates, and  limited I/O, largely using existing message support - but this is my first crack at doing anything like this. 

clpBNR is currently available as an add-on pack and my first objective is to ensure it runs on a pengine and to identify any resulting limitations. Is there any "roadmap" to get from that point to making it available on SWISH?

I think I answered most of this by mail, no? Something seems inconsistent between mails and the github issues page.

Is there any "roadmap" to get from that point to making it available on SWISH?

I decide what is around in swish.swi-prolog.org. If you think the clpBNR pack is ready to go, I can add it to the pack selection that ships with SWISH. Concrete, that implies adding the repo as a git submodule and adding a rule to the Makefile. Finally push this to the production version.

Thanks for taking the time to read and respond. It's somewhat odd that you can't see my previous post on github - it's visible to me.

Anyway, I need to take some time to digest this and actually do some testing with pengines.

I'll use discourse in future, as this "issue" has served its purpose.

SWI-Prolog / swipl-devel

Running `attribute_goals/1` in a sandbox can generate error #1206