1:- module(hornguard, 2 [ hornguard_admit/4, % +Backend, +Profiles, +Goal, -Verdict 3 hornguard_admit/5, % +Backend, +Profiles, +Goal, +Options, -Verdict 4 hornguard_admit_clause/4, % +Backend, +Profiles, +Clause, -Verdict 5 hornguard_admit_clause/5, % +Backend, +Profiles, +Clause, +Options, -Verdict 6 hornguard_admit_program/4, % +Backend, +Profiles, +Clauses, -Verdict 7 hornguard_admit_program/5, % +Backend, +Profiles, +Clauses, +Options, -Verdict 8 hornguard_stratification/2, % +Clauses, -Result 9 hornguard_floundering/2, % +ClauseOrGoal, -NegatedGoals 10 hornguard_rewrite/3, % +Backend, +Term, -Guarded 11 hornguard_call/1, % :Goal judged at the moment it runs 12 hornguard_call/2, 13 hornguard_call/3, 14 hornguard_call/4, 15 hornguard_call/5, 16 hornguard_call/6, 17 hornguard_call/7, 18 hornguard_call/8, 19 hornguard_catch/3, % :Goal, ?Catcher, :Recovery 20 hornguard_set_runtime_context/1, % +Options 21 hornguard_run/4, % +Backend, +Profiles, +Caps, +Goal 22 hornguard_load_profiles/1, % +Dir 23 hornguard_load_policy/1, % +File 24 hornguard_policy/1, % -Policy 25 hornguard_ops/1, % -Ops 26 hornguard_admit/2, % +Goal, -Verdict (under the loaded policy) 27 hornguard_admit_clause/2, % +Clause, -Verdict 28 hornguard_admit_program/2, % +Clauses, -Verdict 29 hornguard_profiles/1 % -Names 30 ]). 31 32:- meta_predicate 33 hornguard_call(0), 34 hornguard_call(1, ?), 35 hornguard_call(2, ?, ?), 36 hornguard_call(3, ?, ?, ?), 37 hornguard_call(4, ?, ?, ?, ?), 38 hornguard_call(5, ?, ?, ?, ?, ?), 39 hornguard_call(6, ?, ?, ?, ?, ?, ?), 40 hornguard_call(7, ?, ?, ?, ?, ?, ?, ?), 41 hornguard_catch(0, ?, 0).

Hornguard: default-deny firewall for untrusted Prolog

The judge. Pure: it never executes the term it is given. It walks a goal or a clause, consults the loaded profiles (allow/2, meta_spec/2) and the pinned class table (pinned/2), and returns a verdict:

admit
admit_with(Guarded) - under dynamic_dispatch(judged): admissible as Guarded, the term with every unbound goal or closure rewritten to a call the judge sees again at the moment it runs. Run Guarded, never the original.
admit_needs(Needs) - admissible once the host satisfies each need: profile(Name) for a known profile not in force, predicate(Indicator) for a sandboxed predicate not yet stored (only under defer_unknown(true))
refused(Reason, Class, Rule) Reason: an ISO error term the host may show the author, subject to its oracle policy Class: benign_miss | capability_probe | escape_attempt | reconnaissance | shadowing | semantics | evasion shadowing is the head family: a clause that would stand in for a definition the judge reasons about. Its body is walked like any other; the harm is to what the host's predicate answers, not to what a call can do, and in practice it is the class a policy gap shows up as (see tools/triage.pl). Rule: pinned(Class) | unbound_goal | qualified | meta_spec(Indicator) | unknown | not_callable | head(Why) | directive | unsupported(What) | evaluable(Name/Arity) | unstratified(Members, Head-Callee) | floundering(NegatedGoal) | cyclic_term | term_depth A pinned rule nested inside a meta-argument carries + depth(N). head(Why) is one of control, pinned(Class), profile(Name), trusted, qualified.

The semantics class is not a threat signal. It marks a program the judge can admit capability-wise but refuses to store because it has no single intended meaning: recursion through negation or aggregation (hornguard_stratification/2), and negation used as if it bound a variable (hornguard_floundering/2). The latter is refused only under strict_negation(true), the default; a host that passes strict_negation(false) may still call hornguard_floundering/2 itself and warn.

Structural rules, in the order the walk applies them:

An unbound goal in call position is refused. Always. This closes construct-then-call at the sink.
Module-qualified goals are refused; the sandbox has one module.
The control constructs (,)/2 (;)/2 (->)/2 (*->)/2 and (^)/2 are walked through without counting depth.
A predicate in a pinned class is refused before any profile is consulted.
A predicate the host declared trust(Indicator, Spec) is admitted with its declared meta spec applied and its body not walked.
A predicate allowed by a profile in force has each goal argument judged one level deeper; closures are completed to full arity with fresh variables first. On backends with introspection, an allowed predicate that the engine declares meta but no profile gives a spec for is refused (fail closed).
A predicate allowed only by a profile not in force is recorded as a need; under defer_unknown(true) so is a predicate the engine does not define.
Anything else is refused as unknown, with an existence or permission reason depending on what the backend can tell.

Two more rules apply where the walk would otherwise not look. An arithmetic predicate's expressions are checked for pinned evaluables (the clock-reading functions), since arithmetic is a second language inside the first. And a clause head may not name a predicate the host trusts: the trusted definition is the one whose body is never walked, and a clause in sandboxed space would stand in for it.

Rule 1 has one sanctioned relaxation. Under dynamic_dispatch(judged) an unbound goal or closure is not refused but rewritten to hornguard_call/N, which judges the goal under the same policy at the moment it runs and only then calls it, and catch/3 becomes hornguard_catch/3, which cannot swallow a runtime refusal. The verdict is then admit_with(Guarded), and the host runs Guarded. Judgment happens twice, statically where the goal is known and at the sink where it is not; nothing runs unjudged either way. The runtime judge is the loaded policy plus whatever hornguard_set_runtime_context/1 has set (a namespace's stored predicates, typically), or a host's own runtime_judge_hook/2 when it wants the judging done in a process the author cannot reach.

Enforcement (hornguard_run/4) is not yet implemented; it belongs to the backend layer, not the judge.

131:- use_module(library(lists)). 132:- use_module(library(apply)). 133:- use_module(library(error)). 134:- use_module(library(ugraphs)). 135 136:- dynamic hg_allow/2, % Profile, Name/Arity 137 hg_meta/2, % Profile, Spec (meta_predicate notation) 138 hg_pinned/2, % Class, Name/Arity (Arity may be unbound) 139 hg_pinned_evaluable/2, % Class, Name/Arity of an arithmetic function 140 hg_unpinned/2, % Class, Name/Arity (moved aside by a policy unpin) 141 hg_engine/2, % Backend, Name/Arity (what the engine defines) 142 hg_enforcement/2, % Backend, native | external | none 143 hg_policy/1, % policy(Backend, Profiles, Options, Allow, Trust) 144 hg_op/3, % Priority, Type, Name: operators the reader honours 145 hg_loaded_dir/1, 146 hg_default_dir/1. 147 148% hornguard:runtime_judge_hook(+Goal, -Verdict) 149% 150% A host that wants hornguard_call/N judged somewhere the author's code 151% cannot reach (its judge worker, say) defines this. Verdict is any 152% verdict hornguard_admit/5 returns under dynamic_dispatch(judged). 153% Dynamic as well as multifile so a host can install it at run time. 154:- multifile runtime_judge_hook/2. 155:- dynamic runtime_judge_hook/2. 156 157:- prolog_load_context(directory, Dir), 158 atomic_list_concat([Dir, '/../profiles'], Rel), 159 absolute_file_name(Rel, Abs), 160 retractall(hg_default_dir(_)), 161 assertz(hg_default_dir(Abs)). 162 163 164 /******************************* 165 * PROFILES * 166 *******************************/

187hornguard_load_profiles(DirOrDirs) :- 188 ( is_list(DirOrDirs) -> Dirs = DirOrDirs ; Dirs = [DirOrDirs] ), 189 must_be(list(atom), Dirs), 190 foldl(hg_collect_profile_dir, Dirs, [], Facts0), 191 reverse(Facts0, Facts), 192 hg_check_profile_pins(Facts), 193 retractall(hg_allow(_, _)), 194 retractall(hg_meta(_, _)), 195 retractall(hg_pinned(_, _)), 196 retractall(hg_pinned_evaluable(_, _)), 197 retractall(hg_unpinned(_, _)), 198 retractall(hg_engine(_, _)), 199 retractall(hg_enforcement(_, _)), 200 retractall(hg_op(_, _, _)), 201 retractall(hg_loaded_dir(_)), 202 forall(member(Fact, Facts), assertz(Fact)), 203 assertz(hg_loaded_dir(Dirs)).

213hornguard_ops(Ops) :- 214 hg_ensure_profiles, 215 findall(op(P, T, N), hg_op(P, T, N), Ops). 216 217hg_collect_profile_dir(Dir, Acc0, Acc) :- 218 directory_files(Dir, Entries), 219 include(hg_profile_file, Entries, Files0), 220 msort(Files0, Files), 221 foldl(hg_collect_profile_file(Dir), Files, Acc0, Acc). 222 223hg_profile_file(F) :- 224 file_name_extension(_, pl, F). 225 226hg_collect_profile_file(Dir, F, Acc0, Acc) :- 227 directory_file_path(Dir, F, Path), 228 setup_call_cleanup( 229 open(Path, read, In), 230 hg_collect_profile_terms(In, Path, Acc0, Acc), 231 close(In)). 232 233hg_collect_profile_terms(In, Path, Acc0, Acc) :- 234 read_term(In, Term, [module(hornguard)]), 235 ( Term == end_of_file 236 -> Acc = Acc0 237 ; hg_profile_fact(Term, Path, Acc0, Acc1), 238 hg_collect_profile_terms(In, Path, Acc1, Acc) 239 ). 240 241% The fact a profile term becomes, consed onto the accumulator; the list 242% is reversed once before it is asserted so file order is kept. 243hg_profile_fact(allow(P, N/A), _, Acc, [hg_allow(P, N/A)|Acc]) :- 244 atom(P), atom(N), integer(A), !. 245hg_profile_fact(meta_spec(P, Spec), _, Acc, [hg_meta(P, Spec)|Acc]) :- 246 atom(P), callable(Spec), !. 247hg_profile_fact(pinned(C, N/A), _, Acc, [hg_pinned(C, N/A)|Acc]) :- 248 atom(C), atom(N), ( var(A) ; integer(A) ), !. 249hg_profile_fact(pinned_evaluable(C, N/A), _, Acc, [hg_pinned_evaluable(C, N/A)|Acc]) :- 250 atom(C), atom(N), integer(A), !. 251hg_profile_fact(engine(B, N/A), _, Acc, [hg_engine(B, N/A)|Acc]) :- 252 atom(B), atom(N), integer(A), !. 253hg_profile_fact(enforcement(B, Kind), _, Acc, [hg_enforcement(B, Kind)|Acc]) :- 254 atom(B), hg_enforcement_kind(Kind), !. 255hg_profile_fact(op(P, T, N), _, Acc, [hg_op(P, T, N)|Acc]) :- 256 integer(P), P >= 0, P =< 1200, atom(T), atom(N), !. 257hg_profile_fact((:- _), _, Acc, Acc) :- !. 258hg_profile_fact(Term, Path, _, _) :- 259 throw(error(domain_error(hornguard_profile_term, Term), context(Path, _))). 260 261% What a backend can do about a running goal. 262% 263% native the engine gives the judge's host time, inference and stack 264% caps, isolation, and an abort the author cannot catch 265% external the host must supply them from outside the engine (a process 266% wrapper, a runtime), and must say so before running anything 267% none judge-only; the backend refuses to run 268hg_enforcement_kind(native). 269hg_enforcement_kind(external). 270hg_enforcement_kind(none). 271 272hg_check_profile_pins(Facts) :- 273 forall(member(hg_allow(P, N/A), Facts), 274 ( member(hg_pinned(C, N/A), Facts) 275 -> throw(error(permission_error(allow, pinned(C), N/A), 276 context(profile(P), 'pinned classes are not reopened by profile'))) 277 ; true 278 )). 279 280hg_ensure_profiles :- 281 ( hg_loaded_dir(_) 282 -> true 283 ; hg_default_dir(Dir), 284 hornguard_load_profiles(Dir) 285 ).

291hornguard_profiles(Names) :- 292 hg_ensure_profiles, 293 setof(P, I^hg_allow(P, I), Names). 294 295 /******************************* 296 * POLICY * 297 *******************************/

327hornguard_load_policy(File) :- 328 hg_ensure_profiles, 329 must_be(atom, File), 330 setup_call_cleanup(open(File, read, In), 331 hg_read_policy_terms(In, File, [], Terms0), 332 close(In)), 333 reverse(Terms0, Terms), 334 hg_install_policy(Terms, File). 335 336hg_read_policy_terms(In, File, Acc, Terms) :- 337 read_term(In, T, [module(hornguard)]), 338 ( T == end_of_file 339 -> Terms = Acc 340 ; hg_read_policy_terms(In, File, [T|Acc], Terms) 341 ). 342 343% The whole file is validated before anything changes, so a file that 344% fails to load leaves the policy and the pins exactly as they were. The 345% unpins it asks for are known while the allows are checked, since an 346% allow of a class the same file reopens is what the file means. 347hg_install_policy(Terms, File) :- 348 foldl(hg_policy_term(File), Terms, pol(iso, [iso], [], [], []), pol(B, Ps, Os, Al, Tr)), 349 findall(C, member(unpin(C), Terms), Unpins0), 350 sort(Unpins0, Unpins), 351 forall(member(C, Unpins), hg_check_unpin_class(C, File)), 352 hg_check_host_allows(Al, Unpins, File), 353 ( memberchk(author_defines(Aus), Os) -> hg_check_author_defines(Aus, Unpins, File) ; true ), 354 hg_repin_all, 355 forall(member(C, Unpins), hg_unpin(C, File)), 356 retractall(hg_policy(_)), 357 assertz(hg_policy(policy(B, Ps, Os, Al, Tr))). 358 359hg_check_unpin_class(Class, File) :- 360 ( atom(Class), ( hg_pinned(Class, _) ; hg_unpinned(Class, _) ) 361 -> true 362 ; throw(error(domain_error(hornguard_pinned_class, Class), context(File, _))) 363 ). 364 365hg_policy_term(_, unpin(_), P, P) :- !. 366hg_policy_term(_, (:- _), P, P) :- !. 367hg_policy_term(File, backend(B), pol(_, Ps, Os, Al, Tr), pol(B, Ps, Os, Al, Tr)) :- !, 368 hg_policy_check(atom(B), File, backend(B)). 369hg_policy_term(File, profiles(Ps), pol(B, _, Os, Al, Tr), pol(B, Ps, Os, Al, Tr)) :- !, 370 hg_policy_check(is_list(Ps), File, profiles(Ps)), 371 forall(member(P, Ps), 372 hg_policy_check(hg_allow(P, _), File, unknown_profile(P))). 373hg_policy_term(File, option(O), pol(B, Ps, Os, Al, Tr), pol(B, Ps, [O|Os], Al, Tr)) :- !, 374 hg_policy_check(hg_policy_option(O), File, option(O)). 375hg_policy_term(File, allow(Ind), pol(B, Ps, Os, Al, Tr), pol(B, Ps, Os, [Ind|Al], Tr)) :- !, 376 hg_policy_check(hg_indicator_term(Ind), File, allow(Ind)). 377hg_policy_term(File, trust(Ind, Spec), pol(B, Ps, Os, Al, Tr), pol(B, Ps, Os, Al, [Ind-Spec|Tr])) :- !, 378 hg_policy_check(hg_indicator_term(Ind), File, trust(Ind, Spec)), 379 hg_policy_check(hg_trust_spec_ok(Ind, Spec), File, trust_spec(Ind, Spec)). 380% author_defines/1 terms accumulate into one author_defines(List) option, 381% so the judge and every host that forwards policy options see one term. 382hg_policy_term(File, author_defines(Ind), pol(B, Ps, Os0, Al, Tr), pol(B, Ps, Os, Al, Tr)) :- !, 383 hg_policy_check(hg_indicator_term(Ind), File, author_defines(Ind)), 384 ( selectchk(author_defines(L0), Os0, Os1) -> true ; L0 = [], Os1 = Os0 ), 385 Os = [author_defines([Ind|L0])|Os1]. 386hg_policy_term(File, Term, _, _) :- 387 throw(error(domain_error(hornguard_policy_term, Term), context(File, _))). 388 389hg_policy_check(Goal, _, _) :- call(Goal), !. 390hg_policy_check(_, File, What) :- 391 throw(error(domain_error(hornguard_policy, What), context(File, _))). 392 393hg_policy_option(strict_negation(B)) :- hg_bool(B). 394hg_policy_option(defer_unknown(B)) :- hg_bool(B). 395hg_policy_option(author_defines(L)) :- is_list(L), maplist(hg_indicator_term, L). 396 397hg_bool(true). 398hg_bool(false). 399 400hg_indicator_term(N/A) :- atom(N), integer(A), A >= 0. 401 402hg_trust_spec_ok(_, none) :- !. 403hg_trust_spec_ok(N/A, Spec) :- callable(Spec), functor(Spec, N, A). 404 405hg_check_author_defines(Inds, Unpins, File) :- 406 forall(member(Ind, Inds), 407 ( ( hg_pinned(C, Ind) ; hg_unpinned(C, Ind) ), 408 \+ memberchk(C, Unpins) 409 -> throw(error(permission_error(author_defines, pinned(C), Ind), 410 context(File, 'an author may not define a pinned predicate'))) 411 ; hg_control_indicator(Ind) 412 -> throw(error(permission_error(author_defines, control, Ind), context(File, _))) 413 ; true 414 )). 415 416hg_check_host_allows(Allows, Unpins, File) :- 417 forall(member(Ind, Allows), 418 ( ( hg_pinned(C, Ind) ; hg_unpinned(C, Ind) ), 419 \+ memberchk(C, Unpins) 420 -> throw(error(permission_error(allow, pinned(C), Ind), 421 context(File, 'pinned classes are reopened with unpin/1, never by allow/1'))) 422 ; true 423 )). 424 425% Unpinning moves the class's entries aside so they can be restored when 426% the next policy loads. It is always reported. 427hg_unpin(Class, File) :- 428 must_be(atom, Class), 429 findall(Ind, hg_pinned(Class, Ind), Inds), 430 ( Inds == [] 431 -> throw(error(domain_error(hornguard_pinned_class, Class), context(File, _))) 432 ; forall(member(Ind, Inds), 433 ( retract(hg_pinned(Class, Ind)), 434 assertz(hg_unpinned(Class, Ind)) )), 435 length(Inds, N), 436 print_message(warning, hornguard(unpinned(Class, N, File))) 437 ). 438 439hg_repin_all :- 440 forall(retract(hg_unpinned(Class, Ind)), assertz(hg_pinned(Class, Ind))). 441 442:- multifile prolog:message//1. 443prolog:message(hornguard(unpinned(Class, N, File))) --> 444 [ 'hornguard: policy ~w reopens pinned class ~w (~d indicators). '-[File, Class, N], 445 'Every goal in that class is now admissible to authors.' ].

463hornguard_admit(Goal, Verdict) :- 464 hg_policy_call(hornguard_admit, Goal, Verdict). 465hornguard_admit_clause(Clause, Verdict) :- 466 hg_policy_call(hornguard_admit_clause, Clause, Verdict). 467hornguard_admit_program(Clauses, Verdict) :- 468 hg_policy_call(hornguard_admit_program, Clauses, Verdict). 469 470hg_policy_call(Pred, Term, Verdict) :- 471 hornguard_policy(policy(B, Ps, Os, Al, Tr)), 472 Options = [allow(Al), trust(Tr)|Os], 473 call(Pred, B, Ps, Term, Options, Verdict). 474 475 476 /******************************* 477 * JUDGE * 478 *******************************/

501hornguard_admit(Backend, Profiles, Goal, Verdict) :- 502 hornguard_admit(Backend, Profiles, Goal, [], Verdict). 503 504hornguard_admit(Backend, Profiles0, Goal0, Options, Verdict) :- 505 hg_ensure_profiles, 506 hg_dynamic_mode(Options, Mode, Profiles0, Profiles), 507 hg_context(Backend, Profiles, Options, Ctx), 508 hg_strict_negation(Options, Strict), 509 hg_prepared(Mode, goal, Goal0, Ctx, Goal1, Verdict0), 510 ( nonvar(Verdict0) 511 -> Verdict = Verdict0 512 ; hg_judged(Goal1, Goal, 513 ( hg_goal(Goal, 0, Ctx, [], Needs0), 514 hg_check_floundering(Strict, Goal), 515 hg_needs_verdict(Needs0, Verdict1) ), 516 Verdict1), 517 hg_mode_verdict(Mode, Verdict1, Goal1, Verdict) 518 ). 519 520% hg_prepared(+Mode, +Kind, +Term0, +Ctx, -Term, -Verdict) 521% 522% Under judged mode, Term is Term0 with its unbound sinks rewritten; the 523% rewrite shares Term0's variables, so a host's variable names still map. 524% The shapes that would defeat the rewrite (a cyclic term, a term too deep 525% to walk) are refused here, as the judge would refuse them. 526hg_prepared(refused, _, Term, _, Term, _) :- !. 527hg_prepared(judged, Kind, Term0, Ctx, Term, Verdict) :- 528 ( \+ acyclic_term(Term0) 529 -> Term = Term0, 530 Verdict = refused(type_error(acyclic_term, cyclic), evasion, cyclic_term) 531 ; catch(hg_guard_kind(Kind, Term0, Ctx, Term), 532 error(resource_error(What), _), 533 ( Term = Term0, 534 Verdict = refused(resource_error(What), evasion, term_depth) )) 535 ). 536 537hg_guard_kind(goal, Goal, Ctx, Guarded) :- 538 hg_guard_goal(Goal, Ctx, Guarded). 539hg_guard_kind(clause, Clause, Ctx, Guarded) :- 540 hg_guard_clause(Clause, Ctx, Guarded). 541hg_guard_kind(program, Clauses, Ctx, Guarded) :- 542 ( is_list(Clauses) 543 -> maplist([C, G]>>hg_guard_clause(C, Ctx, G), Clauses, Guarded) 544 ; Guarded = Clauses 545 ). 546 547hg_guard_clause((Head :- Body), Ctx, (Head :- Guarded)) :- !, 548 hg_guard_goal(Body, Ctx, Guarded). 549hg_guard_clause(Clause, _, Clause). 550 551% hg_judged(+Term0, -Term, :Judgment, -Verdict) 552% 553% Run Judgment over a private copy of Term0 and turn every way it can 554% stop into a verdict. Attributes are stripped from the copy so no 555% coroutine attached to the caller's term can fire inside the judge. A 556% cyclic term is refused before the walk, because the walk would not 557% terminate on it. A walk that exhausts a stack on a pathologically deep 558% term is refused rather than surfaced as an engine error, so the judge 559% never dies where it was asked to decide. 560hg_judged(Term0, Term, Judgment, Verdict) :- 561 copy_term_nat(Term0, Term), 562 ( acyclic_term(Term) 563 -> catch(Judgment, E, hg_exception_verdict(E, Verdict)) 564 ; Verdict = refused(type_error(acyclic_term, cyclic), evasion, cyclic_term) 565 ). 566 567% Commit to the translation before touching the output argument, so a 568% caller that passes a partially bound Verdict gets failure rather than 569% the internal exception. 570hg_exception_verdict(E, Verdict) :- 571 hg_verdict_of_exception(E, V), !, 572 Verdict = V. 573hg_exception_verdict(E, _) :- 574 throw(E). 575 576hg_verdict_of_exception(hg_refused(Reason, Class, Rule), refused(Reason, Class, Rule)). 577hg_verdict_of_exception(error(resource_error(What), _), 578 refused(resource_error(What), evasion, term_depth)). 579 580hg_strict_negation(Options, Strict) :- 581 ( memberchk(strict_negation(S), Options) 582 -> must_be(boolean, S), Strict = S 583 ; Strict = true 584 ).

596hornguard_admit_clause(Backend, Profiles, Clause, Verdict) :- 597 hornguard_admit_clause(Backend, Profiles, Clause, [], Verdict). 598 599hornguard_admit_clause(Backend, Profiles0, Clause0, Options, Verdict) :- 600 hg_ensure_profiles, 601 hg_dynamic_mode(Options, Mode, Profiles0, Profiles), 602 hg_context(Backend, Profiles, Options, Ctx), 603 hg_strict_negation(Options, Strict), 604 hg_prepared(Mode, clause, Clause0, Ctx, Clause1, Verdict0), 605 ( nonvar(Verdict0) 606 -> Verdict = Verdict0 607 ; hg_judged(Clause1, Clause, 608 ( hg_clause(Clause, Ctx, Needs0), 609 hg_check_floundering(Strict, Clause), 610 hg_needs_verdict(Needs0, Verdict1) ), 611 Verdict1), 612 hg_mode_verdict(Mode, Verdict1, Clause1, Verdict) 613 ). 614 615hg_needs_verdict([], admit) :- !. 616hg_needs_verdict(Needs0, admit_needs(Needs)) :- 617 sort(Needs0, Needs). 618 619hg_context(Backend, Profiles, Options, ctx(Backend, Profiles, Allow, Trust, Defer, Defining, Authors)) :- 620 must_be(atom, Backend), 621 must_be(list(atom), Profiles), 622 must_be(list, Options), 623 ( memberchk(allow(Allow0), Options) -> must_be(list, Allow0), Allow = Allow0 624 ; Allow = [] 625 ), 626 ( memberchk(trust(Trust0), Options) -> must_be(list, Trust0), Trust = Trust0 627 ; Trust = [] 628 ), 629 ( memberchk(defer_unknown(D), Options) -> must_be(boolean, D), Defer = D 630 ; Defer = false 631 ), 632 ( memberchk(defining(Df), Options) -> must_be(list(atom), Df), Defining = Df 633 ; Defining = [] 634 ), 635 ( memberchk(author_defines(Au), Options) -> must_be(list, Au), Authors = Au 636 ; Authors = [] 637 ). 638 639% dynamic_dispatch(refused), the default, is rule 1 as written. Under 640% judged, the term is rewritten before it is judged and the runtime profile 641% joins the profiles in force so the rewritten calls are admissible. 642hg_dynamic_mode(Options, Mode, Profiles0, Profiles) :- 643 ( memberchk(dynamic_dispatch(M), Options) 644 -> must_be(oneof([refused, judged]), M), Mode = M 645 ; Mode = refused 646 ), 647 ( Mode == judged, \+ memberchk(hornguard_runtime, Profiles0) 648 -> Profiles = [hornguard_runtime|Profiles0] 649 ; Profiles = Profiles0 650 ). 651 652% Under judged mode, admission of the guarded term is admission with it. 653hg_mode_verdict(judged, admit, Guarded, admit_with(Guarded)) :- !. 654hg_mode_verdict(_, Verdict, _, Verdict). 655 656% hg_goal(+Goal, +Depth, +Ctx, +Needs0, -Needs) 657% 658% Succeeds if Goal is admissible, accumulating profiles it needs; throws 659% hg_refused/3 at the first refusal. Depth counts meta-argument nesting. 660 661hg_goal(Var, _, _, _, _) :- 662 var(Var), !, 663 throw(hg_refused(instantiation_error, escape_attempt, unbound_goal)). 664hg_goal(_:_, _, _, _, _) :- !, 665 throw(hg_refused(permission_error(execute, goal, (:)/2), escape_attempt, qualified)). 666hg_goal((A, B), D, Ctx, N0, N) :- !, 667 hg_goal(A, D, Ctx, N0, N1), 668 hg_goal(B, D, Ctx, N1, N). 669hg_goal((A ; B), D, Ctx, N0, N) :- !, 670 hg_goal(A, D, Ctx, N0, N1), 671 hg_goal(B, D, Ctx, N1, N). 672hg_goal((A -> B), D, Ctx, N0, N) :- !, 673 hg_goal(A, D, Ctx, N0, N1), 674 hg_goal(B, D, Ctx, N1, N). 675hg_goal((A *-> B), D, Ctx, N0, N) :- !, 676 hg_goal(A, D, Ctx, N0, N1), 677 hg_goal(B, D, Ctx, N1, N). 678hg_goal(_ ^ G, D, Ctx, N0, N) :- !, 679 hg_goal(G, D, Ctx, N0, N). 680hg_goal(true, _, _, N, N) :- !. 681hg_goal(fail, _, _, N, N) :- !. 682hg_goal(false, _, _, N, N) :- !. 683hg_goal(!, _, _, N, N) :- !. 684hg_goal(G, D, Ctx, N0, N) :- 685 callable(G), !, 686 functor(G, Name, Arity), 687 hg_indicator(G, Name/Arity, D, Ctx, N0, N), 688 hg_check_evaluables(G, Name/Arity, D). 689hg_goal(G, _, _, _, _) :- 690 throw(hg_refused(type_error(callable, G), benign_miss, not_callable)). 691 692% Arithmetic is a second language the walk would otherwise not look into. 693% Its functions are pure except the ones that read the clock, which hand 694% an author the timing channel the `timing` pin exists to close, so the 695% expressions of an arithmetic predicate are checked for pinned 696% evaluables (profiles/pinned.pl, `pinned_evaluable/2`). Refused with the 697% same class and depth a pinned goal would carry at that position. 698hg_check_evaluables(G, Ind, D) :- 699 ( hg_arith_indicator(Ind) 700 -> G =.. [_|Args], 701 forall(member(A, Args), hg_check_expr(A, D)) 702 ; true 703 ). 704 705hg_arith_indicator((is)/2). 706hg_arith_indicator((=:=)/2). 707hg_arith_indicator((=\=)/2). 708hg_arith_indicator((<)/2). 709hg_arith_indicator((>)/2). 710hg_arith_indicator((=<)/2). 711hg_arith_indicator((>=)/2). 712 713hg_check_expr(V, _) :- 714 var(V), !. 715hg_check_expr(E, D) :- 716 atom(E), !, 717 hg_check_evaluable(E/0, D). 718hg_check_expr(E, D) :- 719 compound(E), !, 720 functor(E, F, A), 721 hg_check_evaluable(F/A, D), 722 E =.. [_|Args], 723 forall(member(Arg, Args), hg_check_expr(Arg, D)). 724hg_check_expr(_, _). 725 726hg_check_evaluable(Ind, D) :- 727 ( hg_pinned_evaluable(Class, Ind) 728 -> hg_pinned_report_class(Class, D, Report), 729 hg_depth_rule(evaluable(Ind), D, Rule), 730 throw(hg_refused(permission_error(evaluate, evaluable, Ind), Report, Rule)) 731 ; true 732 ). 733 734hg_indicator(G, Ind, D, Ctx, N0, N) :- 735 ( hg_pinned(PinClass, Ind) 736 -> hg_pinned_report_class(PinClass, D, Class), 737 hg_depth_rule(pinned(PinClass), D, Rule), 738 throw(hg_refused(permission_error(execute, goal, Ind), Class, Rule)) 739 ; hg_trusted(Ind, Ctx, Spec) 740 -> hg_apply_spec(Spec, G, D, Ctx, N0, N) 741 ; hg_in_force(Ind, Ctx) 742 -> ( hg_spec_in_force(Ind, Ctx, Spec) 743 -> hg_apply_spec(Spec, G, D, Ctx, N0, N) 744 ; hg_engine_meta_gap(Ctx, G) 745 -> throw(hg_refused(permission_error(execute, goal, Ind), benign_miss, meta_spec(Ind))) 746 ; N = N0 747 ) 748 ; hg_available(Ind, Profile) 749 -> ( hg_spec_in_profile(Ind, Profile, Spec) 750 -> hg_apply_spec(Spec, G, D, Ctx, [profile(Profile)|N0], N) 751 ; N = [profile(Profile)|N0] 752 ) 753 ; hg_deferrable(Ctx, G, Ind) 754 -> N = [predicate(Ind)|N0] 755 ; hg_unknown_reason(Ctx, G, Ind, Reason), 756 throw(hg_refused(Reason, benign_miss, unknown)) 757 ). 758 759% Under defer_unknown(true) an indicator the engine does not define is a 760% sandboxed predicate the host has not stored yet. It is reported as a 761% need rather than refused, so a rule may be stored before the rules it 762% calls. An indicator the engine does define but no profile allows stays 763% a refusal: deferral never widens the engine surface. 764% 765% What the engine defines is hg_engine_defines/3's answer and nothing 766% else's, so deferral and the refusal reason can never disagree about it. 767% Keep it that way: a second predicate answering the same question for 768% swi alone once lived here, and every manifest backend deferred what it 769% should have refused. 770hg_deferrable(Ctx, G, Ind) :- 771 Ctx = ctx(_, _, _, _, true, _, _), 772 \+ hg_engine_defines(Ctx, G, Ind). 773 774% Reflection is reconnaissance wherever it appears. Any other pinned 775% class is a probe at the top level and an escape attempt once it is 776% hidden inside a meta-argument: the author expected the outer goal to 777% pass. 778hg_pinned_report_class(reflection, _, reconnaissance) :- !. 779hg_pinned_report_class(_, 0, capability_probe) :- !. 780hg_pinned_report_class(_, _, escape_attempt). 781 782hg_depth_rule(Rule, 0, Rule) :- !. 783hg_depth_rule(Rule, D, Rule + depth(D)). 784 785hg_trusted(Ind, ctx(_, _, _, Trust, _, _, _), Spec) :- 786 memberchk(Ind-Spec, Trust). 787 788hg_in_force(Ind, ctx(_, Profiles, Allow, _, _, _, _)) :- 789 ( member(P, Profiles), hg_allow(P, Ind) 790 -> true 791 ; memberchk(Ind, Allow) 792 ). 793 794hg_spec_in_force(Name/Arity, ctx(_, Profiles, _, _, _, _, _), Spec) :- 795 functor(Spec, Name, Arity), 796 member(P, Profiles), 797 hg_meta(P, Spec), !. 798 799hg_available(Ind, Profile) :- 800 hg_allow(Profile, Ind), !. 801 802hg_spec_in_profile(Name/Arity, Profile, Spec) :- 803 functor(Spec, Name, Arity), 804 hg_meta(Profile, Spec), !. 805 806% Apply a meta_predicate-style spec to the arguments of G. `0` and `^` 807% arguments are goals; an integer K > 0 is a closure completed with K 808% fresh arguments; anything else is data. 809hg_apply_spec(none, _, _, _, N, N) :- !. 810hg_apply_spec(Spec, G, D, Ctx, N0, N) :- 811 D1 is D + 1, 812 Spec =.. [_|Modes], 813 G =.. [_|Args], 814 hg_apply_modes(Modes, Args, D1, Ctx, N0, N). 815 816hg_apply_modes([], [], _, _, N, N). 817hg_apply_modes([M|Ms], [A|As], D, Ctx, N0, N) :- 818 hg_apply_mode(M, A, D, Ctx, N0, N1), 819 hg_apply_modes(Ms, As, D, Ctx, N1, N). 820 821hg_apply_mode(0, A, D, Ctx, N0, N) :- !, 822 hg_goal(A, D, Ctx, N0, N). 823hg_apply_mode(^, A, D, Ctx, N0, N) :- !, 824 hg_strip_existential(A, G), 825 hg_goal(G, D, Ctx, N0, N). 826hg_apply_mode(K, A, D, Ctx, N0, N) :- 827 integer(K), K > 0, !, 828 hg_complete_closure(A, K, G), 829 hg_goal(G, D, Ctx, N0, N). 830hg_apply_mode(_, _, _, _, N, N). 831 832hg_strip_existential(V, V) :- var(V), !. 833hg_strip_existential(_ ^ G0, G) :- !, hg_strip_existential(G0, G). 834hg_strip_existential(G, G). 835 836% An unbound or qualified closure is left alone so hg_goal refuses it 837% under the right rule; anything else gets K fresh arguments appended. 838hg_complete_closure(V, _, V) :- var(V), !. 839hg_complete_closure(M:C, _, M:C) :- !. 840hg_complete_closure(C, K, G) :- 841 callable(C), !, 842 C =.. L0, 843 length(Fresh, K), 844 append(L0, Fresh, L), 845 G =.. L. 846hg_complete_closure(C, _, C). 847 848 849 /******************************* 850 * CLAUSES * 851 *******************************/ 852 853hg_clause(Var, _, _) :- 854 var(Var), !, 855 throw(hg_refused(instantiation_error, escape_attempt, unbound_clause)). 856hg_clause((:- _), _, _) :- !, 857 throw(hg_refused(permission_error(execute, directive, (:-)/1), capability_probe, directive)). 858hg_clause((?- _), _, _) :- !, 859 throw(hg_refused(permission_error(execute, directive, (?-)/1), capability_probe, directive)). 860hg_clause((_ --> _), _, _) :- !, 861 throw(hg_refused(permission_error(modify, static_procedure, (-->)/2), benign_miss, unsupported(dcg))). 862hg_clause((Head :- Body), Ctx0, Needs) :- !, 863 hg_head(Head, Ctx0), 864 hg_allow_head_in_body(Head, Ctx0, Ctx), 865 hg_goal(Body, 0, Ctx, [], Needs). 866hg_clause(Head, Ctx, []) :- 867 hg_head(Head, Ctx). 868 869% A clause may call its own head: recursion is the normal shape of a rule. 870% Any other sandboxed predicate has to arrive through the allow/1 option, 871% because only the host knows what else is stored. 872hg_allow_head_in_body(Head, ctx(B, P, Allow, Trust, D, Df, Au), ctx(B, P, [Ind|Allow], Trust, D, Df, Au)) :- 873 functor(Head, Name, Arity), 874 Ind = Name/Arity. 875 876% A head may not name anything the judge reasons about: a control 877% construct, a pinned or profile predicate, or a predicate the host 878% trusts. The trusted case is the one that is easy to miss: the host's 879% definition is the one whose body is never walked, so a clause in 880% sandboxed space with that head would stand in for it. 881hg_head(Var, _) :- 882 var(Var), !, 883 throw(hg_refused(instantiation_error, shadowing, unbound_head)). 884hg_head(_:_, _) :- !, 885 throw(hg_refused(permission_error(modify, static_procedure, (:)/2), shadowing, head(qualified))). 886hg_head(Head, Ctx) :- 887 callable(Head), !, 888 functor(Head, Name, Arity), 889 Ind = Name/Arity, 890 ( hg_control_indicator(Ind) 891 -> throw(hg_refused(permission_error(modify, static_procedure, Ind), shadowing, head(control))) 892 ; hg_pinned(Class, Ind) 893 -> throw(hg_refused(permission_error(modify, static_procedure, Ind), shadowing, head(pinned(Class)))) 894 ; hg_author_defines(Ind, Ctx) 895 -> true 896 ; hg_trusted(Ind, Ctx, _) 897 -> throw(hg_refused(permission_error(modify, static_procedure, Ind), shadowing, head(trusted))) 898 ; hg_allow(Profile, Ind), \+ hg_defining(Profile, Ctx) 899 -> throw(hg_refused(permission_error(modify, static_procedure, Ind), shadowing, head(profile(Profile)))) 900 ; true 901 ). 902hg_head(Head, _) :- 903 throw(hg_refused(type_error(callable, Head), benign_miss, not_callable)). 904 905% A host judging the program that *is* a profile (a battery's clauses, 906% installed once as platform code) names that profile in defining/1; its 907% heads are then the definitions the profile promises, not shadows of them. 908hg_defining(Profile, ctx(_, _, _, _, _, Defining, _)) :- 909 memberchk(Profile, Defining). 910 911% A predicate the host provides as a table authors populate: entity and 912% attribute facts in a fact store, say. The host declares it in 913% author_defines/1; an author's clause may then carry that head, and its 914% body is walked like any other. Calls to it are governed by the 915% predicate's own allow or trust declaration, as before. Pinned and 916% control indicators are refused at policy load, never here. 917hg_author_defines(Ind, ctx(_, _, _, _, _, _, Authors)) :- 918 memberchk(Ind, Authors). 919 920hg_control_indicator((',')/2). 921hg_control_indicator((;)/2). 922hg_control_indicator((->)/2). 923hg_control_indicator((*->)/2). 924hg_control_indicator((^)/2). 925hg_control_indicator((:)/2). 926hg_control_indicator(true/0). 927hg_control_indicator(fail/0). 928hg_control_indicator(false/0). 929hg_control_indicator((!)/0). 930 931 932 /******************************* 933 * PROGRAMS * 934 *******************************/

946hornguard_admit_program(Backend, Profiles, Clauses, Verdict) :- 947 hornguard_admit_program(Backend, Profiles, Clauses, [], Verdict). 948 949hornguard_admit_program(Backend, Profiles0, Clauses0, Options, Verdict) :- 950 hg_ensure_profiles, 951 must_be(list, Clauses0), 952 hg_dynamic_mode(Options, Mode, Profiles0, Profiles), 953 hg_context(Backend, Profiles, Options, Ctx0), 954 hg_strict_negation(Options, Strict), 955 hg_prepared(Mode, program, Clauses0, Ctx0, Clauses1, Verdict0), 956 ( nonvar(Verdict0) 957 -> Verdict = Verdict0 958 ; hg_judged(Clauses1, Clauses, 959 ( hg_program_heads(Clauses, Heads), 960 hg_allow_all(Heads, Ctx0, Ctx), 961 foldl(hg_program_clause(Ctx), Clauses, [], Needs0), 962 forall(member(C, Clauses), hg_check_floundering(Strict, C)), 963 hg_check_stratified(Clauses), 964 hg_needs_verdict(Needs0, Verdict1) ), 965 Verdict1), 966 hg_mode_verdict(Mode, Verdict1, Clauses1, Verdict) 967 ). 968 969hg_program_clause(Ctx, Clause, N0, N) :- 970 hg_clause(Clause, Ctx, Needs), 971 append(Needs, N0, N). 972 973hg_program_heads(Clauses, Heads) :- 974 findall(Ind, ( member(C, Clauses), hg_clause_head_indicator(C, Ind) ), Heads0), 975 sort(Heads0, Heads). 976 977hg_clause_head_indicator(C, _) :- var(C), !, fail. 978hg_clause_head_indicator((:- _), _) :- !, fail. 979hg_clause_head_indicator((?- _), _) :- !, fail. 980hg_clause_head_indicator((_ --> _), _) :- !, fail. 981hg_clause_head_indicator((H :- _), Ind) :- !, hg_clause_head_indicator(H, Ind). 982hg_clause_head_indicator(_:_, _) :- !, fail. 983hg_clause_head_indicator(H, Name/Arity) :- 984 callable(H), 985 functor(H, Name, Arity). 986 987hg_allow_all(Inds, ctx(B, P, Allow0, Trust, D, Df, Au), ctx(B, P, Allow, Trust, D, Df, Au)) :- 988 append(Inds, Allow0, Allow). 989 990hg_check_stratified(Clauses) :- 991 hornguard_stratification(Clauses, Result), 992 ( Result = unstratified(Members, Edge) 993 -> throw(hg_refused(domain_error(stratified_program, Members), semantics, 994 unstratified(Members, Edge))) 995 ; true 996 ).

1015hornguard_stratification(Clauses0, Result) :- 1016 hg_ensure_profiles, 1017 must_be(list, Clauses0), 1018 copy_term(Clauses0, Clauses), 1019 hg_program_heads(Clauses, Defined), 1020 findall(E, ( member(C, Clauses), hg_clause_edge(C, Defined, E) ), Edges0), 1021 sort(Edges0, Edges), 1022 % Reachability comes from one transitive closure over the dependency 1023 % graph, polynomial in its size. Enumerating paths with a visited list, 1024 % which this once did, is exponential on a dense graph: eleven mutually 1025 % referencing predicates took seconds and fourteen did not finish, which 1026 % made a small stored program a way to stall the judge. 1027 findall(H-C, member(edge(H, C, _), Edges), Pairs0), 1028 sort(Pairs0, Pairs), 1029 vertices_edges_to_ugraph(Defined, Pairs, Graph), 1030 transitive_closure(Graph, Closure), 1031 ( member(edge(H, C, neg), Edges), 1032 hg_closure_reaches(Closure, C, H) 1033 -> findall(P, ( member(P, Defined), 1034 ( P == H 1035 ; hg_closure_reaches(Closure, H, P), hg_closure_reaches(Closure, P, H) 1036 ) ), Ms0), 1037 sort(Ms0, Members), 1038 Result = unstratified(Members, H-C) 1039 ; hg_strata(Defined, Edges, Strata), 1040 Result = stratified(Strata) 1041 ). 1042 1043% From reaches To by at least one edge. 1044hg_closure_reaches(Closure, From, To) :- 1045 memberchk(From-Successors, Closure), 1046 memberchk(To, Successors). 1047 1048hg_clause_edge((H :- B), Defined, edge(HInd, CInd, Sign)) :- 1049 hg_clause_head_indicator(H, HInd), 1050 hg_body_dep(B, pos, Defined, CInd, Sign). 1051 1052% hg_body_dep(+Body, +Polarity, +Defined, -Callee, -Sign) is nondet. 1053hg_body_dep(V, _, _, _, _) :- var(V), !, fail. 1054hg_body_dep((A, B), S, D, C, Sg) :- !, ( hg_body_dep(A, S, D, C, Sg) ; hg_body_dep(B, S, D, C, Sg) ). 1055hg_body_dep((A ; B), S, D, C, Sg) :- !, ( hg_body_dep(A, S, D, C, Sg) ; hg_body_dep(B, S, D, C, Sg) ). 1056hg_body_dep((A -> B), S, D, C, Sg) :- !, ( hg_body_dep(A, S, D, C, Sg) ; hg_body_dep(B, S, D, C, Sg) ). 1057hg_body_dep((A *-> B), S, D, C, Sg) :- !, ( hg_body_dep(A, S, D, C, Sg) ; hg_body_dep(B, S, D, C, Sg) ). 1058hg_body_dep(_ ^ G, S, D, C, Sg) :- !, hg_body_dep(G, S, D, C, Sg). 1059hg_body_dep(_:_, _, _, _, _) :- !, fail. 1060hg_body_dep(G, _, D, C, Sg) :- 1061 hg_negative_context(G, Inner), !, 1062 hg_body_dep(Inner, neg, D, C, Sg). 1063hg_body_dep(G, S, D, C, Sg) :- 1064 callable(G), 1065 functor(G, Name, Arity), 1066 hg_any_meta_spec(Name/Arity, Spec), !, 1067 ( memberchk(Name/Arity, D), C = Name/Arity, Sg = S 1068 ; Spec =.. [_|Modes], G =.. [_|Args], 1069 nth1(I, Modes, Mode), nth1(I, Args, Arg), 1070 hg_meta_arg_goal(Mode, Arg, Inner), 1071 hg_body_dep(Inner, S, D, C, Sg) 1072 ). 1073hg_body_dep(G, S, D, Name/Arity, S) :- 1074 callable(G), 1075 functor(G, Name, Arity), 1076 memberchk(Name/Arity, D). 1077 1078% Goal arguments whose result depends on the callee being complete. 1079hg_negative_context(\+ G, G). 1080hg_negative_context(not(G), G). 1081hg_negative_context(forall(C, A), (C, A)). 1082hg_negative_context(findall(_, G, _), G). 1083hg_negative_context(findall(_, G, _, _), G). 1084hg_negative_context(bagof(_, G0, _), G) :- hg_strip_existential(G0, G). 1085hg_negative_context(setof(_, G0, _), G) :- hg_strip_existential(G0, G). 1086hg_negative_context(aggregate_all(_, G, _), G). 1087hg_negative_context(aggregate_all(_, _, G, _), G). 1088 1089hg_any_meta_spec(Name/Arity, Spec) :- 1090 functor(Spec, Name, Arity), 1091 hg_meta(_, Spec), !. 1092 1093hg_meta_arg_goal(0, A, A). 1094hg_meta_arg_goal(^, A, G) :- hg_strip_existential(A, G). 1095hg_meta_arg_goal(K, A, G) :- integer(K), K > 0, hg_complete_closure(A, K, G). 1096 1097 /******************************* 1098 * FLOUNDERING * 1099 *******************************/

1115hornguard_floundering(Term0, Goals) :- 1116 copy_term(Term0, Term), 1117 hg_floundering(Term, Goals). 1118 1119hg_floundering((Head :- Body), Goals) :- !, 1120 term_variables(Head, HeadVars), 1121 hg_floundering_body(Body, HeadVars, Goals). 1122hg_floundering(Goal, Goals) :- 1123 hg_floundering_body(Goal, [], Goals). 1124 1125hg_floundering_body(Body, HeadVars, Goals) :- 1126 hg_flatten_body(Body, Entries, []), 1127 hg_flounder_scan(Entries, HeadVars, Goals). 1128 1129% Flatten a body into pos(Goal) and neg(Goal) entries in textual order. 1130hg_flatten_body(V, [pos(V)|T], T) :- var(V), !. 1131hg_flatten_body((A, B), E0, E) :- !, hg_flatten_body(A, E0, E1), hg_flatten_body(B, E1, E). 1132hg_flatten_body((A ; B), E0, E) :- !, hg_flatten_body(A, E0, E1), hg_flatten_body(B, E1, E). 1133hg_flatten_body((A -> B), E0, E) :- !, hg_flatten_body(A, E0, E1), hg_flatten_body(B, E1, E). 1134hg_flatten_body((A *-> B), E0, E) :- !, hg_flatten_body(A, E0, E1), hg_flatten_body(B, E1, E). 1135hg_flatten_body(_ ^ G, E0, E) :- !, hg_flatten_body(G, E0, E). 1136hg_flatten_body(\+ G, [neg(\+ G)|T], T) :- !. 1137hg_flatten_body(not(G), [neg(not(G))|T], T) :- !. 1138hg_flatten_body(G, [pos(G)|T], T). 1139 1140hg_flounder_scan(Entries, HeadVars, Goals) :- 1141 hg_flounder_scan(Entries, HeadVars, [], Goals0), 1142 reverse(Goals0, Goals). 1143 1144hg_flounder_scan([], _, Acc, Acc). 1145hg_flounder_scan([pos(G)|Rest], Bound0, Acc, Goals) :- 1146 hg_binding_vars(G, Vs), 1147 append(Vs, Bound0, Bound), 1148 hg_flounder_scan(Rest, Bound, Acc, Goals). 1149hg_flounder_scan([neg(G)|Rest], Bound, Acc, Goals) :- 1150 term_variables(G, Vs), 1151 hg_later_uses(Rest, Later), 1152 ( member(V, Vs), 1153 \+ hg_var_memberchk(V, Bound), 1154 hg_var_memberchk(V, Later) 1155 -> Acc1 = [G|Acc] 1156 ; Acc1 = Acc 1157 ), 1158 hg_flounder_scan(Rest, Bound, Acc1, Goals). 1159 1160% A later occurrence counts as a use only where the variable is expected 1161% bound: a plain positive goal. Inside a later negation, or inside the 1162% template and goal of an aggregation, the same variable name is a fresh 1163% local scope and an unbound value there is the intended meaning. 1164hg_later_uses(Entries, Uses) :- 1165 foldl(hg_entry_uses, Entries, [], Uses). 1166 1167hg_entry_uses(neg(_), Acc, Acc). 1168hg_entry_uses(pos(G), Acc, Uses) :- 1169 hg_binding_vars(G, Vs), 1170 append(Vs, Acc, Uses). 1171 1172% Which variables a positive goal may leave bound. Aggregation binds its 1173% result only; everything else is assumed to bind all its variables. 1174hg_binding_vars(findall(_, _, L), Vs) :- !, term_variables(L, Vs). 1175hg_binding_vars(findall(_, _, L, T), Vs) :- !, term_variables(L-T, Vs). 1176hg_binding_vars(bagof(_, _, L), Vs) :- !, term_variables(L, Vs). 1177hg_binding_vars(setof(_, _, L), Vs) :- !, term_variables(L, Vs). 1178hg_binding_vars(aggregate_all(_, _, R), Vs) :- !, term_variables(R, Vs). 1179hg_binding_vars(aggregate_all(_, _, _, R), Vs) :- !, term_variables(R, Vs). 1180hg_binding_vars(forall(_, _), []) :- !. 1181hg_binding_vars(G, Vs) :- term_variables(G, Vs). 1182 1183hg_var_memberchk(V, [X|Xs]) :- 1184 ( V == X -> true ; hg_var_memberchk(V, Xs) ). 1185 1186hg_check_floundering(false, _) :- !. 1187hg_check_floundering(true, Term) :- 1188 hg_floundering(Term, Goals), 1189 ( Goals = [G|_] 1190 -> throw(hg_refused(domain_error(safe_negation, G), semantics, floundering(G))) 1191 ; true 1192 ). 1193 1194% stratum(P) = max over dependencies of stratum(Q) for a positive edge and 1195% stratum(Q) + 1 for a negative one. Iterated to a fixpoint; on a 1196% stratified program it converges within |Defined| rounds. 1197hg_strata(Defined, Edges, Strata) :- 1198 findall(P-0, member(P, Defined), S0), 1199 length(Defined, Fuel), 1200 hg_strata_fix(Edges, S0, Fuel, S), 1201 ( S == [] -> Strata = [] 1202 ; findall(L, member(_-L, S), Ls), max_list(Ls, Max), 1203 findall(Layer, ( between(0, Max, I), 1204 findall(P, member(P-I, S), Layer0), msort(Layer0, Layer) ), 1205 Strata) 1206 ). 1207 1208hg_strata_fix(Edges, S0, Fuel, S) :- 1209 foldl(hg_strata_edge, Edges, S0-false, S1-Changed), 1210 ( Changed == true, Fuel > 0 1211 -> Fuel1 is Fuel - 1, 1212 hg_strata_fix(Edges, S1, Fuel1, S) 1213 ; S = S1 1214 ). 1215 1216hg_strata_edge(edge(H, C, Sign), S0-Ch0, S-Ch) :- 1217 memberchk(C-SC, S0), 1218 ( Sign == neg -> Need is SC + 1 ; Need = SC ), 1219 memberchk(H-SH, S0), 1220 ( SH < Need 1221 -> selectchk(H-SH, S0, S1), S = [H-Need|S1], Ch = true 1222 ; S = S0, Ch = Ch0 1223 ). 1224 1225 1226 /******************************* 1227 * BACKENDS * 1228 *******************************/ 1229 1230% What a backend can tell the judge. The `iso` backend knows nothing 1231% about the engine, so an allowed predicate without a spec is trusted to 1232% be first-order and an unknown predicate is an existence error. The 1233% `swi` backend asks the engine. 1234 1235% An allowed predicate the engine declares meta, with no spec from any 1236% profile in force, is refused rather than admitted with its goal arguments 1237% unjudged. Only a backend that can be asked supports this; a manifest 1238% records what exists, not what is meta, so on a manifest-driven backend 1239% the profiles' specs are the whole story and must be complete. 1240hg_engine_meta_gap(ctx(swi, _, _, _, _, _, _), G) :- 1241 catch(predicate_property(G, meta_predicate(Spec)), _, fail), 1242 Spec =.. [_|Modes], 1243 member(Mode, Modes), 1244 hg_goal_mode(Mode), !. 1245 1246hg_goal_mode(0). 1247hg_goal_mode(K) :- integer(K), K > 0. 1248hg_goal_mode(^). 1249hg_goal_mode(//). 1250 1251hg_unknown_reason(Ctx, G, Ind, Reason) :- 1252 hg_engine_defines(Ctx, G, Ind), !, 1253 Reason = permission_error(execute, goal, Ind). 1254hg_unknown_reason(_, _, Ind, existence_error(procedure, Ind)). 1255 1256% Does the backend's engine define this? Asked directly on swi, read from 1257% the backend's manifest otherwise. A backend with no manifest knows 1258% nothing, so everything unrecognised is an existence error and 1259% defer_unknown defers it. 1260hg_engine_defines(ctx(swi, _, _, _, _, _, _), G, _) :- !, 1261 catch(predicate_property(G, defined), _, fail). 1262hg_engine_defines(ctx(Backend, _, _, _, _, _, _), _, Ind) :- 1263 hg_engine(Backend, Ind). 1264 1265 1266 /******************************* 1267 * DYNAMIC DISPATCH, JUDGED * 1268 *******************************/

1280hornguard_rewrite(Backend, Term, Guarded) :- 1281 hg_ensure_profiles, 1282 hornguard_policy(policy(_, _, _, Al, Tr)), 1283 hg_context(Backend, [], [allow(Al), trust(Tr)], Ctx), 1284 hg_guard_goal(Term, Ctx, Guarded). 1285 1286% The rewrite walks the same positions the judge does, using the same 1287% specs, and never binds a variable: the result shares the input's. 1288hg_guard_goal(V, _, hornguard_call(V)) :- 1289 var(V), !. 1290hg_guard_goal(M:G, _, M:G) :- !. 1291hg_guard_goal((A, B), Ctx, (GA, GB)) :- !, 1292 hg_guard_goal(A, Ctx, GA), hg_guard_goal(B, Ctx, GB). 1293hg_guard_goal((A ; B), Ctx, (GA ; GB)) :- !, 1294 hg_guard_goal(A, Ctx, GA), hg_guard_goal(B, Ctx, GB). 1295hg_guard_goal((A -> B), Ctx, (GA -> GB)) :- !, 1296 hg_guard_goal(A, Ctx, GA), hg_guard_goal(B, Ctx, GB). 1297hg_guard_goal((A *-> B), Ctx, (GA *-> GB)) :- !, 1298 hg_guard_goal(A, Ctx, GA), hg_guard_goal(B, Ctx, GB). 1299hg_guard_goal(V ^ G, Ctx, V ^ GG) :- !, 1300 hg_guard_goal(G, Ctx, GG). 1301hg_guard_goal(catch(G, E, R), Ctx, hornguard_catch(GG, E, GR)) :- !, 1302 hg_guard_goal(G, Ctx, GG), 1303 hg_guard_goal(R, Ctx, GR). 1304hg_guard_goal(G, _, Guarded) :- 1305 compound(G), G =.. [call, F|Args], 1306 hg_unbound_closure(F), !, 1307 Guarded =.. [hornguard_call, F|Args]. 1308hg_guard_goal(G, Ctx, Guarded) :- 1309 callable(G), 1310 functor(G, Name, Arity), 1311 hg_guard_spec(Name/Arity, Ctx, Spec), !, 1312 Spec =.. [_|Modes], 1313 G =.. [Name|Args], 1314 maplist(hg_guard_arg(Ctx), Modes, Args, GArgs), 1315 Guarded =.. [Name|GArgs]. 1316hg_guard_goal(G, _, G). 1317 1318% A trust spec from the policy, else any loaded profile's spec. 1319hg_guard_spec(Ind, ctx(_, _, _, Trust, _, _, _), Spec) :- 1320 ( memberchk(Ind-Spec0, Trust), Spec0 \== none 1321 -> Spec = Spec0 1322 ; hg_any_meta_spec(Ind, Spec) 1323 ). 1324 1325hg_guard_arg(Ctx, 0, A, GA) :- !, 1326 hg_guard_goal(A, Ctx, GA). 1327hg_guard_arg(Ctx, ^, A, GA) :- !, 1328 hg_guard_goal(A, Ctx, GA). 1329hg_guard_arg(_, K, A, GA) :- 1330 integer(K), K > 0, !, 1331 hg_guard_closure(A, GA). 1332hg_guard_arg(_, _, A, A). 1333 1334% An unbound closure is completed and judged when it is called; so is 1335% `call` itself as a closure (maplist(call, Goals)), which is the same 1336% thing spelled differently. A bound closure the judge already completed 1337% and judged statically is left as it is. 1338hg_guard_closure(C, hornguard_call(C)) :- 1339 var(C), !. 1340hg_guard_closure(call, hornguard_call) :- !. 1341hg_guard_closure(C, G) :- 1342 compound(C), C =.. [call|Args], !, 1343 G =.. [hornguard_call|Args]. 1344hg_guard_closure(C, C). 1345 1346hg_unbound_closure(F) :- var(F), !. 1347hg_unbound_closure(call) :- !. 1348hg_unbound_closure(F) :- compound(F), functor(F, call, _).

1363hornguard_call(Goal) :- 1364 hg_strip_module(Goal, M, G), 1365 hg_runtime_judge(G, Verdict), 1366 hg_runtime_proceed(Verdict, M, G). 1367 1368hornguard_call(G, A) :- hg_extend_closure(G, [A], G1), hornguard_call(G1). 1369hornguard_call(G, A, B) :- hg_extend_closure(G, [A, B], G1), hornguard_call(G1). 1370hornguard_call(G, A, B, C) :- hg_extend_closure(G, [A, B, C], G1), hornguard_call(G1). 1371hornguard_call(G, A, B, C, D) :- hg_extend_closure(G, [A, B, C, D], G1), hornguard_call(G1). 1372hornguard_call(G, A, B, C, D, E) :- hg_extend_closure(G, [A, B, C, D, E], G1), hornguard_call(G1). 1373hornguard_call(G, A, B, C, D, E, F) :- hg_extend_closure(G, [A, B, C, D, E, F], G1), hornguard_call(G1). 1374hornguard_call(G, A, B, C, D, E, F, H) :- hg_extend_closure(G, [A, B, C, D, E, F, H], G1), hornguard_call(G1). 1375 1376% An unbound goal must stay unbound so the judge refuses it as such; the 1377% `M:G` pattern would otherwise unify with it and never stop stripping. 1378hg_strip_module(V, hornguard, V) :- var(V), !. 1379hg_strip_module(M:G0, M, G) :- !, 1380 hg_strip_inner(G0, G). 1381hg_strip_module(G, hornguard, G). 1382 1383hg_strip_inner(V, V) :- var(V), !. 1384hg_strip_inner(_:G0, G) :- !, hg_strip_inner(G0, G). 1385hg_strip_inner(G, G). 1386 1387% An unbound closure stays unbound: the judge refuses it as such. 1388hg_extend_closure(V, _, V) :- var(V), !. 1389hg_extend_closure(M:C, Extra, M:G) :- !, hg_extend_closure(C, Extra, G). 1390hg_extend_closure(C, Extra, G) :- 1391 callable(C), !, 1392 C =.. L0, append(L0, Extra, L), G =.. L. 1393hg_extend_closure(C, _, C). 1394 1395% A goal still unbound when its sink runs is refused here, not judged: the 1396% judged-mode rewrite would wrap it in another hornguard_call/1 and the 1397% two would hand it back and forth without end. 1398hg_runtime_judge(V, refused(instantiation_error, escape_attempt, unbound_goal)) :- 1399 var(V), !. 1400hg_runtime_judge(G, Verdict) :- 1401 ( catch(runtime_judge_hook(G, V0), _, fail) 1402 -> Verdict = V0 1403 ; hornguard_policy(policy(B, Ps, Os, Al, Tr)), 1404 hg_runtime_options(Ro), 1405 ( memberchk(profiles(Ps1), Ro) -> true ; Ps1 = Ps ), 1406 ( memberchk(allow(Al1), Ro) -> true ; Al1 = Al ), 1407 ( memberchk(trust(Tr1), Ro) -> true ; Tr1 = Tr ), 1408 hornguard_admit(B, Ps1, G, [allow(Al1), trust(Tr1), dynamic_dispatch(judged)|Os], Verdict) 1409 ). 1410 1411hg_runtime_proceed(admit, M, G) :- !, 1412 call(M:G). 1413hg_runtime_proceed(admit_with(Guarded), M, _) :- !, 1414 call(M:Guarded). 1415hg_runtime_proceed(admit_needs(Needs), _, G) :- !, 1416 ( callable(G) -> functor(G, N, A), Ind = N/A ; Ind = G ), 1417 throw(error(permission_error(execute, goal, Ind), hornguard(benign_miss, runtime(needs(Needs))))). 1418hg_runtime_proceed(refused(Reason, Class, Rule), _, _) :- 1419 throw(error(Reason, hornguard(Class, runtime(Rule)))).

1428hornguard_set_runtime_context(Options) :- 1429 must_be(list, Options), 1430 nb_setval('$hornguard_runtime_context', Options). 1431 1432hg_runtime_options(Options) :- 1433 ( nb_current('$hornguard_runtime_context', O), is_list(O) 1434 -> Options = O 1435 ; Options = [] 1436 ).

1445hornguard_catch(Goal, Catcher, Recovery) :- 1446 catch(Goal, Ball, 1447 ( hg_uncatchable(Ball) 1448 -> throw(Ball) 1449 ; Catcher = Ball 1450 -> call(Recovery) 1451 ; throw(Ball) 1452 )). 1453 1454% Guarded on the context being bound: an author's own throw(error(X, _)) 1455% carries an unbound one and must stay catchable. 1456hg_uncatchable(error(_, Ctx)) :- nonvar(Ctx), Ctx = hornguard(_, _). 1457hg_uncatchable(time_limit_exceeded). 1458hg_uncatchable(error(resource_error(_), _)). 1459hg_uncatchable(error(permission_error(execute, _, _), _)). 1460 1461 1462 /******************************* 1463 * NOT YET IMPLEMENTED * 1464 *******************************/

1473hornguard_run(Backend, _Profiles, _Caps, _Goal) :- 1474 hg_ensure_profiles, 1475 must_be(atom, Backend), 1476 ( hg_enforcement(Backend, native) 1477 -> throw(error(not_implemented(hornguard_run/4), _)) 1478 ; hg_enforcement(Backend, external) 1479 -> throw(error(permission_error(run, backend, Backend), 1480 context(hornguard_run/4, 1481 'this backend has no in-engine caps; the host must bound the engine from outside and run the goal itself'))) 1482 ; throw(error(permission_error(run, backend, Backend), 1483 context(hornguard_run/4, 1484 'judge-only backend: it can say whether a goal is admissible, not run it safely'))) 1485 )