1:- module(hornguard_worker, 2 [ hornguard_worker_main/0, 3 apply_ops/0, % give the reader the profiles' operators 4 hornguard_read/4, % +Backend, +Text, -Terms, -Report 5 hornguard_read/5, % +Backend, +Text, -Terms, -VarNames, -Report 6 hornguard_canonical/2, % +Term, -Text 7 hornguard_canonical/3, % +Term, +VarNames, -Text 8 hornguard_judge_text/4 % +Op, +Text, +Options, -Response 9 ]).

Hornguard judge worker

The pack in its own process. A host of any language spawns

swipl prolog/hornguard_worker_main.pl        (or: make worker)

and exchanges one JSON object per line over stdin/stdout. The worker reads author text itself, under the backend's reader flags and with the standard operator table, so the untrusted engine never parses author text: an admitted term comes back in canonical form, and only that form should cross to the engine. Reader-level hazards (syntax errors, quasi-quotations, oversized input, more than one term where one is expected) are refused under the evasion class with a reader(Reason) rule.

Handshake: on start the worker writes

{"hello":"hornguard","protocol":1,"engine":"swi","version":"9.2.9",
 "profiles":[...],"profiles_engine":"9.2.9","engine_matches_profiles":true}

profiles_engine is the engine version the generated swi profile records; an attestation of purity is per engine version, so a host running on another one is told at the handshake.

Requests carry an id (echoed), an op, and op-specific fields:

{"id":1,"op":"judge_goal","text":"findall(X, member(X,[a]), L)",
 "backend":"swi","profiles":["iso","prologue"],
 "options":{"strict_negation":true,"defer_unknown":false,
            "allow":["foo/2"],"trust":[["bar/3","none"]],
            "dynamic_dispatch":"judged","defining":["my_battery"]}}
{"id":2,"op":"judge_clause","text":"p(X) :- q(X)."}
{"id":3,"op":"judge_program","text":"p(1).\np(X) :- q(X)."}
{"id":4,"op":"load_policy","path":"/etc/host/policy.pl"}
{"id":5,"op":"load_profiles","dirs":["/a/profiles","/b/profiles"]}
{"id":6,"op":"profiles"}
{"id":7,"op":"ping"}

backend, profiles and options are optional; absent, the loaded policy applies. Responses:

{"id":1,"verdict":"admit","canonical":"findall(A,member(A,[a]),B)"}
{"id":1,"verdict":"admit_with","canonical":"hornguard_call(G)"}
{"id":1,"verdict":"admit_needs","needs":[{"profile":"swi"}],"canonical":"..."}
{"id":1,"verdict":"refused","class":"escape_attempt","rule":"pinned(process)",
 "depth":1,"reason":"permission_error(execute,goal,shell/1)"}
{"id":4,"ok":true}
{"id":9,"error":"unknown_op","detail":"..."}

The worker is sequential; hosts wanting parallelism run several.

62:- use_module(library(http/json)). 63:- use_module(library(lists)). 64:- use_module(library(apply)). 65:- use_module(library(error)). 66:- use_module(hornguard). 67 68protocol_version(1). 69max_input_bytes(1_000_000). 70 71% This module is also loaded as a library (tests, hosts that judge in 72% process), so it must not start the loop on load. hornguard_worker_main.pl 73% is the script that does. 74 75hornguard_worker_main :- 76 set_stream(user_output, encoding(utf8)), 77 set_stream(user_input, encoding(utf8)), 78 seal_autoloading, 79 apply_ops, 80 hello, 81 loop.

89apply_ops :- 90 catch(hornguard_ops(Ops), _, Ops = []), 91 forall(member(op(P, T, N), Ops), 92 catch(op(P, T, hornguard_worker:N), _, true)). 93 94% On the swi backend the judge asks the engine whether a predicate is 95% defined, and SWI answers that question by autoloading the library that 96% defines it. Left as is, an author's text would decide which libraries the 97% judge's own process loads. Everything autoloadable is loaded once here, 98% before any author text is read, and then autoloading is switched off, so 99% the engine surface the judge reasons about is fixed for the worker's 100% lifetime and nothing an author writes changes the judge's process. 101seal_autoloading :- 102 catch(autoload_all, _, true), 103 set_prolog_flag(autoload, false). 104 105hello :- 106 protocol_version(P), 107 current_prolog_flag(version_data, swi(Ma, Mi, Pa, _)), 108 format(atom(V), "~w.~w.~w", [Ma, Mi, Pa]), 109 catch(hornguard_profiles(Ps), _, Ps = []), 110 profiles_engine(PE), 111 ( PE == V -> Match = true ; Match = false ), 112 reply(_{hello: hornguard, protocol: P, engine: swi, version: V, profiles: Ps, 113 profiles_engine: PE, engine_matches_profiles: Match}). 114 115% The generated swi profile records the engine version it was reviewed 116% against. An attestation of purity is per engine version, so a host 117% running the judge on a different one is trusting attestations made 118% elsewhere; the handshake says so, and the host decides what that means. 119profiles_engine(Version) :- 120 catch(( hornguard:hg_default_dir(Dir), 121 directory_file_path(Dir, 'swi.pl', File), 122 read_file_to_string(File, S, []), 123 sub_string(S, B, _, _, "against SWI-Prolog "), 124 string_length("against SWI-Prolog ", L), 125 Start is B + L, 126 sub_string(S, Start, _, 0, Rest), 127 split_string(Rest, ".\n", "", [Ma, Mi, Pa|_]), 128 atomic_list_concat([Ma, Mi, Pa], '.', Version) ), 129 _, Version = unknown), 130 !. 131profiles_engine(unknown). 132 133loop :- 134 read_line_to_string(user_input, Line), 135 ( Line == end_of_file 136 -> true 137 ; handle_line(Line), 138 loop 139 ). 140 141handle_line(Line) :- 142 ( catch(atom_json_dict(Line, Req, [value_string_as(string)]), _, fail), 143 is_dict(Req) 144 -> catch(handle(Req, Resp), E, error_response(E, Resp)) 145 ; Resp = _{id: null, error: bad_json, detail: "each request is one JSON object per line"} 146 ), 147 reply(Resp). 148 149reply(Dict) :- 150 with_output_to(string(S), json_write_dict(current_output, Dict, [width(0)])), 151 format(user_output, "~s~n", [S]), 152 flush_output(user_output). 153 154error_response(E, _{error: internal, detail: D}) :- 155 catch(message_to_string(E, D), _, term_string(D, E)). 156 157handle(Req, Resp) :- 158 ( get_dict(id, Req, Id) -> true ; Id = null ), 159 ( get_dict(op, Req, Op0), string(Op0) -> atom_string(Op, Op0) 160 ; Op = missing 161 ), 162 dispatch(Op, Req, Resp0), 163 put_dict(id, Resp0, Id, Resp). 164 165dispatch(ping, _, _{ok: true}). 166dispatch(profiles, _, _{ok: true, profiles: Ps}) :- 167 hornguard_profiles(Ps). 168dispatch(load_policy, Req, Resp) :- 169 get_dict(path, Req, P0), string(P0), atom_string(P, P0), 170 catch(( hornguard_load_policy(P), Resp = _{ok: true} ), 171 E, ( message_to_string(E, D), Resp = _{error: policy, detail: D} )). 172dispatch(load_profiles, Req, Resp) :- 173 get_dict(dirs, Req, Ds0), is_list(Ds0), maplist([S, A]>>atom_string(A, S), Ds0, Ds), 174 catch(( hornguard_load_profiles(Ds), apply_ops, Resp = _{ok: true} ), 175 E, ( message_to_string(E, D), Resp = _{error: profiles, detail: D} )). 176dispatch(Op, Req, Resp) :- 177 memberchk(Op, [judge_goal, judge_clause, judge_program]), !, 178 ( get_dict(text, Req, Text), string(Text) 179 -> request_options(Req, Backend, Options), 180 hornguard_judge_text(Op, Text, [backend(Backend)|Options], Resp) 181 ; Resp = _{error: bad_request, detail: "text (string) is required"} 182 ). 183dispatch(Op, _, _{error: unknown_op, detail: D}) :- 184 format(string(D), "unknown op ~w", [Op]). 185 186% Per-request overrides over the loaded policy. 187request_options(Req, Backend, Options) :- 188 hornguard_policy(policy(PB, PPs, POpts, PAllow, PTrust)), 189 ( get_dict(backend, Req, B0), string(B0) -> atom_string(Backend, B0) ; Backend = PB ), 190 ( get_dict(profiles, Req, Ps0), is_list(Ps0) -> maplist([S, A]>>atom_string(A, S), Ps0, Ps) ; Ps = PPs ), 191 ( get_dict(options, Req, O), is_dict(O) -> true ; O = _{} ), 192 ( get_dict(strict_negation, O, SN), hg_bool(SN) -> Opts1 = [strict_negation(SN)] ; opt_from_policy(strict_negation, POpts, Opts1) ), 193 ( get_dict(defer_unknown, O, DU), hg_bool(DU) -> Opts2 = [defer_unknown(DU)] ; opt_from_policy(defer_unknown, POpts, Opts2) ), 194 ( get_dict(allow, O, Al0), is_list(Al0) -> maplist(indicator_from_json, Al0, Al) ; Al = PAllow ), 195 ( get_dict(trust, O, Tr0), is_list(Tr0) -> maplist(trust_from_json, Tr0, Tr) ; Tr = PTrust ), 196 ( get_dict(dynamic_dispatch, O, DD0), string(DD0), atom_string(DD, DD0), memberchk(DD, [refused, judged]) 197 -> Opts3 = [dynamic_dispatch(DD)] 198 ; Opts3 = [] 199 ), 200 ( get_dict(defining, O, Df0), is_list(Df0) 201 -> maplist([S, A]>>atom_string(A, S), Df0, Df), Opts4 = [defining(Df)] 202 ; Opts4 = [] 203 ), 204 opt_from_policy(author_defines, POpts, Opts5), 205 append([[profiles(Ps), allow(Al), trust(Tr)], Opts1, Opts2, Opts3, Opts4, Opts5], Options). 206 207hg_bool(true). hg_bool(false). 208 209opt_from_policy(Name, POpts, [Opt]) :- functor(Opt, Name, 1), memberchk(Opt, POpts), !. 210opt_from_policy(_, _, []). 211 212indicator_from_json(S, N/A) :- 213 string(S), term_string(T, S), T = N/A, atom(N), integer(A), !. 214indicator_from_json(S, _) :- 215 throw(error(domain_error(indicator, S), _)). 216 217trust_from_json([IS, SpecS], Ind-Spec) :- 218 indicator_from_json(IS, Ind), 219 ( SpecS == "none" -> Spec = none ; term_string(Spec, SpecS) ), !. 220trust_from_json(X, _) :- 221 throw(error(domain_error(trust_entry, X), _)). 222 223 224 /******************************* 225 * READ + JUDGE * 226 *******************************/

234hornguard_judge_text(Op, Text, Options, Resp) :- 235 memberchk(backend(Backend), Options), 236 memberchk(profiles(Profiles), Options), 237 exclude([O]>>( O = backend(_) ; O = profiles(_) ), Options, JudgeOpts), 238 terminate_text(Op, Text, Text1), 239 hornguard_read(Backend, Text1, Terms, VarNames, Report), 240 ( Report == ok 241 -> arity_check(Op, Terms, VarNames, Resp0), 242 ( Resp0 = ok(Term, Names) 243 -> judge(Op, Backend, Profiles, Term, JudgeOpts, Verdict), 244 verdict_response(Verdict, Term, Names, Resp) 245 ; Resp = Resp0 246 ) 247 ; Report = refused(Reason), 248 term_string(Reason, RS), 249 Resp = _{verdict: refused, class: evasion, rule: RS, reason: RS} 250 ). 251 252% A single goal or clause is usually sent without its terminating period; 253% supply one. A program is a sequence of terminated clauses and is read 254% as given. 255terminate_text(judge_program, Text, Text) :- !. 256terminate_text(_, Text0, Text) :- 257 normalize_space(string(T), Text0), 258 ( sub_string(T, _, 1, 0, ".") -> Text = T 259 ; string_concat(T, " .", Text) 260 ). 261 262arity_check(judge_program, Terms, Names, ok(Terms, Names)) :- !. 263arity_check(_, [Term], [Names], ok(Term, Names)) :- !. 264arity_check(_, Terms, _, _{verdict: refused, class: evasion, rule: "reader(term_count)", reason: R}) :- 265 length(Terms, N), 266 format(string(R), "expected one term, read ~d", [N]). 267 268judge(judge_goal, B, Ps, T, O, V) :- hornguard_admit(B, Ps, T, O, V). 269judge(judge_clause, B, Ps, T, O, V) :- hornguard_admit_clause(B, Ps, T, O, V). 270judge(judge_program, B, Ps, T, O, V) :- hornguard_admit_program(B, Ps, T, O, V). 271 272verdict_response(admit, Term, Names, _{verdict: admit, canonical: C}) :- 273 canonical_of(Term, Names, C). 274% The guarded term shares the author's variables, so their names still 275% apply; the canonical form is of the guarded term, which is what runs. 276verdict_response(admit_with(Guarded), _, Names, _{verdict: admit_with, canonical: C}) :- 277 canonical_of(Guarded, Names, C). 278verdict_response(admit_needs(Needs), Term, Names, _{verdict: admit_needs, needs: Ns, canonical: C}) :- 279 maplist(need_json, Needs, Ns), 280 canonical_of(Term, Names, C). 281verdict_response(refused(Reason, Class, Rule0), _, _, Resp) :- 282 ( Rule0 = Rule + depth(D) -> true ; Rule = Rule0, D = 0 ), 283 term_string(Reason, RS), term_string(Rule, RuS), 284 Resp = _{verdict: refused, class: Class, rule: RuS, depth: D, reason: RS}. 285 286need_json(profile(P), _{profile: P}). 287need_json(predicate(N/A), _{predicate: S}) :- format(string(S), "~w/~w", [N, A]). 288 289canonical_of(Terms, NamesList, C) :- 290 is_list(Terms), !, 291 maplist(hornguard_canonical, Terms, NamesList, Cs), 292 atomic_list_concat(Cs, '\n', C0), atom_string(C0, C). 293canonical_of(Term, Names, C) :- 294 hornguard_canonical(Term, Names, C). 295 296 297 /******************************* 298 * READER * 299 *******************************/

311hornguard_read(Backend, Text, Terms, Report) :- 312 hornguard_read(Backend, Text, Terms, _, Report). 313 314hornguard_read(Backend, Text, Terms, VarNames, Report) :- 315 string_length(Text, Len), 316 max_input_bytes(Max), 317 ( Len > Max 318 -> Terms = [], VarNames = [], Report = refused(reader(too_large)) 319 ; backend_double_quotes(Backend, DQ), 320 catch(read_all_terms(Text, DQ, Terms, VarNames, Report), 321 E, reader_error(E, Terms, VarNames, Report)) 322 ). 323 324backend_double_quotes(swi, string) :- !. 325backend_double_quotes(scryer, chars) :- !. 326backend_double_quotes(trealla, chars) :- !. 327backend_double_quotes(_, codes). 328 329read_all_terms(Text, DQ, Terms, VarNames, Report) :- 330 setup_call_cleanup( 331 open_string(Text, S), 332 read_terms(S, DQ, Terms, VarNames, Report), 333 close(S)). 334 335read_terms(S, DQ, Terms, VarNames, Report) :- 336 read_term(S, T, [ syntax_errors(error), module(hornguard_worker), 337 double_quotes(DQ), quasi_quotations(QQ0), 338 variable_names(VN) ]), 339 ( var(QQ0) -> QQ = [] ; QQ = QQ0 ), 340 ( T == end_of_file 341 -> Terms = [], VarNames = [], Report = ok 342 ; QQ \== [] 343 -> Terms = [], VarNames = [], Report = refused(reader(quasi_quotation)) 344 ; read_terms(S, DQ, Rest, RestNames, Report0), 345 ( Report0 == ok -> Terms = [T|Rest], VarNames = [VN|RestNames], Report = ok 346 ; Terms = [], VarNames = [], Report = Report0 347 ) 348 ). 349 350reader_error(error(syntax_error(What), _), [], [], refused(reader(syntax_error(What)))) :- !. 351reader_error(error(resource_error(What), _), [], [], refused(reader(resource(What)))) :- !. 352reader_error(E, [], [], refused(reader(E))). 353 354 355 /******************************* 356 * CANONICAL * 357 *******************************/

370% Variables are named through write_term's variable_names option and 371% never by binding them to '$VAR'/1 terms: an author can write 372% '$VAR'('Shell') themselves, and a writer in numbervars mode would print 373% that data term as the variable `Shell`, so the engine would read a 374% variable where the judge saw ground data. With numbervars off, the 375% author's '$VAR' terms print as the compounds they are. 376 377hornguard_canonical(Term0, Text) :- 378 copy_term(Term0, Term), 379 term_variables(Term, Vars), 380 term_singletons(Term, Singles), 381 hg_letter_names(Vars, Singles, 0, Bindings), 382 canonical_write(Term, Bindings, Text). 383 384hornguard_canonical(Term0, VarNames0, Text) :- 385 copy_term(Term0-VarNames0, Term-VarNames), 386 term_variables(Term, Vars), 387 maplist(hg_author_name(VarNames), Vars, Bindings), 388 canonical_write(Term, Bindings, Text). 389 390% A, B, ... Z, A1, B1, ... for variables that occur more than once; a 391% singleton prints as `_`. 392hg_letter_names([], _, _, []). 393hg_letter_names([V|Vs], Singles, I, [Name=V|Bs]) :- 394 ( hg_var_in(V, Singles) 395 -> Name = '_' 396 ; Letter is 0'A + I mod 26, 397 Round is I // 26, 398 ( Round =:= 0 399 -> char_code(Name, Letter) 400 ; format(atom(Name), "~c~d", [Letter, Round]) 401 ) 402 ), 403 I1 is I + 1, 404 hg_letter_names(Vs, Singles, I1, Bs). 405 406hg_author_name(VarNames, V, Name=V) :- 407 ( member(Name0=V0, VarNames), V0 == V 408 -> Name = Name0 409 ; Name = '_' 410 ). 411 412hg_var_in(V, [X|Xs]) :- 413 ( V == X -> true ; hg_var_in(V, Xs) ). 414 415% The canonical text is what a receipt hashes and what another engine 416% reads, so it must not depend on which SWI wrote it. Two places the 417% engine's writer changed between 9.2 and 10.0 are pinned down here: 418% a curly term is always written in functional notation, {}(X), and a 419% float is formatted by this module rather than by the engine. 420canonical_write(Term, Bindings, Text) :- 421 with_output_to(string(Text), 422 write_term(Term, [ quoted(true), ignore_ops(true), 423 numbervars(false), variable_names(Bindings), 424 spacing(standard), brace_terms(false), 425 portray_goal(hg_portray_float) ])). 426 427% Floats: the shortest of 15 and 17 significant digits that reads back to 428% the same double, through C's printf so every SWI and platform agrees, 429% with a fraction always present so ISO engines read a float and never 430% an integer. Non-finite values fall through to the engine's own writer. 431:- public hg_portray_float/2. 432hg_portray_float(F, _) :- 433 float(F), 434 hg_float_text(F, Text), 435 write(Text). 436 437hg_float_text(F, Text) :- 438 format(string(S15), "~15g", [F]), 439 ( catch(number_string(N15, S15), _, fail), float(N15), N15 =:= F 440 -> S0 = S15 441 ; format(string(S0), "~17g", [F]) 442 ), 443 \+ sub_string(S0, _, _, _, "inf"), 444 \+ sub_string(S0, _, _, _, "nan"), 445 hg_float_with_fraction(S0, Text). 446 447% "15000000000" -> "15000000000.0", "1e+22" -> "1.0e+22", "0.1" as is. 448hg_float_with_fraction(S0, Text) :- 449 ( sub_string(S0, Before, _, After, "e") 450 -> sub_string(S0, 0, Before, _, Mant), 451 sub_string(S0, _, After, 0, Exp), 452 ( sub_string(Mant, _, _, _, ".") -> Text = S0 453 ; format(string(Text), "~s.0e~s", [Mant, Exp]) 454 ) 455 ; sub_string(S0, _, _, _, ".") -> Text = S0 456 ; string_concat(S0, ".0", Text) 457 )