diff --git a/src/ir/auth_logic/lowering_ast_datalog.h b/src/ir/auth_logic/lowering_ast_datalog.h index 14f65119c..5a906553a 100644 --- a/src/ir/auth_logic/lowering_ast_datalog.h +++ b/src/ir/auth_logic/lowering_ast_datalog.h @@ -35,6 +35,92 @@ namespace raksha::ir::auth_logic { // (Internally, this is a stateful class because it uses a counter to // generate fresh names for arguments. The public interface hides this // implementation detail.) + +//----------------------------------------------------------------------------- +// Description of Translation +//----------------------------------------------------------------------------- +// Asside from queries, this translation is quite similar to the one given in +// Section 7 of the SecPal paper "SecPAL: Design and Semantics of a Decentralized +// Authorization Language" +// https://www.pure.ed.ac.uk/ws/files/17662538/jcs_final.pdf. See that section +// for a formal and completely general description of this translation. This +// comment gives a more intuitive description using a few examples at the +// expense of losing some generality. +// +// As a minor wrinkle, this language also supports grouping assertions together +// as in: +// Prin says { assertion_1, ..., assertion_n } +// and these are simply "unrolled" to +// Prin says assertion_1. +// ... +// Prin says assertion_n. +// +// +// ## Translation of assertions +// +// First, predicates with modifiers like "says", "canSay", and "actAs" are +// converted into normal predicates by appending these modifiers to the +// predicate name and moving the principals referenced by these predicates +// into the arguments of the predicates. So for example +// A says B canSay foo(x, y) +// becomes +// says_canSay_foo(A, B, x, y) +// The rest of this comment ignores this part of the translation for the sake +// of readability. +// +// Next we need to add a principal for the conditions in assertions. To prove +// an assertion like +// "A says fact(x) :- fact1(x), fact2(x). +// we need to show that *A believes* both fact1(x) and fact2(x). So we prepend +// predicates on the RHS in "A says", producing the new assertion: +// A says fact(x) :- A says fact1(x), A says fact2(x) +// (where says is actually prepended to the names of predicates and A becomes +// an extra argument as above). +// +// Next we need to translate delegations which should pass beliefs from one +// principal to another. For example, if we have +// A says B canSay fact(x) :- fact1(x) +// we do the usual translation resulting in +// (1) A says B canSay fact(x) :- A says fact1(x) +// but we also add the additional rule +// (2) A says fact(x) :- x says fact(x), A says x canSay fact(x) +// where x is a fresh variable. +// The result is that rule (1) gives the condition for delegation +// and rule (2) passes beliefs from B to A when the condition from (1) is met. +// +// Finally we need to translate canActAs which should pass properties from +// one principal to another: +// Assertions of either the form +// A says B canActAs C :- ... +// or +// A says B :- +// are claims by A that B has a property (where canActAs is just a special +// case). Syntactically these are both treated as "A says B " with +// different instances of . Whenever some other principal can act +// as B, we want to pass these properties from B to that other principal. +// (For the special case where this property is B canActAs C, this essentially +// makes canActAs transitive). In either case, we add an additional rule +// A says x verbphrase <- A says x canActAs B, A says B verbphrase +// which will add "verbphrase" as a property of D whenever we can prove +// the assertion "A says D canActAsB". +// +// ## Translation of Queries +// Neither Souffle nor SecPal support queries, but this language does. +// Queries check of a single unconditional assertion is true. A query of +// the form: +// ```Datalog +// Q_NAME = query ASSERTION() ? +// ``` +// +// is translated into an assertion with just one argument, and this +// assertion is made an output, so we can simply check the CSV that +// souffle emits as in: +// ```Datalog +// Q_NAME("dummy_var") :- grounded("dummy_var"), ASSERTION(). +// grounded("dummy_var"). +// .output Q_NAME +// ``` + class LoweringToDatalogPass { public: static DLIRProgram Lower(Program auth_logic_program) { @@ -77,16 +163,16 @@ class LoweringToDatalogPass { attribute.predicate()); } - // This is the translation for the attribute case of a base fact. - // This returns two outputs as a pair: + // Translating an attribute results in two objects: // - A predicate, this is the main result of the translation // - An additional rule that allows attributes to be passed with canActAs + // This function is for generating the additional rule. // This takes both a speaker and the actual attribute as argument because - // the speaker is needed to generate the additional rule. Note all base + // the speaker is needed to generate the additional rule. Note that all base // facts have a speaker either explicitly or implicitly: // - If it appears on the LHS of an assertion, it explicitly has a speaker // - If it appears on the RHS of an assertion, it behaves semantically - // like has the same speaker as the head of the assertion. + // like it has the same speaker as the head of the assertion. DLIRAssertion SpokenAttributeToDLIR(Principal speaker, Attribute attribute) { Predicate main_predicate = AttributeToDLIR(attribute); @@ -128,6 +214,11 @@ class LoweringToDatalogPass { can_act_as.right_principal().name()}, kPositive); } + // In the same way that attributes are passed around with "CanActAs", so + // are other "CanActAs" facts. To implement this, the translation of + // CanActAs also results in both a predicate and an extra rule that passes + // these facts around. This function is for generating the extra rule and + // it works similarly to "SpokenAttributeToDLIR". DLIRAssertion SpokenCanActAsToDLIR(Principal speaker, CanActAs can_act_as) { Predicate main_predicate = CanActAsToDLIR(can_act_as);