From a7ac196fb1b37261a69d353c591e4e959b3cb583 Mon Sep 17 00:00:00 2001 From: Harsha Mandadi Date: Mon, 12 Dec 2022 16:41:18 -0800 Subject: [PATCH] Add more integration tests to auth_logic. This CL takes care of following items 1. Add integration tests to authorization logic to validate the datalog generated and expected query results 2. Earlier versions of auth logic did not support number types (instead numbers are declared as symbols). Added support for number types as well. PiperOrigin-RevId: 494864193 --- src/ir/auth_logic/lowering_ast_datalog.cc | 24 ++-- src/ir/auth_logic/souffle_emitter.h | 9 +- src/ir/auth_logic/souffle_emitter_test.cc | 4 - src/ir/auth_logic/test_inputs/BUILD | 76 +++++++++++ .../test_inputs/basic_num_comparisons.auth | 31 +++++ .../test_inputs/basic_num_comparisons.dl | 84 ++++++++++++ .../test_inputs/basic_num_comparisons.queries | 14 ++ src/ir/auth_logic/test_inputs/canActAs.auth | 54 ++++++++ src/ir/auth_logic/test_inputs/canActAs.dl | 129 ++++++++++++++++++ .../auth_logic/test_inputs/canActAs.queries | 2 + .../comparisons_with_delegation.auth | 29 ++++ .../comparisons_with_delegation.dl | 59 ++++++++ .../comparisons_with_delegation.queries | 2 + src/ir/auth_logic/test_inputs/conditions.auth | 13 ++ src/ir/auth_logic/test_inputs/conditions.dl | 35 +++++ .../auth_logic/test_inputs/conditions.queries | 3 + src/ir/auth_logic/test_inputs/delegation.auth | 33 +++++ src/ir/auth_logic/test_inputs/delegation.dl | 58 ++++++++ .../auth_logic/test_inputs/delegation.queries | 6 + .../auth_logic/test_inputs/dot_in_names.auth | 11 ++ src/ir/auth_logic/test_inputs/dot_in_names.dl | 33 +++++ src/ir/auth_logic/test_inputs/hyphenIDs.auth | 27 ++++ src/ir/auth_logic/test_inputs/hyphenIDs.dl | 24 ++++ .../test_inputs/multiverse_handling.auth | 13 ++ .../test_inputs/multiverse_handling.dl | 33 +++++ .../test_inputs/multiverse_handling.queries | 2 + src/ir/auth_logic/test_inputs/negation.auth | 15 ++ src/ir/auth_logic/test_inputs/negation.dl | 29 ++++ .../auth_logic/test_inputs/negation.queries | 3 + .../test_inputs/num_strings_in_names.auth | 6 + .../test_inputs/num_strings_in_names.dl | 22 +++ .../auth_logic/test_inputs/test_authlogic.sh | 85 ++++++++++++ .../test_inputs/test_decl_skip.auth | 6 + .../auth_logic/test_inputs/test_decl_skip.dl | 22 +++ .../test_inputs/type_declarations.auth | 7 + .../test_inputs/type_declarations.dl | 26 ++++ src/policy/auth_logic/AuthLogic.g4 | 2 +- 37 files changed, 1016 insertions(+), 15 deletions(-) create mode 100644 src/ir/auth_logic/test_inputs/BUILD create mode 100644 src/ir/auth_logic/test_inputs/basic_num_comparisons.auth create mode 100644 src/ir/auth_logic/test_inputs/basic_num_comparisons.dl create mode 100644 src/ir/auth_logic/test_inputs/basic_num_comparisons.queries create mode 100644 src/ir/auth_logic/test_inputs/canActAs.auth create mode 100644 src/ir/auth_logic/test_inputs/canActAs.dl create mode 100644 src/ir/auth_logic/test_inputs/canActAs.queries create mode 100644 src/ir/auth_logic/test_inputs/comparisons_with_delegation.auth create mode 100644 src/ir/auth_logic/test_inputs/comparisons_with_delegation.dl create mode 100644 src/ir/auth_logic/test_inputs/comparisons_with_delegation.queries create mode 100644 src/ir/auth_logic/test_inputs/conditions.auth create mode 100644 src/ir/auth_logic/test_inputs/conditions.dl create mode 100644 src/ir/auth_logic/test_inputs/conditions.queries create mode 100644 src/ir/auth_logic/test_inputs/delegation.auth create mode 100644 src/ir/auth_logic/test_inputs/delegation.dl create mode 100644 src/ir/auth_logic/test_inputs/delegation.queries create mode 100644 src/ir/auth_logic/test_inputs/dot_in_names.auth create mode 100644 src/ir/auth_logic/test_inputs/dot_in_names.dl create mode 100644 src/ir/auth_logic/test_inputs/hyphenIDs.auth create mode 100644 src/ir/auth_logic/test_inputs/hyphenIDs.dl create mode 100644 src/ir/auth_logic/test_inputs/multiverse_handling.auth create mode 100644 src/ir/auth_logic/test_inputs/multiverse_handling.dl create mode 100644 src/ir/auth_logic/test_inputs/multiverse_handling.queries create mode 100644 src/ir/auth_logic/test_inputs/negation.auth create mode 100644 src/ir/auth_logic/test_inputs/negation.dl create mode 100644 src/ir/auth_logic/test_inputs/negation.queries create mode 100644 src/ir/auth_logic/test_inputs/num_strings_in_names.auth create mode 100644 src/ir/auth_logic/test_inputs/num_strings_in_names.dl create mode 100755 src/ir/auth_logic/test_inputs/test_authlogic.sh create mode 100644 src/ir/auth_logic/test_inputs/test_decl_skip.auth create mode 100644 src/ir/auth_logic/test_inputs/test_decl_skip.dl create mode 100644 src/ir/auth_logic/test_inputs/type_declarations.auth create mode 100644 src/ir/auth_logic/test_inputs/type_declarations.dl diff --git a/src/ir/auth_logic/lowering_ast_datalog.cc b/src/ir/auth_logic/lowering_ast_datalog.cc index 8a79b1261..25df6eef8 100644 --- a/src/ir/auth_logic/lowering_ast_datalog.cc +++ b/src/ir/auth_logic/lowering_ast_datalog.cc @@ -50,7 +50,14 @@ datalog::Predicate PushOntoPredicate(absl::string_view modifier, datalog::Predicate PushPrincipal(absl::string_view modifier, const Principal& principal, const datalog::Predicate& predicate) { - return PushOntoPredicate(modifier, {principal.name()}, predicate); + // do not modify predicate when dealing with binary operators + static const absl::flat_hash_set comparison_operators = { + {"<"}, {">"}, {"="}, {"!="}, {"<="}, {">="}}; + + return (comparison_operators.find(predicate.name()) == + comparison_operators.end()) + ? PushOntoPredicate(modifier, {principal.name()}, predicate) + : predicate; } datalog::Predicate AttributeToDLIR(const Attribute& attribute) { @@ -397,6 +404,13 @@ LoweringToDatalogPass::RelationDeclarationToDLIR( std::vector transformed_declarations = LoweringToDatalogPass::TransformAttributeDeclarations( relation_declarations); + // The transformed relation declarations are the same as the ones from the + // surface program plus another one for "canActAs". Declaration being added is + //.decl canActAs(p1 : Principal, p2 : Principal) + transformed_declarations.push_back(datalog::RelationDeclaration( + "canActAs", false, + {datalog::Argument("p1", datalog::ArgumentType::MakePrincipalType()), + datalog::Argument("p2", datalog::ArgumentType::MakePrincipalType())})); // Produce a mapping from predicate names to predicate typings // (where a predicate typing is the same as a predicate relation declaration) common::containers::HashMap @@ -407,13 +421,7 @@ LoweringToDatalogPass::RelationDeclarationToDLIR( } absl::c_move(LoweringToDatalogPass::GetCanSayDeclarations(type_environment), std::back_inserter(transformed_declarations)); - // The transformed relation declarations are the same as the ones from the - // surface program plus another one for "canActAs". Declaration being added is - //.decl canActAs(p1 : Principal, p2 : Principal) - transformed_declarations.push_back(datalog::RelationDeclaration( - "canActAs", false, - {datalog::Argument("p1", datalog::ArgumentType::MakePrincipalType()), - datalog::Argument("p2", datalog::ArgumentType::MakePrincipalType())})); + // The translated declarations are all extended with "says_" and a speaker // argument std::vector diff --git a/src/ir/auth_logic/souffle_emitter.h b/src/ir/auth_logic/souffle_emitter.h index 2bf7bef91..8a54e67a4 100644 --- a/src/ir/auth_logic/souffle_emitter.h +++ b/src/ir/auth_logic/souffle_emitter.h @@ -175,9 +175,16 @@ class SouffleEmitter { absl::flat_hash_set type_names; for (const auto& declaration : program.relation_declarations()) { for (const auto& argument : declaration.arguments()) { + if (argument.argument_type().kind() == + datalog::ArgumentType::Kind::kNumber) { + type_names.insert(absl::StrCat( + ".type ", argument.argument_type().name(), " <: number")); + continue; + } if (!skip_declarations && argument.argument_type().kind() != datalog::ArgumentType::Kind::kCustom) continue; + if (!skip_declarations && GetRelationsToNotDeclare().find(argument.argument_type().name()) != GetRelationsToNotDeclare().end()) @@ -186,8 +193,6 @@ class SouffleEmitter { ".type ", argument.argument_type().name(), " <: symbol")); } } - // TODO (#633) work around till we add number types in C++ version. - type_names.insert(absl::StrCat(".type Number", " <: symbol")); std::vector sorted_type_names(type_names.begin(), type_names.end()); std::sort(sorted_type_names.begin(), sorted_type_names.end()); diff --git a/src/ir/auth_logic/souffle_emitter_test.cc b/src/ir/auth_logic/souffle_emitter_test.cc index a6700ff4f..87ed91000 100644 --- a/src/ir/auth_logic/souffle_emitter_test.cc +++ b/src/ir/auth_logic/souffle_emitter_test.cc @@ -61,7 +61,6 @@ Program BuildRelationDeclarationProgram(SaysAssertion assertion) { TEST(EmitterTestSuite, EmptyAuthLogicTest) { std::string expected = R"(.type DummyType <: symbol -.type Number <: symbol .decl grounded_dummy(dummy_param : DummyType) .decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) grounded_dummy("dummy_var"). @@ -74,7 +73,6 @@ grounded_dummy("dummy_var"). TEST(EmitterTestSuite, SimpleTest) { std::string expected = R"(.type DummyType <: symbol -.type Number <: symbol .decl grounded_dummy(dummy_param : DummyType) .decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) says_foo(TestPrincipal, bar, baz). @@ -99,7 +97,6 @@ TEST(EmitterTestSuite, CanSayTest) { std::string expected = R"(.type DummyType <: symbol .type FileName <: symbol -.type Number <: symbol .decl grounded_dummy(dummy_param : DummyType) .decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) .decl says_canSay_grantAccess(speaker : Principal, delegatee1 : Principal, x0 : Principal, x1 : FileName) @@ -128,7 +125,6 @@ TEST(EmitterTestSuite, FloatCanSayTest) { std::string expected = R"(.type DummyType <: symbol .type FileName <: symbol -.type Number <: symbol .decl grounded_dummy(dummy_param : DummyType) .decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) .decl says_canSay_canSay_grantAccess(speaker : Principal, delegatee2 : Principal, delegatee1 : Principal, x0 : Principal, x1 : FileName) diff --git a/src/ir/auth_logic/test_inputs/BUILD b/src/ir/auth_logic/test_inputs/BUILD new file mode 100644 index 000000000..aef4ffd10 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/BUILD @@ -0,0 +1,76 @@ +#----------------------------------------------------------------------------- +# 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 +# +# https://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. +#---------------------------------------------------------------------------- +package( + default_visibility = ["//src:__subpackages__"], + features = ["layering_check"], + licenses = ["notice"], +) + +[sh_test( + name = "test_%s" % test_name, + srcs = ["test_authlogic.sh"], + args = [ + "$(location //src/backends/policy_engine/souffle:raksha_policy_datalog_emitter)", + "$(location :%s.auth)" % test_name, + "$(location :%s.dl)" % test_name, + "1", + "$(location :%s.queries)" % test_name, + ], + data = [ + ":%s.auth" % test_name, + ":%s.dl" % test_name, + ":%s.queries" % test_name, + "//src/backends/policy_engine/souffle:raksha_policy_datalog_emitter", + "//third_party/mcpp", + "//third_party/souffle:main", + ], + env = { + "SOUFFLE_BIN": "$(rootpath //third_party/souffle:main)", + }, +) for test_name in [ + "canActAs", + "conditions", + "negation", + "multiverse_handling", + "delegation", + "comparisons_with_delegation", + "basic_num_comparisons", +]] + +[sh_test( + name = "test_%s" % test_name, + srcs = ["test_authlogic.sh"], + args = [ + "$(location //src/backends/policy_engine/souffle:raksha_policy_datalog_emitter)", + "$(location :%s.auth)" % test_name, + "$(location :%s.dl)" % test_name, + ], + data = [ + ":%s.auth" % test_name, + ":%s.dl" % test_name, + "//src/backends/policy_engine/souffle:raksha_policy_datalog_emitter", + "//third_party/souffle:main", + ], + env = { + "SOUFFLE_BIN": "$(rootpath //third_party/souffle:main)", + }, +) for test_name in [ + "type_declarations", + "test_decl_skip", + "num_strings_in_names", + "hyphenIDs", + "dot_in_names", +]] diff --git a/src/ir/auth_logic/test_inputs/basic_num_comparisons.auth b/src/ir/auth_logic/test_inputs/basic_num_comparisons.auth new file mode 100644 index 000000000..048355dab --- /dev/null +++ b/src/ir/auth_logic/test_inputs/basic_num_comparisons.auth @@ -0,0 +1,31 @@ +.decl someFact(n : Number) + +"test_principal" says someFact(1) :- 3 < 5. +"test_principal" says someFact(2) :- 3 < 0. +"test_principal" says someFact(3) :- 5 > 0. +"test_principal" says someFact(4) :- 3 > 999. +"test_principal" says someFact(5) :- 4 = 4. +"test_principal" says someFact(6) :- 47 = 42. +"test_principal" says someFact(7) :- 47 != 42. +"test_principal" says someFact(8) :- 0 != 0. +"test_principal" says someFact(9) :- 3 <= 5. +"test_principal" says someFact(10) :- 3 <= 3. +"test_principal" says someFact(11) :- 3 <= 0. +"test_principal" says someFact(12) :- 3 >= 2. +"test_principal" says someFact(13) :- 3 >= 3. +"test_principal" says someFact(14) :- 3 >= 5. + +q1 = query "test_principal" says someFact(1)? +q2 = query "test_principal" says someFact(2)? +q3 = query "test_principal" says someFact(3)? +q4 = query "test_principal" says someFact(4)? +q5 = query "test_principal" says someFact(5)? +q6 = query "test_principal" says someFact(6)? +q7 = query "test_principal" says someFact(7)? +q8 = query "test_principal" says someFact(8)? +q9 = query "test_principal" says someFact(9)? +q10 = query "test_principal" says someFact(10)? +q11 = query "test_principal" says someFact(11)? +q12 = query "test_principal" says someFact(12)? +q13 = query "test_principal" says someFact(13)? +q14 = query "test_principal" says someFact(14)? diff --git a/src/ir/auth_logic/test_inputs/basic_num_comparisons.dl b/src/ir/auth_logic/test_inputs/basic_num_comparisons.dl new file mode 100644 index 000000000..a3a0d75bf --- /dev/null +++ b/src/ir/auth_logic/test_inputs/basic_num_comparisons.dl @@ -0,0 +1,84 @@ +.type DummyType <: symbol +.type Number <: number +.type Principal <: symbol +.decl grounded_dummy(dummy_param : DummyType) +.decl q1(dummy_param : DummyType) +.decl q10(dummy_param : DummyType) +.decl q11(dummy_param : DummyType) +.decl q12(dummy_param : DummyType) +.decl q13(dummy_param : DummyType) +.decl q14(dummy_param : DummyType) +.decl q2(dummy_param : DummyType) +.decl q3(dummy_param : DummyType) +.decl q4(dummy_param : DummyType) +.decl q5(dummy_param : DummyType) +.decl q6(dummy_param : DummyType) +.decl q7(dummy_param : DummyType) +.decl q8(dummy_param : DummyType) +.decl q9(dummy_param : DummyType) +.decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) +.decl says_isNumber(speaker : Principal, x : Number) +.decl says_isPrincipal(speaker : Principal, x : Principal) +.decl says_someFact(speaker : Principal, n : Number) +says_isNumber("test_principal", 7). +says_isNumber("test_principal", 9). +says_isNumber("test_principal", 6). +says_isNumber("test_principal", 13). +says_isNumber("test_principal", 4). +says_isNumber("test_principal", 12). +says_isNumber("test_principal", 2). +says_isNumber("test_principal", 999). +says_isNumber("test_principal", 8). +says_isNumber("test_principal", 10). +says_isNumber("test_principal", 0). +says_isNumber("test_principal", 5). +says_isNumber("test_principal", 1). +says_isNumber("test_principal", 3). +says_isNumber("test_principal", 47). +says_isNumber("test_principal", 42). +says_isNumber("test_principal", 14). +says_isPrincipal("test_principal", "test_principal"). +says_isNumber("test_principal", 11). +says_someFact("test_principal", 1) :- 3<5. +says_someFact("test_principal", 2) :- 3<0. +says_someFact("test_principal", 3) :- 5>0. +says_someFact("test_principal", 4) :- 3>999. +says_someFact("test_principal", 5) :- 4=4. +says_someFact("test_principal", 6) :- 47=42. +says_someFact("test_principal", 7) :- 47!=42. +says_someFact("test_principal", 8) :- 0!=0. +says_someFact("test_principal", 9) :- 3<=5. +says_someFact("test_principal", 10) :- 3<=3. +says_someFact("test_principal", 11) :- 3<=0. +says_someFact("test_principal", 12) :- 3>=2. +says_someFact("test_principal", 13) :- 3>=3. +says_someFact("test_principal", 14) :- 3>=5. +q1("dummy_var") :- says_someFact("test_principal", 1), grounded_dummy("dummy_var"). +q2("dummy_var") :- says_someFact("test_principal", 2), grounded_dummy("dummy_var"). +q3("dummy_var") :- says_someFact("test_principal", 3), grounded_dummy("dummy_var"). +q4("dummy_var") :- says_someFact("test_principal", 4), grounded_dummy("dummy_var"). +q5("dummy_var") :- says_someFact("test_principal", 5), grounded_dummy("dummy_var"). +q6("dummy_var") :- says_someFact("test_principal", 6), grounded_dummy("dummy_var"). +q7("dummy_var") :- says_someFact("test_principal", 7), grounded_dummy("dummy_var"). +q8("dummy_var") :- says_someFact("test_principal", 8), grounded_dummy("dummy_var"). +q9("dummy_var") :- says_someFact("test_principal", 9), grounded_dummy("dummy_var"). +q10("dummy_var") :- says_someFact("test_principal", 10), grounded_dummy("dummy_var"). +q11("dummy_var") :- says_someFact("test_principal", 11), grounded_dummy("dummy_var"). +q12("dummy_var") :- says_someFact("test_principal", 12), grounded_dummy("dummy_var"). +q13("dummy_var") :- says_someFact("test_principal", 13), grounded_dummy("dummy_var"). +q14("dummy_var") :- says_someFact("test_principal", 14), grounded_dummy("dummy_var"). +grounded_dummy("dummy_var"). +.output q1 +.output q2 +.output q3 +.output q4 +.output q5 +.output q6 +.output q7 +.output q8 +.output q9 +.output q10 +.output q11 +.output q12 +.output q13 +.output q14 diff --git a/src/ir/auth_logic/test_inputs/basic_num_comparisons.queries b/src/ir/auth_logic/test_inputs/basic_num_comparisons.queries new file mode 100644 index 000000000..ef132d673 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/basic_num_comparisons.queries @@ -0,0 +1,14 @@ +q1.csv, true +q10.csv, true +q11.csv, false +q12.csv, true +q13.csv, true +q14.csv, false +q2.csv, false +q3.csv, true +q4.csv, false +q5.csv, true +q6.csv, false +q7.csv, true +q8.csv, false +q9.csv, true \ No newline at end of file diff --git a/src/ir/auth_logic/test_inputs/canActAs.auth b/src/ir/auth_logic/test_inputs/canActAs.auth new file mode 100644 index 000000000..b71dcbc76 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/canActAs.auth @@ -0,0 +1,54 @@ +.decl attribute hasCertification(subject : Symbol) +.decl attribute hasAttribute(attr_name : Symbol) +.decl groundedPrin(p : Principal) + +// soupExpert is a Principal that represents a role. +// prin1 specifies a policy for when another Principal can occupy +// this role. +"prin1" says "prin2" canActAs "soupExpert" :- + "prin2" hasCertification("soupsmithing"). + +// prin1 grants soupExperts the privilege to grant any other object +// the ability to occupy the "soup" role. +"prin1" says "prin2" canSay "chickenSoup" canActAs "soup" :- + "prin2" canActAs "soupExpert", + groundedPrin("chickenSoup"), groundedPrin("prin2"). + +// Note that, canSay does not act as a delegation on its own. It merely +// passes *properties* from one Principal to the other. So the following +// commented out line would not cause prin1 to delegate to Principals +// that act as soupExperts: +// +// "prin1" says "soupExpert" canSay "chickenSoup" canActAs "soup" :- +// grounded("chickenSoup"). + +// prin1 delegates to certificate authority to produce the needed +// credentials to act as a soup expert. +"prin1" says "nationalInstituteOfSoupChefs" + canSay "prin2" hasCertification("soupsmithing") :- + groundedPrin("prin2"). + +// prin1 specifies attributes of soup (that are applied +// to any Principal that occupies the soup role). +"prin1" says "soup" hasAttribute("liquid"). +"prin1" says "soup" hasAttribute("aSubstantialMeal"). + +// prin2, a credentialed soup expert allows chickenSoup to be +// considered soup. +"nationalInstituteOfSoupChefs" says + "prin2" hasCertification("soupsmithing"). +"prin2" says "chickenSoup" canActAs "soup". + +// prin3 does not have the needed credential in soupsmithing, +// so this spurious claim is ignored by prin1 +//"prin3" says "ketchup" canActAs "soup". + +// This is boilerplate that we can't avoid: +"prin1" says groundedPrin("chickenSoup"). +"prin1" says groundedPrin("ketchup"). +"prin1" says groundedPrin("prin2"). +"prin1" says groundedPrin("prin3"). + +q_chicken = query "prin1" says "chickenSoup" hasAttribute("aSubstantialMeal")? +q_ketchup = query "prin1" says "ketchup" hasAttribute("aSubstantialMeal")? + diff --git a/src/ir/auth_logic/test_inputs/canActAs.dl b/src/ir/auth_logic/test_inputs/canActAs.dl new file mode 100644 index 000000000..289bc2e93 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/canActAs.dl @@ -0,0 +1,129 @@ +.type DummyType <: symbol +.type Number <: number +.type Principal <: symbol +.type Symbol <: symbol +.decl grounded_dummy(dummy_param : DummyType) +.decl q_chicken(dummy_param : DummyType) +.decl q_ketchup(dummy_param : DummyType) +.decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) +.decl says_canSay_canActAs(speaker : Principal, delegatee1 : Principal, p1 : Principal, p2 : Principal) +.decl says_canSay_hasCertification(speaker : Principal, delegatee1 : Principal, attribute_prin : Principal, subject : Symbol) +.decl says_groundedPrin(speaker : Principal, p : Principal) +.decl says_hasAttribute(speaker : Principal, attribute_prin : Principal, attr_name : Symbol) +.decl says_hasCertification(speaker : Principal, attribute_prin : Principal, subject : Symbol) +.decl says_isNumber(speaker : Principal, x : Number) +.decl says_isPrincipal(speaker : Principal, x : Principal) +.decl says_isSymbol(speaker : Principal, x : Symbol) +says_isPrincipal("nationalInstituteOfSoupChefs", "nationalInstituteOfSoupChefs"). +says_isPrincipal("nationalInstituteOfSoupChefs", "chickenSoup"). +says_isPrincipal("nationalInstituteOfSoupChefs", "prin2"). +says_isPrincipal("nationalInstituteOfSoupChefs", "prin3"). +says_isSymbol("nationalInstituteOfSoupChefs", "soupsmithing"). +says_isSymbol("nationalInstituteOfSoupChefs", "aSubstantialMeal"). +says_isPrincipal("nationalInstituteOfSoupChefs", "soup"). +says_isPrincipal("nationalInstituteOfSoupChefs", "prin1"). +says_isPrincipal("nationalInstituteOfSoupChefs", "ketchup"). +says_isPrincipal("nationalInstituteOfSoupChefs", "soupExpert"). +says_isSymbol("nationalInstituteOfSoupChefs", "liquid"). +says_isPrincipal("chickenSoup", "nationalInstituteOfSoupChefs"). +says_isPrincipal("chickenSoup", "chickenSoup"). +says_isPrincipal("chickenSoup", "prin2"). +says_isPrincipal("chickenSoup", "prin3"). +says_isSymbol("chickenSoup", "soupsmithing"). +says_isSymbol("chickenSoup", "aSubstantialMeal"). +says_isPrincipal("chickenSoup", "soup"). +says_isPrincipal("chickenSoup", "prin1"). +says_isPrincipal("chickenSoup", "ketchup"). +says_isPrincipal("chickenSoup", "soupExpert"). +says_isSymbol("chickenSoup", "liquid"). +says_isPrincipal("prin2", "nationalInstituteOfSoupChefs"). +says_isPrincipal("prin2", "chickenSoup"). +says_isPrincipal("prin2", "prin2"). +says_isPrincipal("prin2", "prin3"). +says_isSymbol("prin2", "soupsmithing"). +says_isSymbol("prin2", "aSubstantialMeal"). +says_isPrincipal("prin2", "soup"). +says_isPrincipal("prin2", "prin1"). +says_isPrincipal("prin2", "ketchup"). +says_isPrincipal("prin2", "soupExpert"). +says_isSymbol("prin2", "liquid"). +says_isPrincipal("prin3", "nationalInstituteOfSoupChefs"). +says_isPrincipal("prin3", "chickenSoup"). +says_isPrincipal("prin3", "prin2"). +says_isPrincipal("prin3", "prin3"). +says_isSymbol("prin3", "soupsmithing"). +says_isSymbol("prin3", "aSubstantialMeal"). +says_isPrincipal("prin3", "soup"). +says_isPrincipal("prin3", "prin1"). +says_isPrincipal("prin3", "ketchup"). +says_isPrincipal("prin3", "soupExpert"). +says_isSymbol("prin3", "liquid"). +says_isPrincipal("soup", "nationalInstituteOfSoupChefs"). +says_isPrincipal("soup", "chickenSoup"). +says_isPrincipal("soup", "prin2"). +says_isPrincipal("soup", "prin3"). +says_isSymbol("soup", "soupsmithing"). +says_isSymbol("soup", "aSubstantialMeal"). +says_isPrincipal("soup", "soup"). +says_isPrincipal("soup", "prin1"). +says_isPrincipal("soup", "ketchup"). +says_isPrincipal("soup", "soupExpert"). +says_isSymbol("soup", "liquid"). +says_isPrincipal("prin1", "nationalInstituteOfSoupChefs"). +says_isPrincipal("prin1", "chickenSoup"). +says_isPrincipal("prin1", "prin2"). +says_isPrincipal("prin1", "prin3"). +says_isSymbol("prin1", "soupsmithing"). +says_isSymbol("prin1", "aSubstantialMeal"). +says_isPrincipal("prin1", "soup"). +says_isPrincipal("prin1", "prin1"). +says_isPrincipal("prin1", "ketchup"). +says_isPrincipal("prin1", "soupExpert"). +says_isSymbol("prin1", "liquid"). +says_isPrincipal("ketchup", "nationalInstituteOfSoupChefs"). +says_isPrincipal("ketchup", "chickenSoup"). +says_isPrincipal("ketchup", "prin2"). +says_isPrincipal("ketchup", "prin3"). +says_isSymbol("ketchup", "soupsmithing"). +says_isSymbol("ketchup", "aSubstantialMeal"). +says_isPrincipal("ketchup", "soup"). +says_isPrincipal("ketchup", "prin1"). +says_isPrincipal("ketchup", "ketchup"). +says_isPrincipal("ketchup", "soupExpert"). +says_isPrincipal("soupExpert", "nationalInstituteOfSoupChefs"). +says_isPrincipal("soupExpert", "chickenSoup"). +says_isPrincipal("soupExpert", "prin2"). +says_isPrincipal("soupExpert", "prin3"). +says_isSymbol("soupExpert", "soupsmithing"). +says_isSymbol("soupExpert", "aSubstantialMeal"). +says_isPrincipal("soupExpert", "soup"). +says_isPrincipal("soupExpert", "prin1"). +says_isPrincipal("soupExpert", "ketchup"). +says_isPrincipal("soupExpert", "soupExpert"). +says_isSymbol("soupExpert", "liquid"). +says_isSymbol("ketchup", "liquid"). +says_canActAs("prin1", "chickenSoup", "soup") :- says_canActAs(x__5, "chickenSoup", "soup"), says_canSay_canActAs("prin1", x__5, "chickenSoup", "soup"). +says_canActAs("prin1", "prin2", "soupExpert") :- says_hasCertification("prin1", "prin2", "soupsmithing"). +says_canActAs("prin1", x__2, "soupExpert") :- says_canActAs("prin1", x__2, "prin2"), says_canActAs("prin1", "prin2", "soupExpert"). +says_canActAs("prin1", x__4, "soup") :- says_canActAs("prin1", x__4, "chickenSoup"), says_canActAs("prin1", "chickenSoup", "soup"). +says_canSay_canActAs("prin1", "prin2", "chickenSoup", "soup") :- says_canActAs("prin1", "prin2", "soupExpert"), says_groundedPrin("prin1", "chickenSoup"), says_groundedPrin("prin1", "prin2"). +says_canSay_hasCertification("prin1", "nationalInstituteOfSoupChefs", "prin2", "soupsmithing") :- says_groundedPrin("prin1", "prin2"). +says_hasAttribute("prin1", x__8, "liquid") :- says_canActAs("prin1", x__8, "soup"), says_hasAttribute("prin1", "soup", "liquid"). +says_hasAttribute("prin1", "soup", "liquid"). +says_hasAttribute("prin1", x__9, "aSubstantialMeal") :- says_canActAs("prin1", x__9, "soup"), says_hasAttribute("prin1", "soup", "aSubstantialMeal"). +says_hasAttribute("prin1", "soup", "aSubstantialMeal"). +says_hasCertification("nationalInstituteOfSoupChefs", x__10, "soupsmithing") :- says_canActAs("nationalInstituteOfSoupChefs", x__10, "prin2"), says_hasCertification("nationalInstituteOfSoupChefs", "prin2", "soupsmithing"). +says_hasCertification("nationalInstituteOfSoupChefs", "prin2", "soupsmithing"). +says_hasCertification("prin1", "prin2", "soupsmithing") :- says_hasCertification(x__7, "prin2", "soupsmithing"), says_canSay_hasCertification("prin1", x__7, "prin2", "soupsmithing"). +says_hasCertification("prin1", x__6, "soupsmithing") :- says_canActAs("prin1", x__6, "prin2"), says_hasCertification("prin1", "prin2", "soupsmithing"). +says_canActAs("prin2", x__11, "soup") :- says_canActAs("prin2", x__11, "chickenSoup"), says_canActAs("prin2", "chickenSoup", "soup"). +says_canActAs("prin2", "chickenSoup", "soup"). +says_groundedPrin("prin1", "chickenSoup"). +says_groundedPrin("prin1", "ketchup"). +says_groundedPrin("prin1", "prin2"). +says_groundedPrin("prin1", "prin3"). +q_chicken("dummy_var") :- says_hasAttribute("prin1", "chickenSoup", "aSubstantialMeal"), grounded_dummy("dummy_var"). +q_ketchup("dummy_var") :- says_hasAttribute("prin1", "ketchup", "aSubstantialMeal"), grounded_dummy("dummy_var"). +grounded_dummy("dummy_var"). +.output q_chicken +.output q_ketchup diff --git a/src/ir/auth_logic/test_inputs/canActAs.queries b/src/ir/auth_logic/test_inputs/canActAs.queries new file mode 100644 index 000000000..65becc7dd --- /dev/null +++ b/src/ir/auth_logic/test_inputs/canActAs.queries @@ -0,0 +1,2 @@ +q_chicken.csv, true +q_ketchup.csv, false diff --git a/src/ir/auth_logic/test_inputs/comparisons_with_delegation.auth b/src/ir/auth_logic/test_inputs/comparisons_with_delegation.auth new file mode 100644 index 000000000..531069ce4 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/comparisons_with_delegation.auth @@ -0,0 +1,29 @@ +.decl expected_hash(object : Object, hash : Sha256Hash) +.decl currentTimeIs(real_time : Number) + + +"EndorsementFile_OakFunctionsLoader" says { + expected_hash("OakFunctionsLoader", "sha256:cafed00d") :- + currentTimeIs(real_time), real_time > 42, real_time < 31337. + "VerifierSystemClock" canSay currentTimeIs(real_time). +} + +// This one has expired +"EndorsementFile_OakFunctionsLoader" says { + expected_hash("OakFunctionsLoader", "sha256:deadbeef") :- + currentTimeIs(real_time), real_time > 42, real_time < 1337. +} + +"VerifierSystemClock" says { + currentTimeIs(1776). +} + +"Verifier_OakFunctionsLoader" says { + "EndorsementFile_OakFunctionsLoader" canSay + expected_hash("OakFunctionsLoader", any_hash). +} + +q1 = query "Verifier_OakFunctionsLoader" says + expected_hash("OakFunctionsLoader", "sha256:cafed00d")? +q2 = query "Verifier_OakFunctionsLoader" says + expected_hash("OakFunctionsLoader", "sha256:deadbeef")? diff --git a/src/ir/auth_logic/test_inputs/comparisons_with_delegation.dl b/src/ir/auth_logic/test_inputs/comparisons_with_delegation.dl new file mode 100644 index 000000000..1f7a0ef6f --- /dev/null +++ b/src/ir/auth_logic/test_inputs/comparisons_with_delegation.dl @@ -0,0 +1,59 @@ +.type DummyType <: symbol +.type Number <: number +.type Object <: symbol +.type Principal <: symbol +.type Sha256Hash <: symbol +.decl grounded_dummy(dummy_param : DummyType) +.decl q1(dummy_param : DummyType) +.decl q2(dummy_param : DummyType) +.decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) +.decl says_canSay_currentTimeIs(speaker : Principal, delegatee1 : Principal, real_time : Number) +.decl says_canSay_expected_hash(speaker : Principal, delegatee1 : Principal, object : Object, hash : Sha256Hash) +.decl says_currentTimeIs(speaker : Principal, real_time : Number) +.decl says_expected_hash(speaker : Principal, object : Object, hash : Sha256Hash) +.decl says_isNumber(speaker : Principal, x : Number) +.decl says_isObject(speaker : Principal, x : Object) +.decl says_isPrincipal(speaker : Principal, x : Principal) +.decl says_isSha256Hash(speaker : Principal, x : Sha256Hash) +says_isPrincipal("VerifierSystemClock", "VerifierSystemClock"). +says_isSha256Hash("VerifierSystemClock", "sha256:deadbeef"). +says_isNumber("VerifierSystemClock", 42). +says_isSha256Hash("VerifierSystemClock", "sha256:cafed00d"). +says_isPrincipal("VerifierSystemClock", "Verifier_OakFunctionsLoader"). +says_isNumber("VerifierSystemClock", 31337). +says_isNumber("VerifierSystemClock", 1776). +says_isObject("VerifierSystemClock", "OakFunctionsLoader"). +says_isPrincipal("VerifierSystemClock", "EndorsementFile_OakFunctionsLoader"). +says_isNumber("VerifierSystemClock", 1337). +says_isPrincipal("Verifier_OakFunctionsLoader", "VerifierSystemClock"). +says_isSha256Hash("Verifier_OakFunctionsLoader", "sha256:deadbeef"). +says_isNumber("Verifier_OakFunctionsLoader", 42). +says_isSha256Hash("Verifier_OakFunctionsLoader", "sha256:cafed00d"). +says_isPrincipal("Verifier_OakFunctionsLoader", "Verifier_OakFunctionsLoader"). +says_isNumber("Verifier_OakFunctionsLoader", 31337). +says_isNumber("Verifier_OakFunctionsLoader", 1776). +says_isObject("Verifier_OakFunctionsLoader", "OakFunctionsLoader"). +says_isPrincipal("Verifier_OakFunctionsLoader", "EndorsementFile_OakFunctionsLoader"). +says_isNumber("Verifier_OakFunctionsLoader", 1337). +says_isPrincipal("EndorsementFile_OakFunctionsLoader", "VerifierSystemClock"). +says_isSha256Hash("EndorsementFile_OakFunctionsLoader", "sha256:deadbeef"). +says_isNumber("EndorsementFile_OakFunctionsLoader", 42). +says_isSha256Hash("EndorsementFile_OakFunctionsLoader", "sha256:cafed00d"). +says_isPrincipal("EndorsementFile_OakFunctionsLoader", "Verifier_OakFunctionsLoader"). +says_isNumber("EndorsementFile_OakFunctionsLoader", 31337). +says_isNumber("EndorsementFile_OakFunctionsLoader", 1776). +says_isObject("EndorsementFile_OakFunctionsLoader", "OakFunctionsLoader"). +says_isPrincipal("EndorsementFile_OakFunctionsLoader", "EndorsementFile_OakFunctionsLoader"). +says_isNumber("EndorsementFile_OakFunctionsLoader", 1337). +says_expected_hash("EndorsementFile_OakFunctionsLoader", "OakFunctionsLoader", "sha256:cafed00d") :- says_currentTimeIs("EndorsementFile_OakFunctionsLoader", real_time), real_time>42, real_time<31337. +says_currentTimeIs("EndorsementFile_OakFunctionsLoader", real_time) :- says_currentTimeIs(x__1, real_time), says_canSay_currentTimeIs("EndorsementFile_OakFunctionsLoader", x__1, real_time). +says_canSay_currentTimeIs("EndorsementFile_OakFunctionsLoader", "VerifierSystemClock", real_time) :- says_isNumber("EndorsementFile_OakFunctionsLoader", real_time). +says_expected_hash("EndorsementFile_OakFunctionsLoader", "OakFunctionsLoader", "sha256:deadbeef") :- says_currentTimeIs("EndorsementFile_OakFunctionsLoader", real_time), real_time>42, real_time<1337. +says_currentTimeIs("VerifierSystemClock", 1776). +says_expected_hash("Verifier_OakFunctionsLoader", "OakFunctionsLoader", any_hash) :- says_expected_hash(x__2, "OakFunctionsLoader", any_hash), says_canSay_expected_hash("Verifier_OakFunctionsLoader", x__2, "OakFunctionsLoader", any_hash). +says_canSay_expected_hash("Verifier_OakFunctionsLoader", "EndorsementFile_OakFunctionsLoader", "OakFunctionsLoader", any_hash) :- says_isSha256Hash("Verifier_OakFunctionsLoader", any_hash). +q1("dummy_var") :- says_expected_hash("Verifier_OakFunctionsLoader", "OakFunctionsLoader", "sha256:cafed00d"), grounded_dummy("dummy_var"). +q2("dummy_var") :- says_expected_hash("Verifier_OakFunctionsLoader", "OakFunctionsLoader", "sha256:deadbeef"), grounded_dummy("dummy_var"). +grounded_dummy("dummy_var"). +.output q1 +.output q2 \ No newline at end of file diff --git a/src/ir/auth_logic/test_inputs/comparisons_with_delegation.queries b/src/ir/auth_logic/test_inputs/comparisons_with_delegation.queries new file mode 100644 index 000000000..445aab4cc --- /dev/null +++ b/src/ir/auth_logic/test_inputs/comparisons_with_delegation.queries @@ -0,0 +1,2 @@ +q1.csv, true +q2.csv, false diff --git a/src/ir/auth_logic/test_inputs/conditions.auth b/src/ir/auth_logic/test_inputs/conditions.auth new file mode 100644 index 000000000..3341da29b --- /dev/null +++ b/src/ir/auth_logic/test_inputs/conditions.auth @@ -0,0 +1,13 @@ +.decl fact1(x : Symbol) +.decl fact2(x : Symbol) +.decl cond1(x : Symbol) +.decl cond2(x : Symbol, y : Symbol) + +"prin1" says fact1(thing_x) :- cond1(thing_x). +"prin1" says fact2(thing_x) :- cond1(thing_x), cond2(thing_x, "bar"). +"prin1" says cond1("foo"). +"prin2" says cond1("foo"). + +q_prin1_fact1 = query "prin1" says fact1("foo")? +q_prin1_fact2 = query "prin1" says fact2("foo")? +q_prin2_fact1 = query "prin2" says fact1("foo")? \ No newline at end of file diff --git a/src/ir/auth_logic/test_inputs/conditions.dl b/src/ir/auth_logic/test_inputs/conditions.dl new file mode 100644 index 000000000..3528d1488 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/conditions.dl @@ -0,0 +1,35 @@ +.type DummyType <: symbol +.type Number <: number +.type Principal <: symbol +.type Symbol <: symbol +.decl grounded_dummy(dummy_param : DummyType) +.decl q_prin1_fact1(dummy_param : DummyType) +.decl q_prin1_fact2(dummy_param : DummyType) +.decl q_prin2_fact1(dummy_param : DummyType) +.decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) +.decl says_cond1(speaker : Principal, x : Symbol) +.decl says_cond2(speaker : Principal, x : Symbol, y : Symbol) +.decl says_fact1(speaker : Principal, x : Symbol) +.decl says_fact2(speaker : Principal, x : Symbol) +.decl says_isNumber(speaker : Principal, x : Number) +.decl says_isPrincipal(speaker : Principal, x : Principal) +.decl says_isSymbol(speaker : Principal, x : Symbol) +says_isPrincipal("prin2", "prin2"). +says_isSymbol("prin2", "foo"). +says_isPrincipal("prin2", "prin1"). +says_isSymbol("prin2", "bar"). +says_isPrincipal("prin1", "prin2"). +says_isSymbol("prin1", "foo"). +says_isPrincipal("prin1", "prin1"). +says_isSymbol("prin1", "bar"). +says_fact1("prin1", thing_x) :- says_isSymbol("prin1", thing_x), says_cond1("prin1", thing_x). +says_fact2("prin1", thing_x) :- says_isSymbol("prin1", thing_x), says_cond1("prin1", thing_x), says_cond2("prin1", thing_x, "bar"). +says_cond1("prin1", "foo"). +says_cond1("prin2", "foo"). +q_prin1_fact1("dummy_var") :- says_fact1("prin1", "foo"), grounded_dummy("dummy_var"). +q_prin1_fact2("dummy_var") :- says_fact2("prin1", "foo"), grounded_dummy("dummy_var"). +q_prin2_fact1("dummy_var") :- says_fact1("prin2", "foo"), grounded_dummy("dummy_var"). +grounded_dummy("dummy_var"). +.output q_prin1_fact1 +.output q_prin1_fact2 +.output q_prin2_fact1 diff --git a/src/ir/auth_logic/test_inputs/conditions.queries b/src/ir/auth_logic/test_inputs/conditions.queries new file mode 100644 index 000000000..b9f5c484e --- /dev/null +++ b/src/ir/auth_logic/test_inputs/conditions.queries @@ -0,0 +1,3 @@ +q_prin1_fact1.csv, true +q_prin1_fact2.csv, false +q_prin2_fact1.csv, false diff --git a/src/ir/auth_logic/test_inputs/delegation.auth b/src/ir/auth_logic/test_inputs/delegation.auth new file mode 100644 index 000000000..1c60936e0 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/delegation.auth @@ -0,0 +1,33 @@ +.decl unconditionallyDelegatedFact(x : Symbol) +.decl conditionallyDelegated(x : Symbol) +.decl someCondition(x : Symbol) +.decl anotherCondition(x : Symbol) +.decl undelegatedFact(x : Symbol) +.decl grounded(x : Symbol) + +// prin1 delegates to prin2 about uDF for any variable +"prin1" says "prin2" canSay unconditionallyDelegatedFact(x) :- + grounded(x). +// prin1 delegates to prin2 about cD only if prin1 believes sC +"prin1" says "prin2" canSay conditionallyDelegated(x) :- + grounded(x), someCondition(x). +// prin1 believes uF if aC, but does not delegate uF +"prin1" says undelegatedFact(x) :- anotherCondition(x). +"prin1" says grounded("someX1"). +"prin1" says grounded("someX2"). + +"prin2" says unconditionallyDelegatedFact("someX1"). +q_uncond1_t = query "prin1" says unconditionallyDelegatedFact("someX1")? +q_uncond2_f = query "prin1" says unconditionallyDelegatedFact("someX2")? + +"prin2" says someCondition("someX1"). +"prin1" says someCondition("someX2"). +"prin2" says conditionallyDelegated("someX1"). +"prin2" says conditionallyDelegated("someX2"). +q_cond1_f = query "prin1" says conditionallyDelegated("someX1")? +q_cond2_t = query "prin1" says conditionallyDelegated("someX2")? + +"prin1" says anotherCondition("someX1"). +"prin2" says anotherCondition("someX2"). +q_undel1_t = query "prin1" says undelegatedFact("someX1")? +q_undel2_f = query "prin1" says undelegatedFact("someX2")? diff --git a/src/ir/auth_logic/test_inputs/delegation.dl b/src/ir/auth_logic/test_inputs/delegation.dl new file mode 100644 index 000000000..c98a59f9d --- /dev/null +++ b/src/ir/auth_logic/test_inputs/delegation.dl @@ -0,0 +1,58 @@ +.type DummyType <: symbol +.type Number <: number +.type Principal <: symbol +.type Symbol <: symbol +.decl grounded_dummy(dummy_param : DummyType) +.decl q_cond1_f(dummy_param : DummyType) +.decl q_cond2_t(dummy_param : DummyType) +.decl q_uncond1_t(dummy_param : DummyType) +.decl q_uncond2_f(dummy_param : DummyType) +.decl q_undel1_t(dummy_param : DummyType) +.decl q_undel2_f(dummy_param : DummyType) +.decl says_anotherCondition(speaker : Principal, x : Symbol) +.decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) +.decl says_canSay_conditionallyDelegated(speaker : Principal, delegatee1 : Principal, x : Symbol) +.decl says_canSay_unconditionallyDelegatedFact(speaker : Principal, delegatee1 : Principal, x : Symbol) +.decl says_conditionallyDelegated(speaker : Principal, x : Symbol) +.decl says_grounded(speaker : Principal, x : Symbol) +.decl says_isNumber(speaker : Principal, x : Number) +.decl says_isPrincipal(speaker : Principal, x : Principal) +.decl says_isSymbol(speaker : Principal, x : Symbol) +.decl says_someCondition(speaker : Principal, x : Symbol) +.decl says_unconditionallyDelegatedFact(speaker : Principal, x : Symbol) +.decl says_undelegatedFact(speaker : Principal, x : Symbol) +says_isPrincipal("prin1", "prin1"). +says_isSymbol("prin1", "someX2"). +says_isSymbol("prin1", "someX1"). +says_isPrincipal("prin1", "prin2"). +says_isPrincipal("prin2", "prin1"). +says_isSymbol("prin2", "someX2"). +says_isSymbol("prin2", "someX1"). +says_isPrincipal("prin2", "prin2"). +says_unconditionallyDelegatedFact("prin1", x) :- says_unconditionallyDelegatedFact(x__1, x), says_canSay_unconditionallyDelegatedFact("prin1", x__1, x). +says_canSay_unconditionallyDelegatedFact("prin1", "prin2", x) :- says_isSymbol("prin1", x), says_grounded("prin1", x). +says_conditionallyDelegated("prin1", x) :- says_conditionallyDelegated(x__2, x), says_canSay_conditionallyDelegated("prin1", x__2, x). +says_canSay_conditionallyDelegated("prin1", "prin2", x) :- says_isSymbol("prin1", x), says_grounded("prin1", x), says_someCondition("prin1", x). +says_undelegatedFact("prin1", x) :- says_isSymbol("prin1", x), says_anotherCondition("prin1", x). +says_grounded("prin1", "someX1"). +says_grounded("prin1", "someX2"). +says_unconditionallyDelegatedFact("prin2", "someX1"). +says_someCondition("prin2", "someX1"). +says_someCondition("prin1", "someX2"). +says_conditionallyDelegated("prin2", "someX1"). +says_conditionallyDelegated("prin2", "someX2"). +says_anotherCondition("prin1", "someX1"). +says_anotherCondition("prin2", "someX2"). +q_uncond1_t("dummy_var") :- says_unconditionallyDelegatedFact("prin1", "someX1"), grounded_dummy("dummy_var"). +q_uncond2_f("dummy_var") :- says_unconditionallyDelegatedFact("prin1", "someX2"), grounded_dummy("dummy_var"). +q_cond1_f("dummy_var") :- says_conditionallyDelegated("prin1", "someX1"), grounded_dummy("dummy_var"). +q_cond2_t("dummy_var") :- says_conditionallyDelegated("prin1", "someX2"), grounded_dummy("dummy_var"). +q_undel1_t("dummy_var") :- says_undelegatedFact("prin1", "someX1"), grounded_dummy("dummy_var"). +q_undel2_f("dummy_var") :- says_undelegatedFact("prin1", "someX2"), grounded_dummy("dummy_var"). +grounded_dummy("dummy_var"). +.output q_uncond1_t +.output q_uncond2_f +.output q_cond1_f +.output q_cond2_t +.output q_undel1_t +.output q_undel2_f diff --git a/src/ir/auth_logic/test_inputs/delegation.queries b/src/ir/auth_logic/test_inputs/delegation.queries new file mode 100644 index 000000000..66ff328ff --- /dev/null +++ b/src/ir/auth_logic/test_inputs/delegation.queries @@ -0,0 +1,6 @@ +q_cond1_f.csv, false +q_cond2_t.csv, true +q_uncond1_t.csv, true +q_uncond2_f.csv, false +q_undel1_t.csv, true +q_undel2_f.csv, false diff --git a/src/ir/auth_logic/test_inputs/dot_in_names.auth b/src/ir/auth_logic/test_inputs/dot_in_names.auth new file mode 100644 index 000000000..b68e3bb25 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/dot_in_names.auth @@ -0,0 +1,11 @@ +.decl are(words : Words, anotherWords : Words) +.decl areConditionally(words : Words, anotherWords : Words) +.decl evenIf(words : Words) +.decl areAlso(words : Words, anotherWords : Words) + +"TheTestPrincipal" says are("names.with.dots.in.them", "prefectly.cromulent"). + +"TheTestPrincipal" says areConditionally("names.with.dots.in.them", "cromulent") :- + evenIf("dots.are.on.the.rhs"). + +"TheTest#Principal" says areAlso("names#with#hashes", "perfectly#cromulent"). diff --git a/src/ir/auth_logic/test_inputs/dot_in_names.dl b/src/ir/auth_logic/test_inputs/dot_in_names.dl new file mode 100644 index 000000000..15b825e18 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/dot_in_names.dl @@ -0,0 +1,33 @@ +.type DummyType <: symbol +.type Number <: number +.type Principal <: symbol +.type Words <: symbol +.decl grounded_dummy(dummy_param : DummyType) +.decl says_are(speaker : Principal, words : Words, anotherWords : Words) +.decl says_areAlso(speaker : Principal, words : Words, anotherWords : Words) +.decl says_areConditionally(speaker : Principal, words : Words, anotherWords : Words) +.decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) +.decl says_evenIf(speaker : Principal, words : Words) +.decl says_isNumber(speaker : Principal, x : Number) +.decl says_isPrincipal(speaker : Principal, x : Principal) +.decl says_isWords(speaker : Principal, x : Words) +says_isWords("TheTest#Principal", "prefectly.cromulent"). +says_isWords("TheTest#Principal", "names#with#hashes"). +says_isWords("TheTest#Principal", "cromulent"). +says_isPrincipal("TheTest#Principal", "TheTest#Principal"). +says_isPrincipal("TheTest#Principal", "TheTestPrincipal"). +says_isWords("TheTest#Principal", "perfectly#cromulent"). +says_isWords("TheTest#Principal", "dots.are.on.the.rhs"). +says_isWords("TheTest#Principal", "names.with.dots.in.them"). +says_isWords("TheTestPrincipal", "prefectly.cromulent"). +says_isWords("TheTestPrincipal", "names#with#hashes"). +says_isWords("TheTestPrincipal", "cromulent"). +says_isPrincipal("TheTestPrincipal", "TheTest#Principal"). +says_isPrincipal("TheTestPrincipal", "TheTestPrincipal"). +says_isWords("TheTestPrincipal", "perfectly#cromulent"). +says_isWords("TheTestPrincipal", "dots.are.on.the.rhs"). +says_isWords("TheTestPrincipal", "names.with.dots.in.them"). +says_are("TheTestPrincipal", "names.with.dots.in.them", "prefectly.cromulent"). +says_areConditionally("TheTestPrincipal", "names.with.dots.in.them", "cromulent") :- says_evenIf("TheTestPrincipal", "dots.are.on.the.rhs"). +says_areAlso("TheTest#Principal", "names#with#hashes", "perfectly#cromulent"). +grounded_dummy("dummy_var"). diff --git a/src/ir/auth_logic/test_inputs/hyphenIDs.auth b/src/ir/auth_logic/test_inputs/hyphenIDs.auth new file mode 100644 index 000000000..de5a318e0 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/hyphenIDs.auth @@ -0,0 +1,27 @@ +/* + * 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. + */ +.decl ourFavoritePublicKeyIs(k : Key) +.decl ourFavoriteTrustedBuilderIs(b : Builder) +.decl variablesInsteadOfConstantsWithHyhensAreOKToo(v : TestVariable) +"OakTeam" says { + ourFavoritePublicKeyIs( +"""-----BEGIN PUBLIC KEY----- +MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAErnyr7XY6gxXPnqRGYEpv5lDsbBeX +izVFLckaF/cbgBuzx7kfmf1qi2j+3DDOQYgISQOj9/LYt4c1cxbt+XtG4g== +-----END PUBLIC KEY-----"""). + ourFavoriteTrustedBuilderIs("https://github.com/project-oak/transparent-release"). + ourFavoriteTrustedBuilderIs("https://github.com/Attestations/GitHubHostedActions@v1"). +} \ No newline at end of file diff --git a/src/ir/auth_logic/test_inputs/hyphenIDs.dl b/src/ir/auth_logic/test_inputs/hyphenIDs.dl new file mode 100644 index 000000000..9b0304dcc --- /dev/null +++ b/src/ir/auth_logic/test_inputs/hyphenIDs.dl @@ -0,0 +1,24 @@ +.type Builder <: symbol +.type DummyType <: symbol +.type Key <: symbol +.type Number <: number +.type Principal <: symbol +.type TestVariable <: symbol +.decl grounded_dummy(dummy_param : DummyType) +.decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) +.decl says_isBuilder(speaker : Principal, x : Builder) +.decl says_isKey(speaker : Principal, x : Key) +.decl says_isNumber(speaker : Principal, x : Number) +.decl says_isPrincipal(speaker : Principal, x : Principal) +.decl says_isTestVariable(speaker : Principal, x : TestVariable) +.decl says_ourFavoritePublicKeyIs(speaker : Principal, k : Key) +.decl says_ourFavoriteTrustedBuilderIs(speaker : Principal, b : Builder) +.decl says_variablesInsteadOfConstantsWithHyhensAreOKToo(speaker : Principal, v : TestVariable) +says_isPrincipal("OakTeam", "OakTeam"). +says_isKey("OakTeam", "-----BEGIN PUBLIC KEY-----MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAErnyr7XY6gxXPnqRGYEpv5lDsbBeXizVFLckaF/cbgBuzx7kfmf1qi2j+3DDOQYgISQOj9/LYt4c1cxbt+XtG4g==-----END PUBLIC KEY-----"). +says_isBuilder("OakTeam", "https://github.com/project-oak/transparent-release"). +says_isBuilder("OakTeam", "https://github.com/Attestations/GitHubHostedActions@v1"). +says_ourFavoritePublicKeyIs("OakTeam", "-----BEGIN PUBLIC KEY-----MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAErnyr7XY6gxXPnqRGYEpv5lDsbBeXizVFLckaF/cbgBuzx7kfmf1qi2j+3DDOQYgISQOj9/LYt4c1cxbt+XtG4g==-----END PUBLIC KEY-----"). +says_ourFavoriteTrustedBuilderIs("OakTeam", "https://github.com/project-oak/transparent-release"). +says_ourFavoriteTrustedBuilderIs("OakTeam", "https://github.com/Attestations/GitHubHostedActions@v1"). +grounded_dummy("dummy_var"). \ No newline at end of file diff --git a/src/ir/auth_logic/test_inputs/multiverse_handling.auth b/src/ir/auth_logic/test_inputs/multiverse_handling.auth new file mode 100644 index 000000000..332d5ac50 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/multiverse_handling.auth @@ -0,0 +1,13 @@ +.decl expectedHash(object : Object, hash : Hash) + +"Verifier" says "CoolAppEndorsementFile" canSay + expectedHash("CoolAppBinary", expected_hash). + +"CoolAppEndorsementFile" says expectedHash("CoolAppBinary", "sha256:cafed00d"). + +test_query1_true = query "Verifier" says expectedHash("CoolAppBinary", + "sha256:cafed00d")? + +test_query2_false = query "Verifier" says expectedHash("CoolAppBinary", + "sha256:deadbeef")? + \ No newline at end of file diff --git a/src/ir/auth_logic/test_inputs/multiverse_handling.dl b/src/ir/auth_logic/test_inputs/multiverse_handling.dl new file mode 100644 index 000000000..5174b0845 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/multiverse_handling.dl @@ -0,0 +1,33 @@ +.type DummyType <: symbol +.type Hash <: symbol +.type Number <: number +.type Object <: symbol +.type Principal <: symbol +.decl grounded_dummy(dummy_param : DummyType) +.decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) +.decl says_canSay_expectedHash(speaker : Principal, delegatee1 : Principal, object : Object, hash : Hash) +.decl says_expectedHash(speaker : Principal, object : Object, hash : Hash) +.decl says_isHash(speaker : Principal, x : Hash) +.decl says_isNumber(speaker : Principal, x : Number) +.decl says_isObject(speaker : Principal, x : Object) +.decl says_isPrincipal(speaker : Principal, x : Principal) +.decl test_query1_true(dummy_param : DummyType) +.decl test_query2_false(dummy_param : DummyType) +says_isPrincipal("CoolAppEndorsementFile", "CoolAppEndorsementFile"). +says_isHash("CoolAppEndorsementFile", "sha256:cafed00d"). +says_isPrincipal("CoolAppEndorsementFile", "Verifier"). +says_isObject("CoolAppEndorsementFile", "CoolAppBinary"). +says_isHash("CoolAppEndorsementFile", "sha256:deadbeef"). +says_isPrincipal("Verifier", "CoolAppEndorsementFile"). +says_isHash("Verifier", "sha256:cafed00d"). +says_isPrincipal("Verifier", "Verifier"). +says_isObject("Verifier", "CoolAppBinary"). +says_isHash("Verifier", "sha256:deadbeef"). +says_expectedHash("Verifier", "CoolAppBinary", expected_hash) :- says_expectedHash(x__1, "CoolAppBinary", expected_hash), says_canSay_expectedHash("Verifier", x__1, "CoolAppBinary", expected_hash). +says_canSay_expectedHash("Verifier", "CoolAppEndorsementFile", "CoolAppBinary", expected_hash) :- says_isHash("Verifier", expected_hash). +says_expectedHash("CoolAppEndorsementFile", "CoolAppBinary", "sha256:cafed00d"). +test_query1_true("dummy_var") :- says_expectedHash("Verifier", "CoolAppBinary", "sha256:cafed00d"), grounded_dummy("dummy_var"). +test_query2_false("dummy_var") :- says_expectedHash("Verifier", "CoolAppBinary", "sha256:deadbeef"), grounded_dummy("dummy_var"). +grounded_dummy("dummy_var"). +.output test_query1_true +.output test_query2_false diff --git a/src/ir/auth_logic/test_inputs/multiverse_handling.queries b/src/ir/auth_logic/test_inputs/multiverse_handling.queries new file mode 100644 index 000000000..ec247c986 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/multiverse_handling.queries @@ -0,0 +1,2 @@ +test_query1_true.csv, true +test_query2_false.csv, false \ No newline at end of file diff --git a/src/ir/auth_logic/test_inputs/negation.auth b/src/ir/auth_logic/test_inputs/negation.auth new file mode 100644 index 000000000..a638b0ac2 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/negation.auth @@ -0,0 +1,15 @@ +.decl foo(x : Symbol) +.decl bar(x : Symbol) +.decl baz(x : Symbol) + +"TestPrin" says foo("x") :- !bar("x"). +"TestPrin" says foo("y") :- !bar("y"). +"TestPrin" says baz("x") :- bar("x"). +"TestPrin" says bar("y"). + +// yes +q1 = query "TestPrin" says foo("x")? +// no +q2 = query "TestPrin" says baz("x")? +// no +q3 = query "TestPrin" says foo("y")? diff --git a/src/ir/auth_logic/test_inputs/negation.dl b/src/ir/auth_logic/test_inputs/negation.dl new file mode 100644 index 000000000..49dc52998 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/negation.dl @@ -0,0 +1,29 @@ +.type DummyType <: symbol +.type Number <: number +.type Principal <: symbol +.type Symbol <: symbol +.decl grounded_dummy(dummy_param : DummyType) +.decl q1(dummy_param : DummyType) +.decl q2(dummy_param : DummyType) +.decl q3(dummy_param : DummyType) +.decl says_bar(speaker : Principal, x : Symbol) +.decl says_baz(speaker : Principal, x : Symbol) +.decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) +.decl says_foo(speaker : Principal, x : Symbol) +.decl says_isNumber(speaker : Principal, x : Number) +.decl says_isPrincipal(speaker : Principal, x : Principal) +.decl says_isSymbol(speaker : Principal, x : Symbol) +says_isPrincipal("TestPrin", "TestPrin"). +says_isSymbol("TestPrin", "x"). +says_isSymbol("TestPrin", "y"). +says_foo("TestPrin", "x") :- !says_bar("TestPrin", "x"). +says_foo("TestPrin", "y") :- !says_bar("TestPrin", "y"). +says_baz("TestPrin", "x") :- says_bar("TestPrin", "x"). +says_bar("TestPrin", "y"). +q1("dummy_var") :- says_foo("TestPrin", "x"), grounded_dummy("dummy_var"). +q2("dummy_var") :- says_baz("TestPrin", "x"), grounded_dummy("dummy_var"). +q3("dummy_var") :- says_foo("TestPrin", "y"), grounded_dummy("dummy_var"). +grounded_dummy("dummy_var"). +.output q1 +.output q2 +.output q3 diff --git a/src/ir/auth_logic/test_inputs/negation.queries b/src/ir/auth_logic/test_inputs/negation.queries new file mode 100644 index 000000000..b63e56f67 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/negation.queries @@ -0,0 +1,3 @@ +q1.csv, true +q2.csv, false +q3.csv, false diff --git a/src/ir/auth_logic/test_inputs/num_strings_in_names.auth b/src/ir/auth_logic/test_inputs/num_strings_in_names.auth new file mode 100644 index 000000000..272f94e70 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/num_strings_in_names.auth @@ -0,0 +1,6 @@ +.decl numbersAre(words : Words) +.decl semicolonsAre(words : Words) + +"123" says numbersAre("perfectlyFinePrincipalNames"). +"sha256:deadbeef" says semicolonsAre("alsoFineNames"). + diff --git a/src/ir/auth_logic/test_inputs/num_strings_in_names.dl b/src/ir/auth_logic/test_inputs/num_strings_in_names.dl new file mode 100644 index 000000000..f445d7804 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/num_strings_in_names.dl @@ -0,0 +1,22 @@ +.type DummyType <: symbol +.type Number <: number +.type Principal <: symbol +.type Words <: symbol +.decl grounded_dummy(dummy_param : DummyType) +.decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) +.decl says_isNumber(speaker : Principal, x : Number) +.decl says_isPrincipal(speaker : Principal, x : Principal) +.decl says_isWords(speaker : Principal, x : Words) +.decl says_numbersAre(speaker : Principal, words : Words) +.decl says_semicolonsAre(speaker : Principal, words : Words) +says_isPrincipal("123", "123"). +says_isWords("123", "perfectlyFinePrincipalNames"). +says_isPrincipal("123", "sha256:deadbeef"). +says_isWords("123", "alsoFineNames"). +says_isPrincipal("sha256:deadbeef", "123"). +says_isWords("sha256:deadbeef", "perfectlyFinePrincipalNames"). +says_isPrincipal("sha256:deadbeef", "sha256:deadbeef"). +says_isWords("sha256:deadbeef", "alsoFineNames"). +says_numbersAre("123", "perfectlyFinePrincipalNames"). +says_semicolonsAre("sha256:deadbeef", "alsoFineNames"). +grounded_dummy("dummy_var"). diff --git a/src/ir/auth_logic/test_inputs/test_authlogic.sh b/src/ir/auth_logic/test_inputs/test_authlogic.sh new file mode 100755 index 000000000..b8058ba0e --- /dev/null +++ b/src/ir/auth_logic/test_inputs/test_authlogic.sh @@ -0,0 +1,85 @@ +#!/bin/bash +# +# 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. +# +#------------------------------------------------------------------------------- + +function printUsageAndExit() { + echo "Usage: " + echo " test_authlogic.sh \ " + echo " " + exit 1 +} + +CMD_ARG=$1 +AUTH_LOGIC_FILE_ARG=$2 +EXPECTED_DATALOG_FILE=$3 +TEST_QUERIES=${4:-0} +EXPECTED_QUERIES_FILE=${5:-0} +OUTPUT_SOUFFLE_FILE_ARG=$(mktemp) +OUTPUT_QUERY_DIR_ARG=$(mktemp -d) + +#Generates datalog file for given authorization logic +QUERY_TEST_RESULT=1 +$CMD_ARG --policy_rules=$AUTH_LOGIC_FILE_ARG --datalog_file=$OUTPUT_SOUFFLE_FILE_ARG --skip_declarations=true + +if [ -z "$SOUFFLE_BIN" ] +then + echo "Set SOUFFLE_BIN" + exit 1 +else + echo $SOUFFLE_BIN +fi + +#Populates queries in .csv +PATH=$PATH:third_party/mcpp +$SOUFFLE_BIN $OUTPUT_SOUFFLE_FILE_ARG -D $OUTPUT_QUERY_DIR_ARG/ + +ROOT_DIR=$TEST_SRCDIR/$TEST_WORKSPACE/third_party/raksha/src/ir/auth_logic + +diff <(sort $OUTPUT_SOUFFLE_FILE_ARG) <(sort $EXPECTED_DATALOG_FILE) + +CMD_RESULT=$? + +if [ ${TEST_QUERIES} -eq 1 ]; then + while read line; do + arr=(${line//","/ }) + if [ -s $OUTPUT_QUERY_DIR_ARG/${arr[0]} ]; then + if [ ${arr[1]} == "true" ]; then + QUERY_TEST_RESULT=1 + else + echo "query mismatch" + exit 1; + fi + else + if [ ${arr[1]} == "true" ]; then + echo "query mismatch" + exit 1 + else + QUERY_TEST_RESULT=1 + fi + fi + + done < $EXPECTED_QUERIES_FILE +else + echo "No need to test queries" +fi + +if ([ ${CMD_RESULT} -eq 0 ] && [ ${QUERY_TEST_RESULT} -eq 1 ]); then + exit 0; +else + echo "Expected datalog and generated datalog are different!" + exit 1 +fi diff --git a/src/ir/auth_logic/test_inputs/test_decl_skip.auth b/src/ir/auth_logic/test_inputs/test_decl_skip.auth new file mode 100644 index 000000000..c914bce81 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/test_decl_skip.auth @@ -0,0 +1,6 @@ +.decl attribute isRelevantFor(subject : Symbol) +.decl thisUnitTest(factName : Symbol) + +"TheTestPrincipal" says "thisOtherThing" isRelevantFor("JustAUnitTest") :- + thisUnitTest("isRunning"). + \ No newline at end of file diff --git a/src/ir/auth_logic/test_inputs/test_decl_skip.dl b/src/ir/auth_logic/test_inputs/test_decl_skip.dl new file mode 100644 index 000000000..79405240b --- /dev/null +++ b/src/ir/auth_logic/test_inputs/test_decl_skip.dl @@ -0,0 +1,22 @@ +.type DummyType <: symbol +.type Number <: number +.type Principal <: symbol +.type Symbol <: symbol +.decl grounded_dummy(dummy_param : DummyType) +.decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) +.decl says_isNumber(speaker : Principal, x : Number) +.decl says_isPrincipal(speaker : Principal, x : Principal) +.decl says_isRelevantFor(speaker : Principal, attribute_prin : Principal, subject : Symbol) +.decl says_isSymbol(speaker : Principal, x : Symbol) +.decl says_thisUnitTest(speaker : Principal, factName : Symbol) +says_isPrincipal("TheTestPrincipal", "TheTestPrincipal"). +says_isSymbol("TheTestPrincipal", "JustAUnitTest"). +says_isPrincipal("TheTestPrincipal", "thisOtherThing"). +says_isSymbol("TheTestPrincipal", "isRunning"). +says_isPrincipal("thisOtherThing", "TheTestPrincipal"). +says_isSymbol("thisOtherThing", "JustAUnitTest"). +says_isPrincipal("thisOtherThing", "thisOtherThing"). +says_isSymbol("thisOtherThing", "isRunning"). +says_isRelevantFor("TheTestPrincipal", x__1, "JustAUnitTest") :- says_canActAs("TheTestPrincipal", x__1, "thisOtherThing"), says_isRelevantFor("TheTestPrincipal", "thisOtherThing", "JustAUnitTest"). +says_isRelevantFor("TheTestPrincipal", "thisOtherThing", "JustAUnitTest") :- says_thisUnitTest("TheTestPrincipal", "isRunning"). +grounded_dummy("dummy_var"). diff --git a/src/ir/auth_logic/test_inputs/type_declarations.auth b/src/ir/auth_logic/test_inputs/type_declarations.auth new file mode 100644 index 000000000..ed78bb0ef --- /dev/null +++ b/src/ir/auth_logic/test_inputs/type_declarations.auth @@ -0,0 +1,7 @@ +.decl someFact(x : CustomType) +.decl someOtherFact(x : CustomType, y : Number) +.decl thirdFact(p : Principal) + +"TestPrincipal" says someFact("some_argument"). +"TestPrincipal" says someOtherFact("abcde", "three"). +"TestPrincipal" says thirdFact("OtherPrincipal"). diff --git a/src/ir/auth_logic/test_inputs/type_declarations.dl b/src/ir/auth_logic/test_inputs/type_declarations.dl new file mode 100644 index 000000000..6afd4c200 --- /dev/null +++ b/src/ir/auth_logic/test_inputs/type_declarations.dl @@ -0,0 +1,26 @@ +.type CustomType <: symbol +.type DummyType <: symbol +.type Number <: number +.type Principal <: symbol +.decl grounded_dummy(dummy_param : DummyType) +.decl says_canActAs(speaker : Principal, p1 : Principal, p2 : Principal) +.decl says_isCustomType(speaker : Principal, x : CustomType) +.decl says_isNumber(speaker : Principal, x : Number) +.decl says_isPrincipal(speaker : Principal, x : Principal) +.decl says_someFact(speaker : Principal, x : CustomType) +.decl says_someOtherFact(speaker : Principal, x : CustomType, y : Number) +.decl says_thirdFact(speaker : Principal, p : Principal) +says_isPrincipal("TestPrincipal", "TestPrincipal"). +says_isCustomType("TestPrincipal", "abcde"). +says_isCustomType("TestPrincipal", "some_argument"). +says_isNumber("TestPrincipal", "three"). +says_isPrincipal("TestPrincipal", "OtherPrincipal"). +says_isPrincipal("OtherPrincipal", "TestPrincipal"). +says_isCustomType("OtherPrincipal", "abcde"). +says_isCustomType("OtherPrincipal", "some_argument"). +says_isNumber("OtherPrincipal", "three"). +says_isPrincipal("OtherPrincipal", "OtherPrincipal"). +says_someFact("TestPrincipal", "some_argument"). +says_someOtherFact("TestPrincipal", "abcde", "three"). +says_thirdFact("TestPrincipal", "OtherPrincipal"). +grounded_dummy("dummy_var"). diff --git a/src/policy/auth_logic/AuthLogic.g4 b/src/policy/auth_logic/AuthLogic.g4 index ff20f0cf1..6a3d9d4fc 100644 --- a/src/policy/auth_logic/AuthLogic.g4 +++ b/src/policy/auth_logic/AuthLogic.g4 @@ -141,7 +141,7 @@ ATTRIBUTE: 'attribute'; // Identifiers wrapped in quotes are constants whereas // identifiers without quotes are variables. VARIABLE : [_a-zA-Z][_a-zA-Z0-9/.#:]*; -STRING_LITERAL : '"' [_a-zA-Z%][@_a-zA-Z0-9/.#:-]* '"'; +STRING_LITERAL : '"' ~["]*? '"'; MULTILINE_STRING_LITERAL : '"""' [\n _a-zA-Z+-][\n _a-zA-Z0-9/.#:+=-]* '"""'; NUMLITERAL : [0-9]+;