1/* Part of SWI-Prolog 2 3 Author: Jan Wielemaker 4 E-mail: J.Wielemaker@vu.nl 5 WWW: http://www.swi-prolog.org 6 Copyright (c) 2013-2016, VU University Amsterdam 7 All rights reserved. 8 9 Redistribution and use in source and binary forms, with or without 10 modification, are permitted provided that the following conditions 11 are met: 12 13 1. Redistributions of source code must retain the above copyright 14 notice, this list of conditions and the following disclaimer. 15 16 2. Redistributions in binary form must reproduce the above copyright 17 notice, this list of conditions and the following disclaimer in 18 the documentation and/or other materials provided with the 19 distribution. 20 21 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 22 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 23 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 24 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE 25 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, 26 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, 27 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 28 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER 29 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT 30 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN 31 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 32 POSSIBILITY OF SUCH DAMAGE. 33*/ 34 35:- module(sandbox, 36 [ safe_goal/1, % :Goal 37 safe_call/1 % :Goal 38 ]). 39:- use_module(library(assoc)). 40:- use_module(library(lists)). 41:- use_module(library(debug)). 42:- use_module(library(error)). 43:- use_module(library(prolog_format)). 44:- use_module(library(apply)). 45 46:- multifile 47 safe_primitive/1, % Goal 48 safe_meta_predicate/1, % Name/Arity 49 safe_meta/2, % Goal, Calls 50 safe_meta/3, % Goal, Context, Calls 51 safe_global_variable/1, % Name 52 safe_directive/1. % Module:Goal 53 54% :- debug(sandbox).
70:- meta_predicate
71 safe_goal( ),
72 safe_call( ).
84safe_call(Goal0) :-
85 expand_goal(Goal0, Goal),
86 safe_goal(Goal),
87 call(Goal).
111safe_goal(M:Goal) :- 112 empty_assoc(Safe0), 113 catch(safe(Goal, M, [], Safe0, _), E, true), 114 !, 115 nb_delete(sandbox_last_error), 116 ( var(E) 117 -> true 118 ; throw(E) 119 ). 120safe_goal(_) :- 121 nb_current(sandbox_last_error, E), 122 !, 123 nb_delete(sandbox_last_error), 124 throw(E). 125safe_goal(G) :- 126 debug(sandbox(fail), 'safe_goal/1 failed for ~p', [G]), 127 throw(error(instantiation_error, sandbox(G, []))).
134safe(V, _, Parents, _, _) :- 135 var(V), 136 !, 137 Error = error(instantiation_error, sandbox(V, Parents)), 138 nb_setval(sandbox_last_error, Error), 139 throw(Error). 140safe(M:G, _, Parents, Safe0, Safe) :- 141 !, 142 must_be(atom, M), 143 must_be(callable, G), 144 known_module(M:G, Parents), 145 ( predicate_property(M:G, imported_from(M2)) 146 -> true 147 ; M2 = M 148 ), 149 ( ( safe_primitive(M2:G) 150 ; safe_primitive(G), 151 predicate_property(G, iso) 152 ) 153 -> Safe = Safe0 154 ; ( predicate_property(M:G, exported) 155 ; predicate_property(M:G, public) 156 ; predicate_property(M:G, multifile) 157 ; predicate_property(M:G, iso) 158 ; memberchk(M:_, Parents) 159 ) 160 -> safe(G, M, Parents, Safe0, Safe) 161 ; throw(error(permission_error(call, sandboxed, M:G), 162 sandbox(M:G, Parents))) 163 ). 164safe(G, _, Parents, _, _) :- 165 debugging(sandbox(show)), 166 length(Parents, Level), 167 debug(sandbox(show), '[~D] SAFE ~q?', [Level, G]), 168 fail. 169safe(G, _, Parents, Safe, Safe) :- 170 catch(safe_primitive(G), 171 error(instantiation_error, _), 172 rethrow_instantition_error([G|Parents])), 173 predicate_property(G, iso), 174 !. 175safe(G, M, Parents, Safe, Safe) :- 176 known_module(M:G, Parents), 177 ( predicate_property(M:G, imported_from(M2)) 178 -> true 179 ; M2 = M 180 ), 181 ( catch(safe_primitive(M2:G), 182 error(instantiation_error, _), 183 rethrow_instantition_error([M2:G|Parents])) 184 ; predicate_property(M2:G, number_of_rules(0)) 185 ), 186 !. 187safe(G, M, Parents, Safe0, Safe) :- 188 predicate_property(G, iso), 189 safe_meta_call(G, M, Called), 190 !, 191 add_iso_parent(G, Parents, Parents1), 192 safe_list(Called, M, Parents1, Safe0, Safe). 193safe(G, M, Parents, Safe0, Safe) :- 194 ( predicate_property(M:G, imported_from(M2)) 195 -> true 196 ; M2 = M 197 ), 198 safe_meta_call(M2:G, M, Called), 199 !, 200 safe_list(Called, M, Parents, Safe0, Safe). 201safe(G, M, Parents, Safe0, Safe) :- 202 goal_id(M:G, Id, Gen), 203 ( get_assoc(Id, Safe0, _) 204 -> Safe = Safe0 205 ; put_assoc(Id, Safe0, true, Safe1), 206 ( Gen == M:G 207 -> safe_clauses(Gen, M, [Id|Parents], Safe1, Safe) 208 ; catch(safe_clauses(Gen, M, [Id|Parents], Safe1, Safe), 209 error(instantiation_error, Ctx), 210 unsafe(Parents, Ctx)) 211 ) 212 ), 213 !. 214safe(G, M, Parents, _, _) :- 215 debug(sandbox(fail), 216 'safe/1 failed for ~p (parents:~p)', [M:G, Parents]), 217 fail. 218 219unsafe(Parents, Var) :- 220 var(Var), 221 !, 222 nb_setval(sandbox_last_error, 223 error(instantiation_error, sandbox(_, Parents))), 224 fail. 225unsafe(_Parents, Ctx) :- 226 Ctx = sandbox(_,_), 227 nb_setval(sandbox_last_error, 228 error(instantiation_error, Ctx)), 229 fail. 230 231rethrow_instantition_error(Parents) :- 232 throw(error(instantiation_error, sandbox(_, Parents))). 233 234safe_clauses(G, M, Parents, Safe0, Safe) :- 235 predicate_property(M:G, interpreted), 236 def_module(M:G, MD:QG), 237 \+ compiled(MD:QG), 238 !, 239 findall(Ref-Body, clause(MD:, Body, Ref), Bodies), 240 safe_bodies(Bodies, MD, Parents, Safe0, Safe). 241safe_clauses(G, M, [_|Parents], _, _) :- 242 predicate_property(M:G, visible), 243 !, 244 throw(error(permission_error(call, sandboxed, G), 245 sandbox(M:G, Parents))). 246safe_clauses(_, _, [G|Parents], _, _) :- 247 throw(error(existence_error(procedure, G), 248 sandbox(G, Parents))). 249 250compiled(system:(@(_,_))). 251 252known_module(M:_, _) :- 253 current_module(M), 254 !. 255known_module(M:G, Parents) :- 256 throw(error(permission_error(call, sandboxed, M:G), 257 sandbox(M:G, Parents))). 258 259add_iso_parent(G, Parents, Parents) :- 260 is_control(G), 261 !. 262add_iso_parent(G, Parents, [G|Parents]). 263 264is_control((_,_)). 265is_control((_;_)). 266is_control((_->_)). 267is_control((_*->_)). 268is_control(\+(_)).
277safe_bodies([], _, _, Safe, Safe). 278safe_bodies([Ref-H|T], M, Parents, Safe0, Safe) :- 279 ( H = M2:H2, nonvar(M2), 280 clause_property(Ref, module(M2)) 281 -> copy_term(H2, H3), 282 CM = M2 283 ; copy_term(H, H3), 284 CM = M 285 ), 286 safe(H3, CM, Parents, Safe0, Safe1), 287 safe_bodies(T, M, Parents, Safe1, Safe). 288 289def_module(M:G, MD:QG) :- 290 predicate_property(M:G, imported_from(MD)), 291 !, 292 meta_qualify(MD:G, M, QG). 293def_module(M:G, M:QG) :- 294 meta_qualify(M:G, M, QG).
302safe_list([], _, _, Safe, Safe). 303safe_list([H|T], M, Parents, Safe0, Safe) :- 304 ( H = M2:H2, 305 M == M2 % in our context 306 -> copy_term(H2, H3) 307 ; copy_term(H, H3) % cross-module call 308 ), 309 safe(H3, M, Parents, Safe0, Safe1), 310 safe_list(T, M, Parents, Safe1, Safe).
316meta_qualify(MD:G, M, QG) :- 317 predicate_property(MD:G, meta_predicate(Head)), 318 !, 319 G =.. [Name|Args], 320 Head =.. [_|Q], 321 qualify_args(Q, M, Args, QArgs), 322 QG =.. [Name|QArgs]. 323meta_qualify(_:G, _, G). 324 325qualify_args([], _, [], []). 326qualify_args([H|T], M, [A|AT], [Q|QT]) :- 327 qualify_arg(H, M, A, Q), 328 qualify_args(T, M, AT, QT). 329 330qualify_arg(S, M, A, Q) :- 331 q_arg(S), 332 !, 333 qualify(A, M, Q). 334qualify_arg(_, _, A, A). 335 336q_arg(I) :- integer(I), !. 337q_arg(:). 338q_arg(^). 339q_arg(//). 340 341qualify(A, M, MZ:Q) :- 342 strip_module(M:A, MZ, Q).
354goal_id(M:Goal, M:Id, Gen) :- 355 !, 356 goal_id(Goal, Id, Gen). 357goal_id(Var, _, _) :- 358 var(Var), 359 !, 360 instantiation_error(Var). 361goal_id(Atom, Atom, Atom) :- 362 atom(Atom), 363 !. 364goal_id(Term, _, _) :- 365 \+ compound(Term), 366 !, 367 type_error(callable, Term). 368goal_id(Term, Skolem, Gen) :- % most general form 369 compound_name_arity(Term, Name, Arity), 370 compound_name_arity(Skolem, Name, Arity), 371 compound_name_arity(Gen, Name, Arity), 372 copy_goal_args(1, Term, Skolem, Gen), 373 ( Gen =@= Term 374 -> ! % No more specific one; we can commit 375 ; true 376 ), 377 numbervars(Skolem, 0, _). 378goal_id(Term, Skolem, Term) :- % most specific form 379 debug(sandbox(specify), 'Retrying with ~p', [Term]), 380 copy_term(Term, Skolem), 381 numbervars(Skolem, 0, _).
388copy_goal_args(I, Term, Skolem, Gen) :- 389 arg(I, Term, TA), 390 !, 391 arg(I, Skolem, SA), 392 arg(I, Gen, GA), 393 copy_goal_arg(TA, SA, GA), 394 I2 is I + 1, 395 copy_goal_args(I2, Term, Skolem, Gen). 396copy_goal_args(_, _, _, _). 397 398copy_goal_arg(Arg, SArg, Arg) :- 399 copy_goal_arg(Arg), 400 !, 401 copy_term(Arg, SArg). 402copy_goal_arg(_, _, _). 403 404copy_goal_arg(Var) :- var(Var), !, fail. 405copy_goal_arg(_:_).
417term_expansion(safe_primitive(Goal), Term) :- 418 ( verify_safe_declaration(Goal) 419 -> Term = safe_primitive(Goal) 420 ; Term = [] 421 ). 422 423systemterm_expansion(sandbox:safe_primitive(Goal), Term) :- 424 \+ current_prolog_flag(xref, true), 425 ( verify_safe_declaration(Goal) 426 -> Term = sandbox:safe_primitive(Goal) 427 ; Term = [] 428 ). 429 430verify_safe_declaration(Var) :- 431 var(Var), 432 !, 433 instantiation_error(Var). 434verify_safe_declaration(Module:Goal) :- 435 must_be(atom, Module), 436 must_be(callable, Goal), 437 ( ok_meta(Module:Goal) 438 -> true 439 ; ( predicate_property(Module:Goal, visible) 440 -> true 441 ; predicate_property(Module:Goal, foreign) 442 ), 443 \+ predicate_property(Module:Goal, imported_from(_)), 444 \+ predicate_property(Module:Goal, meta_predicate(_)) 445 -> true 446 ; permission_error(declare, safe_goal, Module:Goal) 447 ). 448verify_safe_declaration(Goal) :- 449 must_be(callable, Goal), 450 ( predicate_property(system:Goal, iso), 451 \+ predicate_property(system:Goal, meta_predicate()) 452 -> true 453 ; permission_error(declare, safe_goal, Goal) 454 ). 455 456ok_meta(system:assert(_)). 457ok_meta(system:use_module(_,_)). 458ok_meta(system:use_module(_)). 459 460verify_predefined_safe_declarations :- 461 forall(clause(safe_primitive(Goal), _Body, Ref), 462 ( catch(verify_safe_declaration(Goal), E, true), 463 ( nonvar(E) 464 -> clause_property(Ref, file(File)), 465 clause_property(Ref, line_count(Line)), 466 print_message(error, bad_safe_declaration(Goal, File, Line)) 467 ; true 468 ) 469 )). 470 471:- initialization(verify_predefined_safe_declarations, now).
485% First, all ISO system predicates that are considered safe 486 487safe_primitive(true). 488safe_primitive(fail). 489safe_primitive(system:false). 490safe_primitive(repeat). 491safe_primitive(!). 492 % types 493safe_primitive(var(_)). 494safe_primitive(nonvar(_)). 495safe_primitive(system:attvar(_)). 496safe_primitive(integer(_)). 497safe_primitive(float(_)). 498safe_primitive(system:rational(_)). 499safe_primitive(number(_)). 500safe_primitive(atom(_)). 501safe_primitive(system:blob(_,_)). 502safe_primitive(system:string(_)). 503safe_primitive(atomic(_)). 504safe_primitive(compound(_)). 505safe_primitive(callable(_)). 506safe_primitive(ground(_)). 507safe_primitive(system:cyclic_term(_)). 508safe_primitive(acyclic_term(_)). 509safe_primitive(system:is_stream(_)). 510safe_primitive(system:'$is_char'(_)). 511safe_primitive(system:'$is_char_code'(_)). 512safe_primitive(system:'$is_char_list'(_,_)). 513safe_primitive(system:'$is_code_list'(_,_)). 514 % ordering 515safe_primitive(@>(_,_)). 516safe_primitive(@>=(_,_)). 517safe_primitive(==(_,_)). 518safe_primitive(@<(_,_)). 519safe_primitive(@=<(_,_)). 520safe_primitive(compare(_,_,_)). 521safe_primitive(sort(_,_)). 522safe_primitive(keysort(_,_)). 523safe_primitive(system: =@=(_,_)). 524safe_primitive(system:'$btree_find_node'(_,_,_,_,_)). 525 526 % unification and equivalence 527safe_primitive(=(_,_)). 528safe_primitive(\=(_,_)). 529safe_primitive(system:'?='(_,_)). 530safe_primitive(system:unifiable(_,_,_)). 531safe_primitive(unify_with_occurs_check(_,_)). 532safe_primitive(\==(_,_)). 533 % arithmetic 534safe_primitive(is(_,_)). 535safe_primitive(>(_,_)). 536safe_primitive(>=(_,_)). 537safe_primitive(=:=(_,_)). 538safe_primitive(=\=(_,_)). 539safe_primitive(=<(_,_)). 540safe_primitive(<(_,_)). 541 % term-handling 542safe_primitive(arg(_,_,_)). 543safe_primitive(system:setarg(_,_,_)). 544safe_primitive(system:nb_setarg(_,_,_)). 545safe_primitive(system:nb_linkarg(_,_,_)). 546safe_primitive(functor(_,_,_)). 547safe_primitive(_ =.. _). 548safe_primitive(system:compound_name_arity(_,_,_)). 549safe_primitive(system:compound_name_arguments(_,_,_)). 550safe_primitive(system:'$filled_array'(_,_,_,_)). 551safe_primitive(copy_term(_,_)). 552safe_primitive(system:duplicate_term(_,_)). 553safe_primitive(system:copy_term_nat(_,_)). 554safe_primitive(numbervars(_,_,_)). 555safe_primitive(subsumes_term(_,_)). 556safe_primitive(system:term_hash(_,_)). 557safe_primitive(system:term_hash(_,_,_,_)). 558safe_primitive(system:variant_sha1(_,_)). 559safe_primitive(system:variant_hash(_,_)). 560safe_primitive(system:'$term_size'(_,_,_)). 561 562 % dicts 563safe_primitive(system:is_dict(_)). 564safe_primitive(system:is_dict(_,_)). 565safe_primitive(system:get_dict(_,_,_)). 566safe_primitive(system:get_dict(_,_,_,_,_)). 567safe_primitive(system:'$get_dict_ex'(_,_,_)). 568safe_primitive(system:dict_create(_,_,_)). 569safe_primitive(system:dict_pairs(_,_,_)). 570safe_primitive(system:put_dict(_,_,_)). 571safe_primitive(system:put_dict(_,_,_,_)). 572safe_primitive(system:del_dict(_,_,_,_)). 573safe_primitive(system:select_dict(_,_,_)). 574safe_primitive(system:b_set_dict(_,_,_)). 575safe_primitive(system:nb_set_dict(_,_,_)). 576safe_primitive(system:nb_link_dict(_,_,_)). 577safe_primitive(system:(:<(_,_))). 578safe_primitive(system:(>:<(_,_))). 579 % atoms 580safe_primitive(atom_chars(_, _)). 581safe_primitive(atom_codes(_, _)). 582safe_primitive(sub_atom(_,_,_,_,_)). 583safe_primitive(atom_concat(_,_,_)). 584safe_primitive(atom_length(_,_)). 585safe_primitive(char_code(_,_)). 586safe_primitive(system:name(_,_)). 587safe_primitive(system:atomic_concat(_,_,_)). 588safe_primitive(system:atomic_list_concat(_,_)). 589safe_primitive(system:atomic_list_concat(_,_,_)). 590safe_primitive(system:downcase_atom(_,_)). 591safe_primitive(system:upcase_atom(_,_)). 592safe_primitive(system:char_type(_,_)). 593safe_primitive(system:normalize_space(_,_)). 594safe_primitive(system:sub_atom_icasechk(_,_,_)). 595 % numbers 596safe_primitive(number_codes(_,_)). 597safe_primitive(number_chars(_,_)). 598safe_primitive(system:atom_number(_,_)). 599safe_primitive(system:code_type(_,_)). 600 % strings 601safe_primitive(system:atom_string(_,_)). 602safe_primitive(system:number_string(_,_)). 603safe_primitive(system:string_chars(_, _)). 604safe_primitive(system:string_codes(_, _)). 605safe_primitive(system:string_code(_,_,_)). 606safe_primitive(system:sub_string(_,_,_,_,_)). 607safe_primitive(system:split_string(_,_,_,_)). 608safe_primitive(system:atomics_to_string(_,_,_)). 609safe_primitive(system:atomics_to_string(_,_)). 610safe_primitive(system:string_concat(_,_,_)). 611safe_primitive(system:string_length(_,_)). 612safe_primitive(system:string_lower(_,_)). 613safe_primitive(system:string_upper(_,_)). 614safe_primitive(system:term_string(_,_)). 615safe_primitive('$syspreds':term_string(_,_,_)). 616 % Lists 617safe_primitive(length(_,_)). 618 % exceptions 619safe_primitive(throw(_)). 620safe_primitive(system:abort). 621 % misc 622safe_primitive(current_prolog_flag(_,_)). 623safe_primitive(current_op(_,_,_)). 624safe_primitive(system:sleep(_)). 625safe_primitive(system:thread_self(_)). 626safe_primitive(system:get_time(_)). 627safe_primitive(system:statistics(_,_)). 628safe_primitive(system:thread_statistics(Id,_,_)) :- 629 ( var(Id) 630 -> instantiation_error(Id) 631 ; thread_self(Id) 632 ). 633safe_primitive(system:thread_property(Id,_)) :- 634 ( var(Id) 635 -> instantiation_error(Id) 636 ; thread_self(Id) 637 ). 638safe_primitive(system:format_time(_,_,_)). 639safe_primitive(system:format_time(_,_,_,_)). 640safe_primitive(system:date_time_stamp(_,_)). 641safe_primitive(system:stamp_date_time(_,_,_)). 642safe_primitive(system:strip_module(_,_,_)). 643safe_primitive('$messages':message_to_string(_,_)). 644safe_primitive(system:import_module(_,_)). 645safe_primitive(system:file_base_name(_,_)). 646safe_primitive(system:file_directory_name(_,_)). 647safe_primitive(system:file_name_extension(_,_,_)). 648 649safe_primitive(clause(H,_)) :- safe_clause(H). 650safe_primitive(asserta(X)) :- safe_assert(X). 651safe_primitive(assertz(X)) :- safe_assert(X). 652safe_primitive(retract(X)) :- safe_assert(X). 653safe_primitive(retractall(X)) :- safe_assert(X). 654 655% We need to do data flow analysis to find the tag of the 656% target key before we can conclude that functions on dicts 657% are safe. 658safe_primitive('$dicts':'.'(_,K,_)) :- atom(K). 659safe_primitive('$dicts':'.'(_,K,_)) :- 660 ( nonvar(K) 661 -> dict_built_in(K) 662 ; instantiation_error(K) 663 ). 664 665dict_built_in(get(_)). 666dict_built_in(put(_)). 667dict_built_in(put(_,_)). 668 669% The non-ISO system predicates. These can be redefined, so we must 670% be careful to ensure the system ones are used. 671 672safe_primitive(system:false). 673safe_primitive(system:cyclic_term(_)). 674safe_primitive(system:msort(_,_)). 675safe_primitive(system:sort(_,_,_,_)). 676safe_primitive(system:between(_,_,_)). 677safe_primitive(system:succ(_,_)). 678safe_primitive(system:plus(_,_,_)). 679safe_primitive(system:term_variables(_,_)). 680safe_primitive(system:term_variables(_,_,_)). 681safe_primitive(system:'$term_size'(_,_,_)). 682safe_primitive(system:atom_to_term(_,_,_)). 683safe_primitive(system:term_to_atom(_,_)). 684safe_primitive(system:atomic_list_concat(_,_,_)). 685safe_primitive(system:atomic_list_concat(_,_)). 686safe_primitive(system:downcase_atom(_,_)). 687safe_primitive(system:upcase_atom(_,_)). 688safe_primitive(system:is_list(_)). 689safe_primitive(system:memberchk(_,_)). 690safe_primitive(system:'$skip_list'(_,_,_)). 691 % attributes 692safe_primitive(system:get_attr(_,_,_)). 693safe_primitive(system:get_attrs(_,_)). 694safe_primitive(system:term_attvars(_,_)). 695safe_primitive(system:del_attr(_,_)). 696safe_primitive(system:del_attrs(_)). 697safe_primitive('$attvar':copy_term(_,_,_)). 698 % globals 699safe_primitive(system:b_getval(_,_)). 700safe_primitive(system:b_setval(Var,_)) :- 701 safe_global_var(Var). 702safe_primitive(system:nb_getval(_,_)). 703safe_primitive('$syspreds':nb_setval(Var,_)) :- 704 safe_global_var(Var). 705safe_primitive(system:nb_current(_,_)). 706 % database 707safe_primitive(system:assert(X)) :- 708 safe_assert(X). 709 % Output 710safe_primitive(system:writeln(_)). 711safe_primitive('$messages':print_message(_,_)). 712 713 % Stack limits (down) 714safe_primitive('$syspreds':set_prolog_stack(Stack, limit(ByteExpr))) :- 715 nonvar(Stack), 716 stack_name(Stack), 717 catch(Bytes is ByteExpr, _, fail), 718 prolog_stack_property(Stack, limit(Current)), 719 Bytes =< Current. 720 721stack_name(global). 722stack_name(local). 723stack_name(trail). 724 725safe_primitive('$tabling':abolish_all_tables). 726 727 728% use_module/1. We only allow for .pl files that are loaded from 729% relative paths that do not contain /../ 730 731safe_primitive(system:use_module(Spec, _Import)) :- 732 safe_primitive(system:use_module(Spec)). 733safe_primitive(system:use_module(Spec)) :- 734 ground(Spec), 735 ( atom(Spec) 736 -> Path = Spec 737 ; Spec =.. [_Alias, Segments], 738 phrase(segments_to_path(Segments), List), 739 atomic_list_concat(List, Path) 740 ), 741 \+ is_absolute_file_name(Path), 742 \+ sub_atom(Path, _, _, _, '/../'), 743 absolute_file_name(Spec, AbsFile, 744 [ access(read), 745 file_type(prolog), 746 file_errors(fail) 747 ]), 748 file_name_extension(_, Ext, AbsFile), 749 save_extension(Ext). 750 751% support predicates for safe_primitive, validating the safety of 752% arguments to certain goals. 753 754segments_to_path(A/B) --> 755 !, 756 segments_to_path(A), 757 [/], 758 segments_to_path(B). 759segments_to_path(X) --> 760 [X]. 761 762save_extension(pl).
assert(Term)
is safe, which means it asserts in the
current module. Cross-module asserts are considered unsafe. We
only allow for adding facts. In theory, we could also allow for
rules if we prove the safety of the body.771safe_assert(C) :- cyclic_term(C), !, fail. 772safe_assert(X) :- var(X), !, fail. 773safe_assert(_Head:-_Body) :- !, fail. 774safe_assert(_:_) :- !, fail. 775safe_assert(_).
783safe_clause(H) :- var(H), !. 784safe_clause(_:_) :- !, fail. 785safe_clause(_).
793safe_global_var(Name) :- 794 var(Name), 795 !, 796 instantiation_error(Name). 797safe_global_var(Name) :- 798 safe_global_variable(Name).
810safe_meta(system:put_attr(V,M,A), Called) :- 811 !, 812 ( atom(M) 813 -> attr_hook_predicates([ attr_unify_hook(A, _), 814 attribute_goals(V,_,_), 815 project_attributes(_,_) 816 ], M, Called) 817 ; instantiation_error(M) 818 ). 819safe_meta(system:with_output_to(Output, G), [G]) :- 820 safe_output(Output), 821 !. 822safe_meta(system:format(Format, Args), Calls) :- 823 format_calls(Format, Args, Calls). 824safe_meta(system:format(Output, Format, Args), Calls) :- 825 safe_output(Output), 826 format_calls(Format, Args, Calls). 827safe_meta(prolog_debug:debug(_Term, Format, Args), Calls) :- 828 format_calls(Format, Args, Calls). 829safe_meta('$attvar':freeze(_Var,Goal), [Goal]). 830safe_meta(phrase(NT,Xs0,Xs), [Goal]) :- % phrase/2,3 and call_dcg/2,3 831 expand_nt(NT,Xs0,Xs,Goal). 832safe_meta(phrase(NT,Xs0), [Goal]) :- 833 expand_nt(NT,Xs0,[],Goal). 834safe_meta('$dcg':call_dcg(NT,Xs0,Xs), [Goal]) :- 835 expand_nt(NT,Xs0,Xs,Goal). 836safe_meta('$dcg':call_dcg(NT,Xs0), [Goal]) :- 837 expand_nt(NT,Xs0,[],Goal). 838safe_meta('$tabling':abolish_table_subgoals(V), []) :- 839 \+ qualified(V). 840safe_meta('$tabling':current_table(V, _), []) :- 841 \+ qualified(V). 842 843qualified(V) :- 844 nonvar(V), 845 V = _:_.
855attr_hook_predicates([], _, []). 856attr_hook_predicates([H|T], M, Called) :- 857 ( predicate_property(M:H, defined) 858 -> Called = [M:H|Rest] 859 ; Called = Rest 860 ), 861 attr_hook_predicates(T, M, Rest).
869expand_nt(NT, _Xs0, _Xs, _NewGoal) :- 870 strip_module(NT, _, Plain), 871 var(Plain), 872 !, 873 instantiation_error(Plain). 874expand_nt(NT, Xs0, Xs, NewGoal) :- 875 dcg_translate_rule((pseudo_nt --> NT), 876 (pseudo_nt(Xs0c,Xsc) :- NewGoal0)), 877 ( var(Xsc), Xsc \== Xs0c 878 -> Xs = Xsc, NewGoal1 = NewGoal0 879 ; NewGoal1 = (NewGoal0, Xsc = Xs) 880 ), 881 ( var(Xs0c) 882 -> Xs0 = Xs0c, 883 NewGoal = NewGoal1 884 ; NewGoal = ( Xs0 = Xs0c, NewGoal1 ) 885 ).
892safe_meta_call(Goal, _, _Called) :- 893 debug(sandbox(meta), 'Safe meta ~p?', [Goal]), 894 fail. 895safe_meta_call(Goal, Context, Called) :- 896 ( safe_meta(Goal, Called) 897 -> true 898 ; safe_meta(Goal, Context, Called) 899 ), 900 !. % call hook 901safe_meta_call(Goal, _, Called) :- 902 Goal = M:Plain, 903 compound(Plain), 904 compound_name_arity(Plain, Name, Arity), 905 safe_meta_predicate(M:Name/Arity), 906 predicate_property(Goal, meta_predicate(Spec)), 907 !, 908 called(Spec, Plain, Called). 909safe_meta_call(M:Goal, _, Called) :- 910 !, 911 generic_goal(Goal, Gen), 912 safe_meta(M:Gen), 913 called(Gen, Goal, Called). 914safe_meta_call(Goal, _, Called) :- 915 generic_goal(Goal, Gen), 916 safe_meta(Gen), 917 called(Gen, Goal, Called). 918 919called(Gen, Goal, Called) :- 920 compound_name_arity(Goal, _, Arity), 921 called(1, Arity, Gen, Goal, Called). 922 923called(I, Arity, Gen, Goal, Called) :- 924 I =< Arity, 925 !, 926 arg(I, Gen, Spec), 927 ( calling_meta_spec(Spec) 928 -> arg(I, Goal, Called0), 929 extend(Spec, Called0, G), 930 Called = [G|Rest] 931 ; Called = Rest 932 ), 933 I2 is I+1, 934 called(I2, Arity, Gen, Goal, Rest). 935called(_, _, _, _, []). 936 937generic_goal(G, Gen) :- 938 functor(G, Name, Arity), 939 functor(Gen, Name, Arity). 940 941calling_meta_spec(V) :- var(V), !, fail. 942calling_meta_spec(I) :- integer(I), !. 943calling_meta_spec(^). 944calling_meta_spec(//). 945 946 947extend(^, G, Plain) :- 948 !, 949 strip_existential(G, Plain). 950extend(//, DCG, Goal) :- 951 !, 952 ( expand_phrase(call_dcg(DCG,_,_), Goal) 953 -> true 954 ; instantiation_error(DCG) % Ask more instantiation. 955 ). % might not help, but does not harm. 956extend(0, G, G) :- !. 957extend(I, M:G0, M:G) :- 958 !, 959 G0 =.. List, 960 length(Extra, I), 961 append(List, Extra, All), 962 G =.. All. 963extend(I, G0, G) :- 964 G0 =.. List, 965 length(Extra, I), 966 append(List, Extra, All), 967 G =.. All. 968 969strip_existential(Var, Var) :- 970 var(Var), 971 !. 972strip_existential(M:G0, M:G) :- 973 !, 974 strip_existential(G0, G). 975strip_existential(_^G0, G) :- 976 !, 977 strip_existential(G0, G). 978strip_existential(G, G).
982safe_meta((0,0)). 983safe_meta((0;0)). 984safe_meta((0->0)). 985safe_meta(system:(0*->0)). 986safe_meta(catch(0,*,0)). 987safe_meta(findall(*,0,*)). 988safe_meta('$bags':findall(*,0,*,*)). 989safe_meta(setof(*,^,*)). 990safe_meta(bagof(*,^,*)). 991safe_meta('$bags':findnsols(*,*,0,*)). 992safe_meta('$bags':findnsols(*,*,0,*,*)). 993safe_meta(system:call_cleanup(0,0)). 994safe_meta(system:setup_call_cleanup(0,0,0)). 995safe_meta(system:setup_call_catcher_cleanup(0,0,*,0)). 996safe_meta('$attvar':call_residue_vars(0,*)). 997safe_meta('$syspreds':call_with_inference_limit(0,*,*)). 998safe_meta('$syspreds':call_with_depth_limit(0,*,*)). 999safe_meta(^(*,0)). 1000safe_meta(\+(0)). 1001safe_meta(call(0)). 1002safe_meta(call(1,*)). 1003safe_meta(call(2,*,*)). 1004safe_meta(call(3,*,*,*)). 1005safe_meta(call(4,*,*,*,*)). 1006safe_meta(call(5,*,*,*,*,*)). 1007safe_meta(call(6,*,*,*,*,*,*)). 1008safe_meta('$tabling':start_tabling(*,0)). 1009safe_meta('$tabling':start_tabling(*,0,*,*)).
1016safe_output(Output) :- 1017 var(Output), 1018 !, 1019 instantiation_error(Output). 1020safe_output(atom(_)). 1021safe_output(string(_)). 1022safe_output(codes(_)). 1023safe_output(codes(_,_)). 1024safe_output(chars(_)). 1025safe_output(chars(_,_)). 1026safe_output(current_output). 1027safe_output(current_error).
1033:- public format_calls/3. % used in pengines_io 1034 1035format_calls(Format, _Args, _Calls) :- 1036 var(Format), 1037 !, 1038 instantiation_error(Format). 1039format_calls(Format, Args, Calls) :- 1040 format_types(Format, Types), 1041 ( format_callables(Types, Args, Calls) 1042 -> true 1043 ; throw(error(format_error(Format, Types, Args), _)) 1044 ). 1045 1046format_callables([], [], []). 1047format_callables([callable|TT], [G|TA], [G|TG]) :- 1048 !, 1049 format_callables(TT, TA, TG). 1050format_callables([_|TT], [_|TA], TG) :- 1051 !, 1052 format_callables(TT, TA, TG). 1053 1054 1055 /******************************* 1056 * SAFE COMPILATION HOOKS * 1057 *******************************/ 1058 1059:- multifile 1060 prolog:sandbox_allowed_directive/1, 1061 prolog:sandbox_allowed_goal/1, 1062 prolog:sandbox_allowed_expansion/1.
1068prologsandbox_allowed_directive(Directive) :- 1069 debug(sandbox(directive), 'Directive: ~p', [Directive]), 1070 fail. 1071prologsandbox_allowed_directive(Directive) :- 1072 safe_directive(Directive), 1073 !. 1074prologsandbox_allowed_directive(M:PredAttr) :- 1075 \+ prolog_load_context(module, M), 1076 !, 1077 debug(sandbox(directive), 'Cross-module directive', []), 1078 permission_error(execute, sandboxed_directive, (:- M:PredAttr)). 1079prologsandbox_allowed_directive(M:PredAttr) :- 1080 safe_pattr(PredAttr), 1081 !, 1082 PredAttr =.. [Attr, Preds], 1083 ( safe_pattr(Preds, Attr) 1084 -> true 1085 ; permission_error(execute, sandboxed_directive, (:- M:PredAttr)) 1086 ). 1087prologsandbox_allowed_directive(_:Directive) :- 1088 safe_source_directive(Directive), 1089 !. 1090prologsandbox_allowed_directive(_:Directive) :- 1091 directive_loads_file(Directive, File), 1092 !, 1093 safe_path(File). 1094prologsandbox_allowed_directive(G) :- 1095 safe_goal(G).
Module:Directive
(without :-
wrapper). In almost all
cases, the implementation must verify that the Module is the
current load context as illustrated below. This check is not
performed by the system to allow for cases where particular
cross-module directives are allowed.
sandbox:safe_directive(M:Directive) :- prolog_load_context(module, M), ...
1113safe_pattr(dynamic(_)). 1114safe_pattr(thread_local(_)). 1115safe_pattr(volatile(_)). 1116safe_pattr(discontiguous(_)). 1117safe_pattr(multifile(_)). 1118safe_pattr(public(_)). 1119safe_pattr(meta_predicate(_)). 1120safe_pattr(table(_)). 1121 1122safe_pattr(Var, _) :- 1123 var(Var), 1124 !, 1125 instantiation_error(Var). 1126safe_pattr((A,B), Attr) :- 1127 !, 1128 safe_pattr(A, Attr), 1129 safe_pattr(B, Attr). 1130safe_pattr(M:G, Attr) :- 1131 !, 1132 ( atom(M), 1133 prolog_load_context(module, M) 1134 -> true 1135 ; Goal =.. [Attr,M:G], 1136 permission_error(directive, sandboxed, (:- Goal)) 1137 ). 1138safe_pattr(_, _). 1139 1140safe_source_directive(op(_,_,Name)) :- 1141 !, 1142 ( atom(Name) 1143 -> true 1144 ; is_list(Name), 1145 maplist(atom, Name) 1146 ). 1147safe_source_directive(set_prolog_flag(Flag, Value)) :- 1148 !, 1149 atom(Flag), ground(Value), 1150 safe_directive_flag(Flag, Value). 1151safe_source_directive(style_check(_)). 1152safe_source_directive(initialization(_)). % Checked at runtime 1153safe_source_directive(initialization(_,_)). % Checked at runtime 1154 1155directive_loads_file(use_module(library(X)), X). 1156directive_loads_file(use_module(library(X), _Imports), X). 1157directive_loads_file(ensure_loaded(library(X)), X). 1158directive_loads_file(include(X), X). 1159 1160safe_path(X) :- 1161 var(X), 1162 !, 1163 instantiation_error(X). 1164safe_path(X) :- 1165 ( atom(X) 1166 ; string(X) 1167 ), 1168 !, 1169 \+ sub_atom(X, 0, _, 0, '..'), 1170 \+ sub_atom(X, 0, _, _, '/'), 1171 \+ sub_atom(X, 0, _, _, '../'), 1172 \+ sub_atom(X, _, _, 0, '/..'), 1173 \+ sub_atom(X, _, _, _, '/../'). 1174safe_path(A/B) :- 1175 !, 1176 safe_path(A), 1177 safe_path(B).
1189safe_directive_flag(generate_debug_info, _). 1190safe_directive_flag(var_prefix, _). 1191safe_directive_flag(double_quotes, _). 1192safe_directive_flag(back_quotes, _).
Our assumption is that external expansion rules are coded safely and we only need to be careful if the sandboxed code defines expansion rules.
1207prologsandbox_allowed_expansion(Directive) :- 1208 prolog_load_context(module, M), 1209 debug(sandbox(expansion), 'Expand in ~p: ~p', [M, Directive]), 1210 fail. 1211prologsandbox_allowed_expansion(M:G) :- 1212 prolog_load_context(module, M), 1213 !, 1214 safe_goal(M:G). 1215prologsandbox_allowed_expansion(_,_).
1221prologsandbox_allowed_goal(G) :- 1222 safe_goal(G). 1223 1224 1225 /******************************* 1226 * MESSAGES * 1227 *******************************/ 1228 1229:- multifile 1230 prolog:message//1, 1231 prolog:message_context//1, 1232 prolog:error_message//1. 1233 1234prologmessage(error(instantiation_error, Context)) --> 1235 { nonvar(Context), 1236 Context = sandbox(_Goal,Parents), 1237 numbervars(Context, 1, _) 1238 }, 1239 [ 'Sandbox restriction!'-[], nl, 1240 'Could not derive which predicate may be called from'-[] 1241 ], 1242 ( { Parents == [] } 1243 -> [ 'Search space too large'-[] ] 1244 ; callers(Parents, 10) 1245 ). 1246 1247prologmessage_context(sandbox(_G, [])) --> !. 1248prologmessage_context(sandbox(_G, Parents)) --> 1249 [ nl, 'Reachable from:'-[] ], 1250 callers(Parents, 10). 1251 1252callers([], _) --> !. 1253callers(_, 0) --> !. 1254callers([G|Parents], Level) --> 1255 { NextLevel is Level-1 1256 }, 1257 [ nl, '\t ~p'-[G] ], 1258 callers(Parents, NextLevel). 1259 1260prologmessage(bad_safe_declaration(Goal, File, Line)) --> 1261 [ '~w:~d: Invalid safe_primitive/1 declaration: ~p'- 1262 [File, Line, Goal] ]. 1263 1264prologerror_message(format_error(Format, Types, Args)) --> 1265 format_error(Format, Types, Args). 1266 1267format_error(Format, Types, Args) --> 1268 { length(Types, TypeLen), 1269 length(Args, ArgsLen), 1270 ( TypeLen > ArgsLen 1271 -> Problem = 'not enough' 1272 ; Problem = 'too many' 1273 ) 1274 }, 1275 [ 'format(~q): ~w arguments (found ~w, need ~w)'- 1276 [Format, Problem, ArgsLen, TypeLen] 1277 ]
Sandboxed Prolog code
Prolog is a full-featured Turing complete programming language in which it is easy to write programs that can harm your computer. On the other hand, Prolog is a logic based query language which can be exploited to query data interactively from, e.g., the web. This library provides safe_goal/1, which determines whether it is safe to call its argument.