diff --git a/src/ir/auth_logic/BUILD b/src/ir/auth_logic/BUILD index 3ac023dfc..5ea7b6508 100644 --- a/src/ir/auth_logic/BUILD +++ b/src/ir/auth_logic/BUILD @@ -25,6 +25,29 @@ cc_library( "ast.h", ], visibility = ["//test:__pkg__"], + deps = [ + "//src/common/logging", + "//src/utils:overloaded", + "@absl//absl/strings:str_format", + ], +) + +cc_library( + name = "lowering_ast_datalog", + srcs = ["lowering_ast_datalog.cc"], + hdrs = [ + "ast.h", + "datalog_ir.h", + "lowering_ast_datalog.h", + "map_iter.h", + "move_append.h", + ], + visibility = ["//test:__pkg__"], + deps = [ + "//src/common/logging", + "//src/utils:overloaded", + "@absl//absl/strings:str_format", + ], ) cc_test( diff --git a/src/ir/auth_logic/ast.h b/src/ir/auth_logic/ast.h index b4c7bf8be..f647594ce 100644 --- a/src/ir/auth_logic/ast.h +++ b/src/ir/auth_logic/ast.h @@ -19,6 +19,7 @@ #ifndef SRC_IR_AUTH_LOGIC_AST_H_ #define SRC_IR_AUTH_LOGIC_AST_H_ +#include #include #include #include @@ -37,7 +38,7 @@ class Principal { // Used to represent whether a predicate is negated or not enum Sign { kNegated, kPositive }; -// Predicate corresponds to a predicate in of the form +// Predicate corresponds to a predicate of the form // (arg_1, ..., arg_n), and it may or may not be negated class Predicate { public: @@ -50,7 +51,7 @@ class Predicate { const std::string& name() const { return name_; } const std::vector& args() const { return args_; } - Sign sign() { return sign_; } + Sign sign() const { return sign_; } private: std::string name_; @@ -63,9 +64,10 @@ class Predicate { class Attribute { public: explicit Attribute(Principal principal, Predicate predicate) - : principal_(principal), predicate_(predicate) {} + : principal_(principal), predicate_(predicate) {} const Principal& principal() const { return principal_; } const Predicate& predicate() const { return predicate_; } + private: Principal principal_; Predicate predicate_; @@ -76,34 +78,35 @@ class Attribute { class CanActAs { public: explicit CanActAs(Principal left_principal, Principal right_principal) - : left_principal_(std::move(left_principal)), - right_principal_(std::move(right_principal)) {} + : left_principal_(std::move(left_principal)), + right_principal_(std::move(right_principal)) {} const Principal& left_principal() const { return left_principal_; } const Principal& right_principal() const { return right_principal_; } private: - Principal left_principal_; - Principal right_principal_; + Principal left_principal_; + Principal right_principal_; }; -// BaseFact corresponds to a base-case fact that cannot recursively include other -// facts through "canSay". "Fact" includes the recursive case. It is necessary -// that BaseFact is a separate class from Fact because the RHS of conditional -// assertions can only contain BaseFacts. +// BaseFact corresponds to a base-case fact that cannot recursively include +// other facts through "canSay". "Fact" includes the recursive case. It is +// necessary that BaseFact is a separate class from Fact because the RHS of +// conditional assertions can only contain BaseFacts. // Base facts have three forms: // - A predicate // - An attribute // - A canActAs expression -// The particular choice of form is represented with a variant which is -// encapsulated. class BaseFact { public: - explicit BaseFact(Predicate predicate) : value_(std::move(predicate)) {}; - explicit BaseFact(Attribute attribute) : value_(std::move(attribute)) {}; - explicit BaseFact(CanActAs canActAs) : value_(std::move(canActAs)) {}; + // BaseFactVariantType gives the different forms of BaseFacts. Client code + // should use this type to traverse these forms. This type may be changed in + // the future. + using BaseFactVariantType = std::variant; + explicit BaseFact(BaseFactVariantType value) : value_(std::move(value)){}; + const BaseFactVariantType& GetValue() const { return value_; } private: - std::variant value_; + BaseFactVariantType value_; }; // CanSay and Fact are forward-declared because they are mutually recursive. @@ -112,40 +115,45 @@ class Fact; // CanSay corresponds to an expression of the form canSay Fact class CanSay { - public: - explicit CanSay(Principal principal, std::unique_ptr& fact) + public: + explicit CanSay(Principal principal, std::unique_ptr& fact) : principal_(principal), fact_(std::move(fact)) {} - const Principal& principal() const { return principal_; } - const Fact* fact() const { return fact_.get(); } - private: - Principal principal_; - std::unique_ptr fact_; + const Principal& principal() const { return principal_; } + const Fact* fact() const { return fact_.get(); } + + private: + Principal principal_; + std::unique_ptr fact_; }; -// Fact corresponds to either a base fact or a an expression of the form -// canSay +// Fact corresponds to either a base fact or a an expression of the form +// canSay class Fact { public: - explicit Fact(BaseFact base_fact) : value_(std::move(base_fact)) {} - explicit Fact(std::unique_ptr can_say) - : value_(std::move(can_say)) {} + // FactVariantType gives the different forms of Facts. Client code + // should use this type to traverse these forms. This type may be changed in + // the future. + using FactVariantType = std::variant>; + explicit Fact(FactVariantType value) : value_(std::move(value)) {} + const FactVariantType& GetValue() const { return value_; } private: - std::variant> value_; + FactVariantType value_; }; -// ConditionalAssertion the particular form of assertion that can have +// ConditionalAssertion the particular form of assertion that can have // conditions which is: // :- ... class ConditionalAssertion { - public: - explicit ConditionalAssertion(Fact lhs, std::vector rhs) + public: + explicit ConditionalAssertion(Fact lhs, std::vector rhs) : lhs_(std::move(lhs)), rhs_(std::move(rhs)) {} - const Fact& lhs() const { return lhs_; } - const std::vector& rhs() const { return rhs_; } - private: - Fact lhs_; - std::vector rhs_; + const Fact& lhs() const { return lhs_; } + const std::vector& rhs() const { return rhs_; } + + private: + Fact lhs_; + std::vector rhs_; }; // Assertions can have two forms: @@ -153,20 +161,22 @@ class ConditionalAssertion { // - Conditional assertions class Assertion { public: - explicit Assertion(Fact fact) : value_(std::move(fact)) {} - explicit Assertion(ConditionalAssertion conditional_assertion) - : value_(std::move(conditional_assertion)) {} + // AssertionVariantType gives the different forms of Facts. Client code + // should use this type to traverse these forms. This type may be changed in + // the future. + using AssertionVariantType = std::variant; + explicit Assertion(AssertionVariantType value) : value_(std::move(value)) {} + const AssertionVariantType& GetValue() const { return value_; } private: - std::variant value_; + AssertionVariantType value_; }; -// SaysAssertion prepends an assertion with says" +// SaysAssertion prepends an assertion with " says" class SaysAssertion { public: explicit SaysAssertion(Principal principal, std::vector assertions) - : principal_(std::move(principal)), - assertions_(std::move(assertions)) {}; + : principal_(std::move(principal)), assertions_(std::move(assertions)){}; const Principal& principal() const { return principal_; } const std::vector& assertions() const { return assertions_; } @@ -193,7 +203,7 @@ class Query { Fact fact_; }; -// This is a top-level program which can contain +// This is a top-level program. class Program { public: explicit Program(std::vector says_assertions, diff --git a/src/ir/auth_logic/ast_test.cc b/src/ir/auth_logic/ast_test.cc index d7dd77560..757b52a72 100644 --- a/src/ir/auth_logic/ast_test.cc +++ b/src/ir/auth_logic/ast_test.cc @@ -14,8 +14,9 @@ // limitations under the License. //---------------------------------------------------------------------------- +#include "src/ir/auth_logic/ast.h" + #include #include -#include "src/ir/auth_logic/ast.h" -#include "src/common/testing/gtest.h" +#include "src/common/testing/gtest.h" diff --git a/src/ir/auth_logic/datalog_ir.h b/src/ir/auth_logic/datalog_ir.h new file mode 100644 index 000000000..2dade0c47 --- /dev/null +++ b/src/ir/auth_logic/datalog_ir.h @@ -0,0 +1,69 @@ +/* + * Copyright 2022 Google LLC. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +// This file contains the datalog IR (DLIR) which makes the translation from +// this authorization logic into datalog simpler. +#ifndef SRC_IR_AUTH_LOGIC_DATALOG_IR_H_ +#define SRC_IR_AUTH_LOGIC_DATALOG_IR_H_ + +#include + +#include "src/ir/auth_logic/ast.h" + +namespace raksha::ir::auth_logic { + +// A conditional datalog assertion with a left hand side and a right hand +// side. +class DLIRCondAssertion { + public: + explicit DLIRCondAssertion(Predicate lhs, std::vector rhs) + : lhs_(std::move(lhs)), rhs_(std::move(rhs)) {} + + private: + Predicate lhs_; + std::vector rhs_; +}; + +// A Datalog IR assertion is either: +// - an unconditional fact which is just a predicate +// - a conditional assertion +class DLIRAssertion { + public: + // DLIRAssertionVariantType represents the alternative forms for + // DLIRAssertions. Client code should use this type for traversing + // DLIRAssertions. This type may be changed in the future. + using DLIRAssertionVariantType = std::variant; + explicit DLIRAssertion(DLIRAssertionVariantType value) + : value_(std::move(value)) {} + + private: + std::variant value_; +}; + +class DLIRProgram { + public: + DLIRProgram(std::vector assertions, + std::vector outputs) + : assertions_(std::move(assertions)), outputs_(std::move(outputs)) {} + + private: + std::vector assertions_; + std::vector outputs_; +}; + +} // namespace raksha::ir::auth_logic + +#endif // SRC_IR_AUTH_LOGIC_DATALOG_IR_H_ diff --git a/src/ir/auth_logic/lowering_ast_datalog.cc b/src/ir/auth_logic/lowering_ast_datalog.cc new file mode 100644 index 000000000..ec9080039 --- /dev/null +++ b/src/ir/auth_logic/lowering_ast_datalog.cc @@ -0,0 +1,299 @@ +/* + * Copyright 2022 Google LLC. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +#include "src/ir/auth_logic/lowering_ast_datalog.h" + +#include "src/ir/auth_logic/ast.h" +#include "src/ir/auth_logic/map_iter.h" +#include "src/ir/auth_logic/move_append.h" + +namespace raksha::ir::auth_logic { + +namespace { +// This function takes a `predicate` and creates a new predicate as follows: +// - Prepend the `modifier` to the name of the given `predicate`. +// - Prepend the given `args` to the original list of arguments of +// `predicate`. +// +// This is used in a few places in the translation, for example, to translate +// "X says blah(args)" into "says_blah(X, args)". +Predicate PushOntoPredicate(absl::string_view modifier, + std::vector new_args, + const Predicate& predicate) { + std::string new_name = absl::StrCat(std::move(modifier), predicate.name()); + MoveAppend(new_args, std::vector(predicate.args())); + Sign sign_copy = predicate.sign(); + return Predicate(new_name, std::move(new_args), sign_copy); +} + +// This function is an abbreviation for `PushPrincipal` where: +// - a modifier is added +// - just one new principal is added as an argument. +// This is a common case in this translation because it is used for +// `x says blah(args)` and `x canActAs y` and other constructions involving a +// principal name. +Predicate PushPrincipal(absl::string_view modifier, const Principal& principal, + const Predicate& predicate) { + return PushOntoPredicate(modifier, {principal.name()}, predicate); +} + +Predicate AttributeToDLIR(const Attribute& attribute) { + // If attribute is `X pred(args...)` the following predicate is + // `pred(X, args...)` + return PushPrincipal("", attribute.principal(), attribute.predicate()); +} + +Predicate CanActAsToDLIR(const CanActAs& can_act_as) { + return Predicate( + "canActAs", + {can_act_as.left_principal().name(), can_act_as.right_principal().name()}, + kPositive); +} +} // namespace + +DLIRAssertion LoweringToDatalogPass::SpokenAttributeToDLIR( + const Principal& speaker, const Attribute& attribute) { + Predicate main_predicate = AttributeToDLIR(attribute); + + // Attributes interact with "canActAs" because if "Y canActAs X" + // then Y also picks up X's attributes. We need to generate + // an additional rule to implement this behavior. If the attribute + // under translation is `X PredX`, the additional rule is: + // `speaker says Y PredX :- + // speaker says Y canActAs X, speaker says X PredX` + // (Where Y is a fresh variable) + Principal prin_y(FreshVar()); + + // This is `speaker says Y PredX` + Predicate generated_lhs = PushPrincipal("says_", prin_y, main_predicate); + + Predicate y_can_act_as_x("canActAs", + {prin_y.name(), attribute.principal().name()}, + Sign::kPositive); + + Predicate speaker_says_y_can_act_as_x = + PushPrincipal("says_", speaker, y_can_act_as_x); + + // This is `speaker says X PredX` + Predicate speaker_says_x_pred = + PushPrincipal("says_", speaker, main_predicate); + + // This is the full generated rule: + // `speaker says Y PredX :- + // speaker says Y canActAs X, speaker says X PredX` + return DLIRAssertion( + DLIRCondAssertion(generated_lhs, {std::move(speaker_says_y_can_act_as_x), + std::move(speaker_says_x_pred)})); +} + +DLIRAssertion LoweringToDatalogPass::SpokenCanActAsToDLIR( + const Principal& speaker, const CanActAs& can_act_as) { + Predicate main_predicate = CanActAsToDLIR(can_act_as); + + // "canActAs" facts are passed to principals via other canActAs facts in + // essentially the same way as attributes. This function adds extra + // rules to pass these around. If the `canActAs` under translation + // is `X canActAs Z`, then the rule we need to generate is: + // `speaker says Y PredX :- + // speaker says Y canActAs X, speaker says X canActAsZ` + // (Where Y is a fresh variable) + Principal prin_y(FreshVar()); + + // This is `speaker says Y PredX` + Predicate generated_lhs = PushPrincipal("says_", prin_y, main_predicate); + + Predicate y_can_act_as_x("canActAs", + {prin_y.name(), can_act_as.left_principal().name()}, + Sign::kPositive); + + Predicate speaker_says_y_can_act_as_x = + PushPrincipal("says_", speaker, y_can_act_as_x); + + // This is `speaker says X canActAs Z` + Predicate speaker_says_x_can_act_as_z = + PushPrincipal("says_", speaker, main_predicate); + + // This is the full generated rule: + // `speaker says Y PredX :- + // speaker says Y canActAs X, speaker says X canActAs Z` + return DLIRAssertion(DLIRCondAssertion( + generated_lhs, {std::move(speaker_says_y_can_act_as_x), + std::move(speaker_says_x_can_act_as_z)})); +} + +std::pair> +LoweringToDatalogPass::BaseFactToDLIRInner(const Principal& speaker, + const Predicate& predicate) { + return std::make_pair(predicate, std::vector({})); +} + +std::pair> +LoweringToDatalogPass::BaseFactToDLIRInner(const Principal& speaker, + const Attribute& attribute) { + return std::make_pair( + AttributeToDLIR(attribute), + std::vector({SpokenAttributeToDLIR(speaker, attribute)})); +} + +std::pair> +LoweringToDatalogPass::BaseFactToDLIRInner(const Principal& speaker, + const CanActAs& canActAs) { + return std::make_pair( + CanActAsToDLIR(canActAs), + std::vector({SpokenCanActAsToDLIR(speaker, canActAs)})); +} + +std::pair> +LoweringToDatalogPass::BaseFactToDLIR(const Principal& speaker, + const BaseFact& base_fact) { + return std::visit( + [this, &speaker](auto value) { + return BaseFactToDLIRInner(speaker, value); + }, + base_fact.GetValue()); +} + +std::pair> +LoweringToDatalogPass::FactToDLIR(const Principal& speaker, const Fact& fact) { + return std::visit( + raksha::utils::overloaded{ + [this, speaker](const BaseFact& base_fact) { + return BaseFactToDLIR(speaker, base_fact); + }, + [this, speaker](const std::unique_ptr& can_say) { + auto [inner_fact_dlir, gen_rules] = + FactToDLIR(speaker, *can_say->fact()); + + Principal fresh_principal(FreshVar()); + + // The following code generates the extra rule that does + // delegation. This rule is: + // ``` + // speaker says inner_fact_dlir:- + // fresh_principal says inner_fact_dlir, + // speaker says fresh_principal canSay inner_fact_dlir + // ``` + + // This is p says inner_fact_dlir + auto lhs = PushPrincipal("says_", speaker, inner_fact_dlir); + auto fresh_prin_says_inner = + PushPrincipal("says_", fresh_principal, inner_fact_dlir); + auto speaker_says_fresh_cansay_inner = PushPrincipal( + "says_", speaker, + PushPrincipal("canSay_", fresh_principal, inner_fact_dlir)); + auto rhs = {fresh_prin_says_inner, speaker_says_fresh_cansay_inner}; + DLIRAssertion generated_rule(DLIRCondAssertion(lhs, rhs)); + gen_rules.push_back(generated_rule); + + // Note that prin_cansay_pred does not begin with "speaker says" + // because only the top-level fact should. This could + // be a recursive call, so it might not be processing + // the top-level fact. The top-level fact gets wrapped + // in a "says" during the call to translate the assertion + // in which this appears. + auto prin_cansay_pred = + PushPrincipal("canSay_", can_say->principal(), inner_fact_dlir); + return std::make_pair(prin_cansay_pred, gen_rules); + }}, + fact.GetValue()); +} + +std::vector LoweringToDatalogPass::GenerateDLIRAssertions( + const Principal& speaker, const Fact& fact) { + auto [fact_predicate, generated_rules] = FactToDLIR(speaker, fact); + DLIRAssertion main_assertion = + DLIRAssertion(PushPrincipal("says_", speaker, fact_predicate)); + generated_rules.push_back(main_assertion); + return generated_rules; +} + +std::vector LoweringToDatalogPass::GenerateDLIRAssertions( + const Principal& speaker, + const ConditionalAssertion& conditional_assertion) { + auto dlir_rhs = MapIter( + conditional_assertion.rhs(), [this, speaker](const BaseFact& base_fact) { + auto [dlir_translation, not_used] = BaseFactToDLIR(speaker, base_fact); + return PushPrincipal("says_", speaker, dlir_translation); + }); + auto [dlir_lhs, gen_rules] = FactToDLIR(speaker, conditional_assertion.lhs()); + auto dlir_lhs_prime = PushPrincipal("says_", speaker, dlir_lhs); + DLIRAssertion dlir_assertion(DLIRCondAssertion(dlir_lhs_prime, dlir_rhs)); + gen_rules.push_back(dlir_assertion); + return gen_rules; +} + +std::vector LoweringToDatalogPass::SingleSaysAssertionToDLIR( + const Principal& speaker, const Assertion& assertion) { + return std::visit( + // I thought it would be possible to skip the overloaded (just like + // in BaseFactToDLIR, but I needed to give the types for each + // variant explicitly to avoid a type error). + raksha::utils::overloaded{ + [this, &speaker](const Fact& fact) { + return GenerateDLIRAssertions(speaker, fact); + }, + [this, &speaker](const ConditionalAssertion& conditional_assertion) { + return GenerateDLIRAssertions(speaker, conditional_assertion); + }}, + assertion.GetValue()); +} + +std::vector LoweringToDatalogPass::SaysAssertionToDLIR( + const SaysAssertion& says_assertion) { + std::vector ret = {}; + for (const Assertion& assertion : says_assertion.assertions()) { + std::vector single_translation = + SingleSaysAssertionToDLIR(says_assertion.principal(), assertion); + MoveAppend(ret, std::move(single_translation)); + } + return ret; +} + +std::vector LoweringToDatalogPass::SaysAssertionsToDLIR( + const std::vector& says_assertions) { + std::vector ret = {}; + for (const SaysAssertion& says_assertion : says_assertions) { + auto single_translation = SaysAssertionToDLIR(says_assertion); + MoveAppend(ret, std::move(single_translation)); + } + return ret; +} + +std::vector LoweringToDatalogPass::QueriesToDLIR( + const std::vector& queries) { + return MapIter(queries, [this](const Query& query) { + auto [main_pred, not_used] = FactToDLIR(query.principal(), query.fact()); + main_pred = PushPrincipal("says_", query.principal(), main_pred); + Predicate lhs(query.name(), {"dummy_var"}, kPositive); + return DLIRAssertion(DLIRCondAssertion(lhs, {main_pred, kDummyPredicate})); + }); +} + +DLIRProgram LoweringToDatalogPass::ProgToDLIR(const Program& program) { + auto dlir_assertions = SaysAssertionsToDLIR(program.says_assertions()); + auto dlir_queries = QueriesToDLIR(program.queries()); + // We need to add a fact that says the dummy variable used in queries is + // grounded. + DLIRAssertion dummy_assertion(kDummyPredicate); + MoveAppend(dlir_assertions, std::move(dlir_queries)); + dlir_assertions.push_back(dummy_assertion); + + auto outputs = MapIter( + program.queries(), [](const Query& query) { return query.name(); }); + return DLIRProgram(dlir_assertions, outputs); +} + +} // namespace raksha::ir::auth_logic diff --git a/src/ir/auth_logic/lowering_ast_datalog.h b/src/ir/auth_logic/lowering_ast_datalog.h new file mode 100644 index 000000000..ea331762a --- /dev/null +++ b/src/ir/auth_logic/lowering_ast_datalog.h @@ -0,0 +1,219 @@ +/* + * Copyright 2022 Google LLC. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +// This file contains the datalog IR (DLIR) which makes the translation from +// this authorization logic into datalog simpler. +#ifndef SRC_IR_AUTH_LOGIC_LOWERING_AST_DATALOG_H_ +#define SRC_IR_AUTH_LOGIC_LOWERING_AST_DATALOG_H_ + +#include +#include +#include //included for std::pair + +#include "absl/strings/str_cat.h" +#include "absl/strings/str_format.h" +#include "src/common/logging/logging.h" +#include "src/ir/auth_logic/ast.h" +#include "src/ir/auth_logic/datalog_ir.h" +#include "src/ir/auth_logic/move_append.h" +#include "src/utils/overloaded.h" + +namespace raksha::ir::auth_logic { + +// This implements a compiler pass for converting authorization logic +// (represented by ast.h) into the datalog ir (in datalog_ir.h). The only +// public interface to this class is a single function "Lower" which takes +// as input an authorization logic program and returns a datalog program. +// +// (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(const Program& auth_logic_program) { + return LoweringToDatalogPass().ProgToDLIR(auth_logic_program); + } + + private: + LoweringToDatalogPass() : fresh_var_count_(0) {} + + // This returns a fresh variable name. Fresh variables are introduced in a + // few places during the translation. + std::string FreshVar() { + CHECK(fresh_var_count_ < std::numeric_limits::max()); + return "x__" + std::to_string(++fresh_var_count_); + } + + // 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 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 it has the same speaker as the head of the assertion. + DLIRAssertion SpokenAttributeToDLIR(const Principal& speaker, + const Attribute& attribute); + + // 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(const Principal& speaker, + const CanActAs& can_act_as); + + std::pair> BaseFactToDLIRInner( + const Principal& speaker, const Predicate& predicate); + + std::pair> BaseFactToDLIRInner( + const Principal& speaker, const Attribute& attribute); + + std::pair> BaseFactToDLIRInner( + const Principal& speaker, const CanActAs& canActAs); + + // The second return value represents 0 or 1 newly generated rules, so an + // option might seem more intuitive. However, the interface that consumes + // this needs to construct a vector anyway, so a vector is used in the + // return type. + std::pair> BaseFactToDLIR( + const Principal& speaker, const BaseFact& base_fact); + + // This can result in 0 or more new rules because the translation of + // nested canSayFacts might result in more than 1 rule. + std::pair> FactToDLIR( + const Principal& speaker, const Fact& fact); + + std::vector GenerateDLIRAssertions(const Principal& speaker, + const Fact& fact); + + std::vector GenerateDLIRAssertions( + const Principal& speaker, + const ConditionalAssertion& conditional_assertion); + + std::vector SingleSaysAssertionToDLIR( + const Principal& speaker, const Assertion& assertion); + + std::vector SaysAssertionToDLIR( + const SaysAssertion& says_assertion); + + std::vector SaysAssertionsToDLIR( + const std::vector& says_assertions); + + // Queries are like predicates with arity 0. Souffle does not have predicates + // with arity 0, so we represent them as having one argument which is a + // constant. + static inline Predicate kDummyPredicate = + Predicate("grounded_dummy", {"dummy_var"}, kPositive); + + std::vector QueriesToDLIR(const std::vector& queries); + + DLIRProgram ProgToDLIR(const Program& program); + + uint64_t fresh_var_count_; +}; + +} // namespace raksha::ir::auth_logic + +#endif // SRC_IR_AUTH_LOGIC_AST_H_ diff --git a/src/ir/auth_logic/map_iter.h b/src/ir/auth_logic/map_iter.h new file mode 100644 index 000000000..dbd19d8ff --- /dev/null +++ b/src/ir/auth_logic/map_iter.h @@ -0,0 +1,36 @@ +/* + * Copyright 2022 Google LLC. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +// This file contains the datalog IR (DLIR) which makes the translation from +// this authorization logic into datalog simpler. +#ifndef SRC_IR_AUTH_LOGIC_MAP_ITER_H_ +#define SRC_IR_AUTH_LOGIC_MAP_ITER_H_ + +namespace raksha::ir::auth_logic { + +template +std::vector MapIter(const std::vector& input, F f) { + std::vector result; + result.reserve(input.size()); + for (auto& entity : input) { + result.push_back(f(entity)); + } + return result; +} + +} // namespace raksha::ir::auth_logic + +#endif // SRC_IR_AUTH_LOGIC_MAP_ITER_H_ diff --git a/src/ir/auth_logic/move_append.h b/src/ir/auth_logic/move_append.h new file mode 100644 index 000000000..34815b7ff --- /dev/null +++ b/src/ir/auth_logic/move_append.h @@ -0,0 +1,31 @@ +/* + * Copyright 2022 Google LLC. + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +// This file contains the datalog IR (DLIR) which makes the translation from +// this authorization logic into datalog simpler. +#ifndef SRC_IR_AUTH_LOGIC_MOVE_APPEND_H_ +#define SRC_IR_AUTH_LOGIC_MOVE_APPEND_H_ + +namespace raksha::ir::auth_logic { + +template +void MoveAppend(std::vector& dst, std::vector&& src) { + dst.insert(dst.end(), std::make_move_iterator(src.begin()), + std::make_move_iterator(src.end())); +} + +} // namespace raksha::ir::auth_logic +#endif // SRC_IR_AUTH_LOGIC_MOVE_APPEND_H_