diff --git a/rust/tools/authorization-logic/BUILD b/rust/tools/authorization-logic/BUILD index 482c9c11f..f3186bc81 100644 --- a/rust/tools/authorization-logic/BUILD +++ b/rust/tools/authorization-logic/BUILD @@ -76,6 +76,7 @@ filegroup( "src/souffle/mod.rs", "src/souffle/souffle_emitter.rs", "src/souffle/souffle_interface.rs", + "src/souffle/universe_translation.rs", ], ) @@ -89,11 +90,13 @@ filegroup( "src/test/test_export_signatures.rs", "src/test/test_multimic_no_overrides.rs", "src/test/test_multimic_overrides.rs", + "src/test/test_multiverse_handling.rs", "src/test/test_negation.rs", "src/test/test_num_string_names.rs", "src/test/test_queries.rs", "src/test/test_relation_declarations.rs", "src/test/test_signing.rs", + "src/test/test_type_error.rs", ], ) diff --git a/rust/tools/authorization-logic/raksha_examples/multimic-no-overrides/multimic.authlogic b/rust/tools/authorization-logic/raksha_examples/multimic-no-overrides/multimic.authlogic index 89bb82ce8..24599a498 100644 --- a/rust/tools/authorization-logic/raksha_examples/multimic-no-overrides/multimic.authlogic +++ b/rust/tools/authorization-logic/raksha_examples/multimic-no-overrides/multimic.authlogic @@ -1,4 +1,4 @@ -.decl attribute may(action : symbol, tag : symbol) +.decl may(prin : Principal, action : symbol, tag : symbol) .decl overridePreferences(subject : symbol) .decl will(action : symbol, tag : symbol) @@ -6,14 +6,6 @@ .decl ownsTag(owner : Principal, y : symbol) .decl downgrades(path : symbol, tag : symbol) -.decl isAction(action : symbol) -.decl isPath(path : symbol) -.decl isTag(tag : symbol) -.decl isPrincipal(p : Principal) -.decl isSpeechTranscript(x : symbol) -.decl isUserTranscript(x : symbol) -.decl isUserSpeech(x : symbol) - // When "UserX" enters the room, a runtime on the user's // mobile device sends a packet to the microphone which contains the following // facts serialized (and with relevant signatures): @@ -37,27 +29,11 @@ // The user allows the userSpeech tag to just be dropped, or for any // action to be done with data owned by UserA. UserA grants permission for // TrustedCompany to give any particle (PrincipalX) these permissions. - "TrustedCompany" canSay downgrades(pathX, "UserA_userSpeech") :- - isPath(pathX). + "TrustedCompany" canSay downgrades(pathX, "UserA_userSpeech"). // This says any tag, but because of how Raksha works internally, only // permissions UserA gives about its own tags matter - "TrustedCompany" canSay may(PrincipalX, anyActionX, userATagX) :- - isAction(anyActionX), isPrincipal(PrincipalX), isTag(userATagX). - - // This is stuff that needs to be generated behind the scenes - // (Clearly A's policy should have no knowledge of this) - isAction("deliver_privacy_notifications"). - isAction("local_computation"). - isAction("store"). - isPrincipal("Notifier"). - isPrincipal("MicCompute"). - isPrincipal("SpeechToTextStorageSink"). - isPath("audioIn"). - isPath("asrStorageConn"). - isPath("speechToTextIn"). - isTag("UserA_userSpeech"). - isTag("UserA_speechTranscript"). + "TrustedCompany" canSay may(PrincipalX, anyActionX, userATagX). } // UserB is a guest user. UserB is somewhat privacy sensitive. They want their @@ -76,33 +52,20 @@ // (In practice, PrincipalX is going to be any software module of // "TrustedCompany"'s choosing). "TrustedCompany" canSay - may(PrincipalX, "local_computation", "UserB_userSpeech") :- isPrincipal(PrincipalX). + may(PrincipalX, "local_computation", "UserB_userSpeech"). "TrustedCompany" canSay - may(PrincipalX, "store", "UserB_speechTranscript") :- isPrincipal(PrincipalX). + may(PrincipalX, "store", "UserB_speechTranscript"). // UserB trusts TrustedCompany to properly transform userSpeech into just // transcripts. "TrustedCompany" canSay downgrades(pathX, "UserB_userSpeech") :- hasTag(pathX, "UserB_speechTranscript"). - "TrustedCompany" canSay hasTag(PathX, "UserB_speechTranscript") :- - isPath(PathX). + "TrustedCompany" canSay hasTag(PathX, "UserB_speechTranscript"). // Audio can also be used to deliver notifications about the fact that there is a // microphone in the room "TrustedCompany" canSay - may(PrincipalX, "deliver_privacy_notifications", "UserB_userSpeech") :- - isPrincipal(PrincipalX). + may(PrincipalX, "deliver_privacy_notifications", "UserB_userSpeech"). - // This is stuff that needs to be generated behind the scenes - // (Clearly B's policy should have no knowledge of this) - isAction("deliver_privacy_notifications"). - isAction("local_computation"). - isAction("store"). - isPrincipal("Notifier"). - isPrincipal("MicCompute"). - isPrincipal("SpeechToTextStorageSink"). - isPath("audioIn"). - isPath("asrStorageConn"). - isPath("speechToTextIn"). } // UserC is a very privacy sensitive user. They do not trust anyone to store @@ -114,39 +77,23 @@ ownsTag("UserC", "UserC_userSpeech"). ownsTag("UserC", "UserC_speechTranscript"). "TrustedCompany" canSay - may(PrincipalX, "deliver_privacy_notifications", "UserC_userSpeech") :- - isPrincipal(PrincipalX). + may(PrincipalX, "deliver_privacy_notifications", "UserC_userSpeech"). // Unlike UserB, UserC does NOT give any additional permissions for data // that has been transformed into a transcript. - isPrincipal("Notifier"). } // TrustedCompany delegates the needed permissions to the specific particles // after having done review of the code in those particles. "TrustedCompany" says { - may("Notifier", "deliver_privacy_notifications", UserX_userSpeech) :- + may("Notifier", "deliver_privacy_notifications", UserX_userSpeech). // ideally, the "UserX_" Prefix would be a feature that allows us to just // refer to the second part of the name and the "isUserSpeech" predicate would // not be needed - isUserSpeech(UserX_userSpeech). - may("MicCompute", "local_computation", UserX_userSpeech) :- - isUserSpeech(UserX_userSpeech). - "MicCompute" canSay downgrades("asrStorageConn", UserX_userSpeech) :- - isUserSpeech(UserX_userSpeech). - "MicCompute" canSay hasTag("asrStorageConn", UserX_speechTranscript) :- - isSpeechTranscript(UserX_speechTranscript). - may("SpeechToTextStorageSink", "store", UserX_speechTranscript) :- - isSpeechTranscript(UserX_speechTranscript). - - // something like this needs to be generated "behind the scenes" for this to - // work - isUserSpeech("UserA_userSpeech"). - isUserSpeech("UserB_userSpeech"). - isUserSpeech("UserC_userSpeech"). - isSpeechTranscript("UserA_speechTranscript"). - isSpeechTranscript("UserB_speechTranscript"). - isSpeechTranscript("UserC_speechTranscript"). + may("MicCompute", "local_computation", UserX_userSpeech). + "MicCompute" canSay downgrades("asrStorageConn", UserX_userSpeech). + "MicCompute" canSay hasTag("asrStorageConn", UserX_speechTranscript). + may("SpeechToTextStorageSink", "store", UserX_speechTranscript). } //----------------------------------------------------------------------------- @@ -162,20 +109,8 @@ "MicCompute" says { will("local_computation", "audioIn"). // Assumes we can figure out tags with namespaces like this: - downgrades("asrStorageConn", UserX_userSpeech) :- - // ideally this predicate would be added behind the scenes: - isUserSpeech(UserX_userSpeech). - hasTag("asrStorageConn", UserX_userTranscript) :- - // should be added behind the scenes - isSpeechTranscript(UserX_userTranscript). - - // should be added behind the scenes: - isUserSpeech("UserA_userSpeech"). - isUserSpeech("UserB_userSpeech"). - isUserSpeech("UserC_userSpeech"). - isSpeechTranscript("UserA_speechTranscript"). - isSpeechTranscript("UserB_speechTranscript"). - isSpeechTranscript("UserA_speechTranscript"). + downgrades("asrStorageConn", UserX_userSpeech). + hasTag("asrStorageConn", UserX_userTranscript). } "SpeechToTextStorageSink" says { diff --git a/rust/tools/authorization-logic/raksha_examples/multimic-overrides/multimic-preferences.authlogic b/rust/tools/authorization-logic/raksha_examples/multimic-overrides/multimic-preferences.authlogic index 9826a9308..8f4ee7341 100644 --- a/rust/tools/authorization-logic/raksha_examples/multimic-overrides/multimic-preferences.authlogic +++ b/rust/tools/authorization-logic/raksha_examples/multimic-overrides/multimic-preferences.authlogic @@ -10,16 +10,6 @@ .decl downgrades(path : symbol, tag : symbol) .decl allowTranscription(p : Principal) -.decl isAction(action : symbol) -.decl isPath(path : symbol) -.decl isTag(tag : symbol) -.decl isPrincipal(p : Principal) -.decl isSpeechTranscript(x : symbol) -.decl isUserTranscript(x : symbol) -.decl isPrivacyPreference(pref : symbol) -.decl isPrivacyResolution(resolution : symbol) -.decl isUserSpeech(x : symbol) - // When "UserX" enters the room, a runtime on the user's // mobile device sends a packet to the microphone which contains the following // facts serialized (and with relevant signatures): @@ -66,27 +56,10 @@ // User A gives the policy principal the right to decide that any action can // be done with UserA's data and to transform this data in any way. - "AmbientPrivacyPolicy" canSay PrincipalX may(ActionX, TagX) :- - isAction(ActionX), isPrincipal(PrincipalX), isTag(TagX). - "AmbientPrivacyPolicy" canSay downgrades(PathX, TagX) :- - isPath(PathX), isTag(TagX). - "AmbientPrivacyPolicy" canSay hasTag(PathX, TagX) :- - isPath(PathX), isTag(TagX). - - // This is stuff that needs to be generated behind the scenes - // (Clearly A's policy should have no knowledge of this) - isAction("deliver_privacy_notifications"). - isAction("local_computation"). - isAction("store"). - isPrincipal("AmbientPrivacyPolicy"). - isPrincipal("Notifier"). - isPrincipal("MicCompute"). - isPrincipal("SpeechToTextStorageSink"). - isPath("audioIn"). - isPath("asrStorageConn"). - isPath("speechToTextIn"). - isTag("UserA_userSpeech"). - isTag("UserA_speechTranscript"). + "AmbientPrivacyPolicy" canSay PrincipalX may(ActionX, TagX). + "AmbientPrivacyPolicy" canSay downgrades(PathX, TagX). + "AmbientPrivacyPolicy" canSay hasTag(PathX, TagX). + } // UserB is a guest user. UserB is somewhat privacy sensitive. They want their @@ -105,27 +78,10 @@ // User B gives the policy principal the right to decide that any action can // be done with UserB's data and to transform this data in any way. - "AmbientPrivacyPolicy" canSay PrincipalX may(ActionX, TagX) :- - isAction(ActionX), isPrincipal(PrincipalX), isTag(TagX). - "AmbientPrivacyPolicy" canSay downgrades(PathX, TagX) :- - isPath(PathX), isTag(TagX). - "AmbientPrivacyPolicy" canSay hasTag(PathX, TagX) :- - isPath(PathX), isTag(TagX). - - // This is stuff that needs to be generated behind the scenes - // (Clearly B's policy should have no knowledge of this) - isAction("deliver_privacy_notifications"). - isAction("local_computation"). - isAction("store"). - isPrincipal("AmbientPrivacyPolicy"). - isPrincipal("Notifier"). - isPrincipal("MicCompute"). - isPrincipal("SpeechToTextStorageSink"). - isPath("audioIn"). - isPath("asrStorageConn"). - isPath("speechToTextIn"). - isTag("UserB_userSpeech"). - isTag("UserB_speechTranscript"). + "AmbientPrivacyPolicy" canSay PrincipalX may(ActionX, TagX). + "AmbientPrivacyPolicy" canSay downgrades(PathX, TagX). + "AmbientPrivacyPolicy" canSay hasTag(PathX, TagX). + } // UserC is a very privacy sensitive user. They do not trust anyone to store @@ -146,27 +102,9 @@ // User C gives the policy principal the right to decide that any action can // be done with UserC's data and to transform this data in any way. - "AmbientPrivacyPolicy" canSay PrincipalX may(ActionX, TagX) :- - isAction(ActionX), isPrincipal(PrincipalX), isTag(TagX). - "AmbientPrivacyPolicy" canSay downgrades(PathX, TagX) :- - isPath(PathX), isTag(TagX). - "AmbientPrivacyPolicy" canSay hasTag(PathX, TagX) :- - isPath(PathX), isTag(TagX). - - // This is stuff that needs to be generated behind the scenes - // (Clearly C's policy should have no knowledge of this) - isAction("deliver_privacy_notifications"). - isAction("local_computation"). - isAction("store"). - isPrincipal("AmbientPrivacyPolicy"). - isPrincipal("Notifier"). - isPrincipal("MicCompute"). - isPrincipal("SpeechToTextStorageSink"). - isPath("audioIn"). - isPath("asrStorageConn"). - isPath("speechToTextIn"). - isTag("UserC_userSpeech"). - isTag("UserC_speechTranscript"). + "AmbientPrivacyPolicy" canSay PrincipalX may(ActionX, TagX). + "AmbientPrivacyPolicy" canSay downgrades(PathX, TagX). + "AmbientPrivacyPolicy" canSay hasTag(PathX, TagX). } // The facts here are produced by some part of the microphone's operating @@ -182,13 +120,10 @@ // This policy allows end-users to express their own preferences and state // their own preference for how dispute resolution should be done. - UserX canSay UserX hasPrivacyPreference("audio", PreferenceX) :- - isPrivacyPreference(PreferenceX), isPrincipal(UserX). - UserX canSay UserX setsPrivacyResolution("audio", ResolutionX) :- - isPrivacyResolution(ResolutionX), isPrincipal(UserX). + UserX canSay UserX hasPrivacyPreference("audio", PreferenceX). + UserX canSay UserX setsPrivacyResolution("audio", ResolutionX). - "DeviceRoleAuthority" canSay UserX ownsDevice("this_microphone") :- - isPrincipal(UserX). + "DeviceRoleAuthority" canSay UserX ownsDevice("this_microphone"). // The privacy preferences of some members of the room might not be met if // the owner of the device says that it needs to stay on. @@ -197,8 +132,7 @@ // Regardless of preferences, notification that there is a microphone is // always allowed. - "Notifier" may("deliver_privacy_notifications", UserX_userSpeech) :- - isUserSpeech(UserX_userSpeech). + "Notifier" may("deliver_privacy_notifications", UserX_userSpeech). // The pipleine involving transcription and storage of the transcript is // allowed to run for a particular user if: @@ -210,42 +144,28 @@ allowTranscription(UserX) :- UserX hasPrivacyPreference("audio", "only_store_transcript"). allowTranscription(UserX) :- UserX hasPrivacyPreference("audio", "permissive"). - allowTranscription(UserX) :- overridePreferences("audio"), isPrincipal(UserX). + allowTranscription(UserX) :- overridePreferences("audio"). "MicCompute" may("local_computation", UserX_userSpeech) :- - isUserSpeech(UserX_userSpeech), ownsTag(UserX, UserX_userSpeech), + ownsTag(UserX, UserX_userSpeech), allowTranscription(UserX). "MicCompute" canSay downgrades("asrStorageConn", UserX_userSpeech) :- - isUserSpeech(UserX_userSpeech), ownsTag(UserX, UserX_userSpeech), + ownsTag(UserX, UserX_userSpeech), allowTranscription(UserX). "MicCompute" canSay hasTag("asrStorageConn", UserX_speechTranscript) :- - isUserTranscript(UserX_speechTranscript), ownsTag(UserX, UserX_speechTranscript), + ownsTag(UserX, UserX_speechTranscript), allowTranscription(UserX). "SpeechToTextStorageSink" may("store", UserX_speechTranscript) :- - isUserTranscript(UserX_speechTranscript), ownsTag(UserX, UserX_speechTranscript), + ownsTag(UserX, UserX_speechTranscript), allowTranscription(UserX). // Should be generated behind the scenes: - isPrincipal("UserA"). - isPrincipal("UserB"). - isPrincipal("UserC"). - isPrivacyPreference("permissive"). - isPrivacyPreference("only_store_transcript"). - isPrivacyPreference("only_notify"). - isPrivacyResolution("stay_on"). - isPrivacyResolution("meet_requests"). - isUserSpeech("UserA_userSpeech"). - isUserSpeech("UserB_userSpeech"). - isUserSpeech("UserC_userSpeech"). ownsTag("UserA", "UserA_userSpeech"). ownsTag("UserB", "UserB_userSpeech"). ownsTag("UserC", "UserC_userSpeech"). - isUserTranscript("UserA_speechTranscript"). - isUserTranscript("UserB_speechTranscript"). - isUserTranscript("UserC_speechTranscript"). ownsTag("UserA", "UserA_speechTranscript"). ownsTag("UserB", "UserB_speechTranscript"). ownsTag("UserC", "UserC_speechTranscript"). @@ -264,20 +184,8 @@ "MicCompute" says { will("local_computation", "audioIn"). // Assumes we can figure out tags with namespaces like this: - downgrades("asrStorageConn", UserX_userSpeech) :- - // ideally this predicate would be added behind the scenes: - isUserSpeech(UserX_userSpeech). - hasTag("asrStorageConn", UserX_userTranscript) :- - // should be added behind the scenes - isSpeechTranscript(UserX_userTranscript). - - // should be added behind the scenes: - isUserSpeech("UserA_userSpeech"). - isUserSpeech("UserB_userSpeech"). - isUserSpeech("UserC_userSpeech"). - isSpeechTranscript("UserA_speechTranscript"). - isSpeechTranscript("UserB_speechTranscript"). - isSpeechTranscript("UserA_speechTranscript"). + downgrades("asrStorageConn", UserX_userSpeech). + hasTag("asrStorageConn", UserX_userTranscript). } "SpeechToTextStorageSink" says { diff --git a/rust/tools/authorization-logic/src/souffle/lowering_ast_datalog.rs b/rust/tools/authorization-logic/src/souffle/lowering_ast_datalog.rs index f6a53cb7e..3dbee2a35 100644 --- a/rust/tools/authorization-logic/src/souffle/lowering_ast_datalog.rs +++ b/rust/tools/authorization-logic/src/souffle/lowering_ast_datalog.rs @@ -1,5 +1,5 @@ /* - * Copyright 2021 The Raksha Authors + * Copyright 2021 Google LLC. * * Licensed under the Apache License, Version 2.0 (the "License"); * you may not use this file except in compliance with the License. diff --git a/rust/tools/authorization-logic/src/souffle/mod.rs b/rust/tools/authorization-logic/src/souffle/mod.rs index a3d102fad..86772afc4 100644 --- a/rust/tools/authorization-logic/src/souffle/mod.rs +++ b/rust/tools/authorization-logic/src/souffle/mod.rs @@ -14,6 +14,7 @@ * limitations under the License. */ +mod universe_translation; mod datalog_ir; mod lowering_ast_datalog; mod souffle_emitter; diff --git a/rust/tools/authorization-logic/src/souffle/souffle_emitter.rs b/rust/tools/authorization-logic/src/souffle/souffle_emitter.rs index 7d5233873..67c20963b 100644 --- a/rust/tools/authorization-logic/src/souffle/souffle_emitter.rs +++ b/rust/tools/authorization-logic/src/souffle/souffle_emitter.rs @@ -72,11 +72,12 @@ fn emit_assertion(a: &DLIRAssertion) -> String { } fn emit_program_body(p: &DLIRProgram) -> String { - p.assertions + let mut body_vec = p.assertions .iter() .map(|x| emit_assertion(&x)) - .collect::>() - .join("\n") + .collect::>(); + body_vec.sort(); + body_vec.join("\n") } fn emit_type_declarations(p: &DLIRProgram, decl_skip: &Vec) -> String { @@ -96,26 +97,29 @@ fn emit_type_declarations(p: &DLIRProgram, decl_skip: &Vec) -> String { !(**type_name == "symbol".to_string()) }).collect::>(); - type_names_filtered.iter() + let mut ret_vec = type_names_filtered.iter() .map(|type_| format!(".type {} <: symbol", type_)) - .collect::>() - .join("\n") + .collect::>(); + ret_vec.sort(); + ret_vec.join("\n") } fn emit_relation_declarations(p: &DLIRProgram, decl_skip: &Vec) -> String { - p.relation_declarations + let mut ret_vec = p.relation_declarations .iter() .filter(|x| !decl_skip.contains(&x.predicate_name)) .map(|x| emit_decl(x)) - .collect::>() - .join("\n") + .collect::>(); + ret_vec.sort(); + ret_vec.join("\n") } fn emit_outputs(p: &DLIRProgram) -> String { - p.outputs + let mut ret_vec = p.outputs .iter() .map(|o| String::from(".output ") + &o) - .collect::>() - .join("\n") + .collect::>(); + ret_vec.sort(); + ret_vec.join("\n") } diff --git a/rust/tools/authorization-logic/src/souffle/souffle_interface.rs b/rust/tools/authorization-logic/src/souffle/souffle_interface.rs index b272825e7..93cd73ed8 100644 --- a/rust/tools/authorization-logic/src/souffle/souffle_interface.rs +++ b/rust/tools/authorization-logic/src/souffle/souffle_interface.rs @@ -22,7 +22,7 @@ use std::process::Command; use crate::{ ast::*, parsing::astconstructionvisitor, - souffle::{lowering_ast_datalog::*, souffle_emitter}, + souffle::{universe_translation::*, lowering_ast_datalog::*, souffle_emitter}, }; /// Given a filename containing policy code this function parses it, @@ -31,7 +31,8 @@ use crate::{ pub fn emit_souffle(filename: &str) { let source = fs::read_to_string(filename).expect("failed to read input in emit_souffle"); let prog = astconstructionvisitor::parse_program(&source[..]); - let dlir_prog = LoweringToDatalogPass::lower(&prog); + let universe_handled_prog = UniverseHandlingPass::handle_universes(&prog); + let dlir_prog = LoweringToDatalogPass::lower(&universe_handled_prog); let souffle_code = souffle_emitter::emit_program(&dlir_prog, &None); println!("souffle code from {}, \n{}", &filename, souffle_code); } @@ -44,7 +45,8 @@ pub fn input_to_souffle_file(filename: &str, in_dir: &str, out_dir: &str) { let source = fs::read_to_string(&format!("{}/{}", in_dir, filename)) .expect("failed to read input in input_to_souffle_file"); let prog = astconstructionvisitor::parse_program(&source[..]); - let dlir_prog = LoweringToDatalogPass::lower(&prog); + let universe_handled_prog = UniverseHandlingPass::handle_universes(&prog); + let dlir_prog = LoweringToDatalogPass::lower(&universe_handled_prog); let souffle_code = souffle_emitter::emit_program(&dlir_prog, &None); fs::write(&format!("{}/{}.dl", out_dir, filename), souffle_code) .expect("failed to write output to file"); @@ -56,7 +58,8 @@ pub fn input_to_souffle_file(filename: &str, in_dir: &str, out_dir: &str) { /// main code. pub fn ast_to_souffle_file(prog: &AstProgram, filename: &str, out_dir: &str, decl_skip: &Option>) { - let dlir_prog = LoweringToDatalogPass::lower(&prog); + let universe_handled_prog = UniverseHandlingPass::handle_universes(&prog); + let dlir_prog = LoweringToDatalogPass::lower(&universe_handled_prog); let souffle_code = souffle_emitter::emit_program(&dlir_prog, decl_skip); fs::write(&format!("{}/{}.dl", out_dir, filename), souffle_code) .expect("failed to write output to file"); diff --git a/rust/tools/authorization-logic/src/souffle/universe_translation.rs b/rust/tools/authorization-logic/src/souffle/universe_translation.rs new file mode 100644 index 000000000..35a9b1008 --- /dev/null +++ b/rust/tools/authorization-logic/src/souffle/universe_translation.rs @@ -0,0 +1,514 @@ +/* + * 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 a translation that populates the universe relations. +//! Universe relations are facts of the form `isSymbol(x)` that are used to +//! keep datalog rules grounded and finite. This pattern works by putting facts +//! of the form `isSymbol(x)` on the RHS of a conditional rule where the variable `x` +//! would otherwise be ungrounded; then the set of symbols is populated by adding unconditional +//! facts of the form `isSymbol("specific_symbol").` to populate these universes. +//! +//! A problem with using this pattern in the context of authorization logic is that these universes +//! need to be shared across principals. Manually using this pattern is also tedius, and makes the +//! code less clear. This translation handles both of these problems by: +//! 1) extending the program to implement the universe relation pattern by: adding universe +//! predicates to the RHS of rules, and adding facts that add elements to universes. +//! 2) extending the program with facts that use delegation to pass membership of universes across +//! principals. +//! +//! This translation is a compiler pass that operates on the data structure described in `ast.rs` +//! and produces a new instance of the data structure in `ast.rs`. +//! It should come before the translation in `lowering_ast_datalog.rs`. + +use crate::ast::*; +use std::collections::{HashMap, HashSet}; + +// Determine if a function argument or principal name is a constant or +// return false if this name is a variable. In the ast, all arguments are +// represented as strings, and +// they are constants if and only if they are wrapped in quotes. A better +// way to represent this in the future might be to add an AST node for +// arguments with varibales and constants as two possible forms. +fn is_name_constant(arg: &str) -> bool { + return arg.starts_with("\"") +} + +fn push_option_to_vec(vec: &mut Vec, elt: Option) { + if let Some(x) = elt { + vec.push(x); + } +} + +fn push_if_constant(hash_set: &mut HashSet, name: String) { + if is_name_constant(&name) { + hash_set.insert(name); + } +} + +fn universe_condition_principal(principal: &AstPrincipal) -> Option { + if is_name_constant(&principal.name) { + None + } else { + Some(AstPredicate { + sign: Sign::Positive, + name: type_to_universe_name(&AstType::PrincipalType), + args: vec![principal.name.clone()] + }) + } +} + +fn type_to_universe_name(ast_type: &AstType) -> String { + match ast_type { + AstType::NumberType => "isNumber".to_string(), + AstType::PrincipalType => "isPrincipal".to_string(), + AstType::CustomType { type_name } => format!("is{}", type_name.clone()) + } +} + +fn universe_declarations(rel_decls: &Vec) + -> Vec { + // Set of all custom type names + let mut custom_types = rel_decls.iter() + .map(|rel_decl| rel_decl.arg_typings.clone()) + .flatten() + .map(|(name, typ)| typ) + .filter(|type_| match type_ { + AstType::CustomType { type_name } => true, + _ => false + }) + .collect::>(); + custom_types.extend([AstType::NumberType, AstType::PrincipalType]); + let universe_type_pairs = custom_types.iter() + .map(|typ| (type_to_universe_name(typ), typ)); + + universe_type_pairs.map(|(rel_name, typ)| AstRelationDeclaration { + predicate_name: rel_name.to_string(), + is_attribute: false, + arg_typings: vec![("x".to_string(), typ.clone())] + }) + .collect::>() +} + +//----------------------------------------------------------------------------- +// Populate Constant Type Environment & Type Checking +//----------------------------------------------------------------------------- +// These functions populate a mapping from constants (which may either be constant +// principals or other constant values applied as arguments to predicates) to types. +// This environment is needed to generate facts that put the constants into +// universe relations; we need to know which universe relation to put each one in. + +// TODO(#416): these functions should be refactored into a visitor. These are probably +// the first really good use-case for a visitor since this is the first +// functionality that traverses the AST in a way that is not highly order-dependent. +// TODO(#417) it might also be useful to move this into its own separate pass. + +// This attempts to add a typing for principals and predicate arguments if they +// are constant. It does nothing if it is applied to an `arg_name` that is not +// constant. If there is no typing for this constant, it adds this typing to +// the environment. If the same typing already exists in the environment, +// it does nothing. If the constant already has a different typing in the +// environment, throw an error. +fn add_typing(constant_type_environment: &mut HashMap, + arg_name: &str, typ: AstType) { + if is_name_constant(arg_name) { + let arg_name_string = arg_name.to_string(); + match constant_type_environment.get(&arg_name_string) { + None => { + constant_type_environment.insert(arg_name_string, typ); + }, + Some(old_typ) => { + if old_typ != &typ { + // Type errors could be improved by getting line numbers. + panic!("type error: {} was used with distinct types {:?} and {:?}", + arg_name, old_typ, typ); + } + } + } + } +} + + +fn populate_constant_type_environment_prog( + relation_type_environment: &RelationTypeEnv, + prog: &AstProgram) -> HashMap { + let mut constant_type_environment = HashMap::new(); + + // Add typings for constant speakers in says_assertions + for says_assertion in &prog.assertions + { + add_typing(&mut constant_type_environment, + &says_assertion.prin.name, + AstType::PrincipalType); + } + + // Add typings for constants appearing in assertions + for assertion in prog.assertions.iter() + .map(|says_assertion| &says_assertion.assertions) + .flatten() { + populate_constant_type_environment_assertion( + &relation_type_environment, + &mut constant_type_environment, + &assertion); + } + + for query in prog.queries.iter() { + populate_constant_type_environment_query( + &relation_type_environment, + &mut constant_type_environment, + &query); + } + + constant_type_environment +} + +fn populate_constant_type_environment_assertion( + relation_type_environment: &RelationTypeEnv, + constant_type_environment: &mut HashMap, + assertion: &AstAssertion) { + match assertion { + AstAssertion::AstFactAssertion { f: fact } => { + populate_constant_type_environment_fact( + &relation_type_environment, + constant_type_environment, + fact); + } + AstAssertion::AstCondAssertion { lhs, rhs } => { + populate_constant_type_environment_fact( + &relation_type_environment, + constant_type_environment, + lhs); + for flat_fact in rhs { + populate_constant_type_environment_flat_fact( + &relation_type_environment, + constant_type_environment, + flat_fact); + } + } + } +} + +fn populate_constant_type_environment_query( + relation_type_environment: &RelationTypeEnv, + constant_type_environment: &mut HashMap, + query: &AstQuery) { + + add_typing(constant_type_environment, &query.principal.name, + AstType::PrincipalType); + populate_constant_type_environment_fact(relation_type_environment, + constant_type_environment, + &query.fact); +} + +fn populate_constant_type_environment_fact( + relation_type_environment: &RelationTypeEnv, + constant_type_environment: &mut HashMap, + fact: &AstFact) { + match fact { + AstFact::AstFlatFactFact { f: flat_fact } => { + populate_constant_type_environment_flat_fact( + relation_type_environment, + constant_type_environment, + flat_fact); + }, + AstFact::AstCanSayFact { p: speaker, f: fact } => { + add_typing(constant_type_environment, &speaker.name, + AstType::PrincipalType); + populate_constant_type_environment_fact( + relation_type_environment, + constant_type_environment, + fact); + } + } +} + +fn populate_constant_type_environment_flat_fact( + relation_type_environment: &RelationTypeEnv, + constant_type_environment: &mut HashMap, + flat_fact: &AstFlatFact) { + match flat_fact { + AstFlatFact::AstPrinFact { p: principal, v: verb_phrase } => { + add_typing(constant_type_environment, &principal.name, + AstType::PrincipalType); + match verb_phrase { + AstVerbPhrase::AstPredPhrase { p : predicate } => { + populate_constant_type_environment_predicate( + relation_type_environment, + constant_type_environment, + predicate); + } + AstVerbPhrase::AstCanActPhrase { p : as_principal } => { + add_typing(constant_type_environment, &as_principal.name, + AstType::PrincipalType); + } + } + } + AstFlatFact::AstPredFact { p: predicate } => { + populate_constant_type_environment_predicate( + relation_type_environment, + constant_type_environment, + predicate); + } + } +} + +fn populate_constant_type_environment_predicate( + relation_type_environment: &RelationTypeEnv, + constant_type_environment: &mut HashMap, + predicate: &AstPredicate) { + + let predicate_decl = relation_type_environment.get(&predicate.name).expect( + &format!("The relation \"{}\" was used but not declared", + &predicate.name)); + for (pos, arg_name) in predicate.args.iter().enumerate() { + add_typing(constant_type_environment, arg_name, + predicate_decl.get(&pos).unwrap().clone()); + } + +} + +type RelationTypeEnv = HashMap>; +pub struct UniverseHandlingPass { + // mapping from relation names to relation typings. The relation + // typings map from positions in the relation declaration to types. + // A map from positions in the relation declarations to the + // type of the parameter at those positions. For example, + // `.decl foo(x: SomeThing, y: SomeOtherThing)` + // would yield the map + // ``` + // (foo -> + // (1 -> CustomType{ SomeThing }, + // 2 -> CustomType { SomeOtherThing })) + // ``` + relation_type_environment: RelationTypeEnv, + // maping from constant names to constant typings + constant_type_environment: HashMap +} + +impl UniverseHandlingPass { + + pub fn handle_universes(prog: &AstProgram) -> AstProgram { + let universe_handling_pass = UniverseHandlingPass::new(prog); + let mut new_prog = prog.clone(); + new_prog.assertions = prog.assertions.iter() + .map(|x| { + universe_handling_pass.add_universe_conditions_says_assertion(x) + }) + .collect(); + new_prog.relation_declarations.append(&mut universe_declarations( + &prog.relation_declarations)); + universe_handling_pass.add_universe_defining_says_assertions(&new_prog) + } + + fn new(prog: &AstProgram) -> UniverseHandlingPass { + let rel_typ_env = (&prog.relation_declarations) + .iter() + .map(|decl| { + let position_map = decl.arg_typings.clone() + .into_iter() + .map(|(param_name, typ)| typ) + .into_iter() + .enumerate() + .collect::>(); + (decl.predicate_name.clone(), position_map) + }) + .collect(); + + UniverseHandlingPass { + constant_type_environment: + populate_constant_type_environment_prog( + &rel_typ_env, prog), + relation_type_environment: rel_typ_env + } + } + + //----------------------------------------------------------------------------- + // Add Universe Defining Facts + //----------------------------------------------------------------------------- + // These functions find all the constant principals, and all the constant predicate + // arguments, and emits facts that populate the universes. + fn add_universe_defining_says_assertions(&self, prog: &AstProgram) -> AstProgram { + let constant_speakers: Vec = prog.assertions.clone() + .into_iter() + .map(|says_assertion| says_assertion.prin) + .filter(|prin| is_name_constant(&prin.name)) + .collect(); + let constant_subexpressions: Vec<&String> = + self.constant_type_environment.keys() + .collect(); + + let mut universe_defining_says_assertions = Vec::new(); + for speaker in &constant_speakers { + for subexpr in &constant_subexpressions { + universe_defining_says_assertions.push( + self.universe_defining_says_assertion(&speaker, subexpr)); + } + } + + let mut ret = prog.clone(); + ret.assertions.extend(universe_defining_says_assertions); + ret + } + + fn universe_defining_says_assertion(&self, speaker: &AstPrincipal, + expr: &str) -> AstSaysAssertion { + AstSaysAssertion { + prin: speaker.clone(), + assertions: vec![ AstAssertion::AstFactAssertion { + f: AstFact::AstFlatFactFact { + f: AstFlatFact::AstPredFact { + p: AstPredicate { + sign: Sign::Positive, + name: type_to_universe_name( + self.constant_type_environment.get(expr).unwrap()), + args: vec![expr.to_string()] + } + } + } + }], + export_file: None + } + } + + //----------------------------------------------------------------------------- + // Add Grounding Conditions + //----------------------------------------------------------------------------- + // For rules and facts that would contain otherwise ungrounded variables, + // add universe relations to the RHS to make these assertions grounded. + fn add_universe_conditions_says_assertion(&self, + says_assertion: &AstSaysAssertion) -> AstSaysAssertion { + AstSaysAssertion { + prin: says_assertion.prin.clone(), + assertions: says_assertion.assertions.iter() + .map(|x| self.add_universe_conditions_assertion(x)) + .collect(), + export_file: says_assertion.export_file.clone() + } + } + + // For ungrounded variables appearing in the LHS, extend the RHS + // with prediates that put them in the universe relations. + // TODO(#418) at the moment, this conservatively adds a universe condition + // for all variables on the LHS rather than just the ungrounded ones. Extend + // this to capture just the ungrounded variables. + fn add_universe_conditions_assertion(&self, assertion: &AstAssertion) + -> AstAssertion { + match assertion { + AstAssertion::AstFactAssertion { f: fact } => { + let new_rhs_predicates = self.universe_conditions_fact(&fact); + if new_rhs_predicates.len() > 0 { + AstAssertion::AstCondAssertion { + lhs: fact.clone(), + rhs: new_rhs_predicates + .iter() + .map(|pred| AstFlatFact::AstPredFact{p: pred.clone()}) + .collect() + } + } else { + assertion.clone() + } + } + AstAssertion::AstCondAssertion { lhs, rhs } => { + let mut new_rhs = rhs.clone(); + for x in self.universe_conditions_fact(lhs).iter() { + new_rhs.push( + AstFlatFact::AstPredFact {p: x.clone()}); + } + AstAssertion::AstCondAssertion { + lhs: lhs.clone(), + rhs: new_rhs + } + } + } + } + + // For an AstFact appearing on the LHS of a conditional assertion, + // generate the set of universe predicates that should be added to the RHS + // from the variables that are subexprs of the AstFact. + fn universe_conditions_fact(&self, ast_fact: &AstFact) -> Vec { + match ast_fact { + AstFact::AstFlatFactFact { f: flat_fact } => { + self.universe_conditions_flat_fact(flat_fact) + }, + AstFact::AstCanSayFact { p: delegatee, f: fact } => { + let mut ret = self.universe_conditions_fact(fact); + push_option_to_vec(&mut ret, + universe_condition_principal(&delegatee)); + ret + } + } + } + + fn universe_conditions_flat_fact(&self, ast_flat_fact: &AstFlatFact) + -> Vec { + match ast_flat_fact { + AstFlatFact::AstPrinFact {p: principal, v: verb_phrase} => { + let mut ret = self + .universe_conditions_verb_phrase(verb_phrase); + push_option_to_vec(&mut ret, + universe_condition_principal(&principal)); + ret + } + AstFlatFact::AstPredFact { p: predicate } => { + self.universe_conditions_predicate(predicate) + } + } + } + + fn universe_conditions_verb_phrase(&self, verb_phrase: &AstVerbPhrase) + -> Vec { + match verb_phrase { + AstVerbPhrase::AstPredPhrase { p: predicate } => { + self.universe_conditions_predicate(&predicate) + } + AstVerbPhrase::AstCanActPhrase { p: principal } => { + universe_condition_principal(&principal) + .iter() + // iter returns references so copying is needed + .map(|x| x.clone()) + .collect::>() + } + } + } + + fn universe_conditions_predicate(&self, predicate: &AstPredicate) + -> Vec { + predicate.args.iter().enumerate() + .map(|(pos, arg)| self.universe_condition_arg( + &predicate.name, arg, pos)) + .flatten() + .collect() + } + + fn universe_condition_arg(&self, predicate_name: &str, argument: &str, position: usize) + -> Option { + if is_name_constant(argument) { + None + } else { + let predicate_decl = self.relation_type_environment + .get(predicate_name).expect( + &format!("The relation \"{}\" was used but not declared", + &predicate_name)); + let arg_type = predicate_decl + .get(&position) + .unwrap(); + Some(AstPredicate { + sign: Sign::Positive, + name: type_to_universe_name(arg_type), + args: vec![argument.to_string()] + }) + } + } +} diff --git a/rust/tools/authorization-logic/src/test/mod.rs b/rust/tools/authorization-logic/src/test/mod.rs index d7f6fc6dc..ef8bce811 100644 --- a/rust/tools/authorization-logic/src/test/mod.rs +++ b/rust/tools/authorization-logic/src/test/mod.rs @@ -1,5 +1,5 @@ /* - * Copyright 2021 The Raksha Authors + * Copyright 2021 Google LLC. * * Licensed under the Apache License, Version 2.0 (the "License"); * you may not use this file except in compliance with the License. @@ -25,3 +25,5 @@ mod test_multimic_no_overrides; mod test_multimic_overrides; mod test_num_string_names; mod test_relation_declarations; +mod test_type_error; +mod test_multiverse_handling; diff --git a/rust/tools/authorization-logic/src/test/test_multiverse_handling.rs b/rust/tools/authorization-logic/src/test/test_multiverse_handling.rs new file mode 100644 index 000000000..f5bd12f88 --- /dev/null +++ b/rust/tools/authorization-logic/src/test/test_multiverse_handling.rs @@ -0,0 +1,37 @@ +/* + * Copyright 2021 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. + */ + +#[cfg(test)] +mod test { + use crate::{ + ast::*, compilation_top_level::*, souffle::souffle_interface::*, + test::test_queries::test::*, + }; + use std::fs; + + #[test] + fn test_multiverse_handling() { + run_query_test(QueryTest { + filename: "multiverse_handling", + input_dir: "test_inputs", + output_dir: "test_outputs", + query_expects: vec![ + ("test_query1_true", true), + ("test_query2_false", false) + ] + }) + } +} diff --git a/rust/tools/authorization-logic/src/test/test_negation.rs b/rust/tools/authorization-logic/src/test/test_negation.rs index 77fb2a6f6..b2e2e50c9 100644 --- a/rust/tools/authorization-logic/src/test/test_negation.rs +++ b/rust/tools/authorization-logic/src/test/test_negation.rs @@ -1,5 +1,5 @@ /* - * Copyright 2021 The Raksha Authors + * Copyright 2021 Google LLC. * * Licensed under the Apache License, Version 2.0 (the "License"); * you may not use this file except in compliance with the License. diff --git a/rust/tools/authorization-logic/src/test/test_type_error.rs b/rust/tools/authorization-logic/src/test/test_type_error.rs new file mode 100644 index 000000000..249d6b1aa --- /dev/null +++ b/rust/tools/authorization-logic/src/test/test_type_error.rs @@ -0,0 +1,27 @@ +/* + * Copyright 2021 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. + */ + +#[cfg(test)] +mod test { + use crate::{ast::*, compilation_top_level::*, souffle::souffle_interface::*}; + use std::fs; + + #[test] + #[should_panic] + fn test_type_error() { + compile("type_error", "test_inputs", "test_outputs", ""); + } +} diff --git a/rust/tools/authorization-logic/test_inputs/dotsInNames b/rust/tools/authorization-logic/test_inputs/dotsInNames index 1f74e011d..24ec3c13c 100644 --- a/rust/tools/authorization-logic/test_inputs/dotsInNames +++ b/rust/tools/authorization-logic/test_inputs/dotsInNames @@ -1,3 +1,8 @@ +.decl are(words : Words) +.decl areConditionally(words : Words) +.decl evenIf(words : Words) +.decl areAlso(words : Words) + "TheTestPrincipal" says "names.with.dots.in.them" are("prefectly.cromulent"). "TheTestPrincipal" says "names.with.dots.in.them" areConditionally("cromulent") :- diff --git a/rust/tools/authorization-logic/test_inputs/exporting b/rust/tools/authorization-logic/test_inputs/exporting index 9637bc343..277008a62 100644 --- a/rust/tools/authorization-logic/test_inputs/exporting +++ b/rust/tools/authorization-logic/test_inputs/exporting @@ -1,3 +1,6 @@ +.decl someProposition(words : Words) +.decl otherProposition(words : Words) + BindPrivKey "principal1" test_keys/principal1_priv.json BindPubKey "principal1" test_keys/principal1_pub.json diff --git a/rust/tools/authorization-logic/test_inputs/importing_export_half b/rust/tools/authorization-logic/test_inputs/importing_export_half index 3e1380419..32b2eafcf 100644 --- a/rust/tools/authorization-logic/test_inputs/importing_export_half +++ b/rust/tools/authorization-logic/test_inputs/importing_export_half @@ -5,6 +5,9 @@ BindPrivKey "principal1e" test_keys/principal1e_priv.json BindPubKey "principal1e" test_keys/principal1e_pub.json +.decl someProposition(words : Words) +.decl otherProposition(words : Words) + "principal1e" says { someProposition("these_args"). otherProposition("these_other_args"). diff --git a/rust/tools/authorization-logic/test_inputs/multiverse_handling b/rust/tools/authorization-logic/test_inputs/multiverse_handling new file mode 100644 index 000000000..bf39d1077 --- /dev/null +++ b/rust/tools/authorization-logic/test_inputs/multiverse_handling @@ -0,0 +1,12 @@ +.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")? diff --git a/rust/tools/authorization-logic/test_inputs/numStringsInNames b/rust/tools/authorization-logic/test_inputs/numStringsInNames index eb6867551..e2dbd663a 100644 --- a/rust/tools/authorization-logic/test_inputs/numStringsInNames +++ b/rust/tools/authorization-logic/test_inputs/numStringsInNames @@ -1,2 +1,5 @@ +.decl numbersAre(words : Words) +.decl semicolonsAre(words : Words) + "123" says numbersAre("perfectlyFinePrincipalNames"). "sha256:deadbeef" says semicolonsAre("alsoFineNames"). diff --git a/rust/tools/authorization-logic/test_inputs/quotesInExports b/rust/tools/authorization-logic/test_inputs/quotesInExports index bdac94b52..fbfb7193c 100644 --- a/rust/tools/authorization-logic/test_inputs/quotesInExports +++ b/rust/tools/authorization-logic/test_inputs/quotesInExports @@ -2,6 +2,9 @@ BindPrivKey "p1_noq" test_keys/p1_noq_priv.json BindPubKey "p1_noq" test_keys/p1_noq_pub.json +.decl someProposition(words : Words) +.decl otherProposition(words : Words) + "p1_noq" says { someProposition("these_args"). otherProposition("these_other_args"). diff --git a/rust/tools/authorization-logic/test_inputs/type_error b/rust/tools/authorization-logic/test_inputs/type_error new file mode 100644 index 000000000..ac0ee38db --- /dev/null +++ b/rust/tools/authorization-logic/test_inputs/type_error @@ -0,0 +1,5 @@ +.decl foo(a : OneThing) +.decl bar(a : AnotherThing) + +"PrincipalA" says foo("x"). +"PrincipalA" says bar("x"). diff --git a/src/analysis/souffle/examples/simple/ok_claim_propagates.raksha b/src/analysis/souffle/examples/simple/ok_claim_propagates.raksha index e8ffbb50c..18f00a4a0 100644 --- a/src/analysis/souffle/examples/simple/ok_claim_propagates.raksha +++ b/src/analysis/souffle/examples/simple/ok_claim_propagates.raksha @@ -19,10 +19,7 @@ recipe R .decl ownsTag(principal : Principal, tag : Tag) .decl ownsAccessPath(principal : Principal, path : AccessPath) .decl hasTag(path : AccessPath, prin : Principal, tag : Tag) -.decl isAccessPath(path : AccessPath) "EndUser" says "P1" canSay ownsTag("P1", "userSelection"). "P1" says ownsTag("P1", "userSelection"). "EndUser" says ownsAccessPath("EndUser", "R.P1#0.foo"). -"EndUser" says "P1" canSay hasTag(accessPathX, "EndUser", "userSelection") :- isAccessPath(accessPathX). -"EndUser" says isAccessPath("R.P3#2.bar"). -// "EndUser" says hasTag("R.P3#2.bar", "EndUser", "userSelection"). +"EndUser" says "P1" canSay hasTag(accessPathX, "EndUser", "userSelection"). diff --git a/src/analysis/souffle/examples/simple_canSayDowngrades/ok_claim_propagates_downgrade_granted.authlogic b/src/analysis/souffle/examples/simple_canSayDowngrades/ok_claim_propagates_downgrade_granted.authlogic index f8dd730a6..b6379d943 100644 --- a/src/analysis/souffle/examples/simple_canSayDowngrades/ok_claim_propagates_downgrade_granted.authlogic +++ b/src/analysis/souffle/examples/simple_canSayDowngrades/ok_claim_propagates_downgrade_granted.authlogic @@ -6,5 +6,5 @@ //TODO(#220): This should be at the level of handles which correspond to stores, // where ownership makes more sense. "EndUser" says ownsAccessPath("EndUser", "R.P1#0.foo"). -"EndUser" says "P1" canSay hasTag(accessPathX, "EndUser", "userSelection") :- isAccessPath(accessPathX). -"EndUser" says "P2" canSay removeTag(accessPathX, "EndUser", "userSelection") :- isAccessPath(accessPathX). +"EndUser" says "P1" canSay hasTag(accessPathX, "EndUser", "userSelection"). +"EndUser" says "P2" canSay removeTag(accessPathX, "EndUser", "userSelection"). diff --git a/src/analysis/souffle/examples/simple_canSayDowngrades/ok_claim_propagates_downgrade_granted_by_non_owner.authlogic b/src/analysis/souffle/examples/simple_canSayDowngrades/ok_claim_propagates_downgrade_granted_by_non_owner.authlogic index 622c3abbf..3351f4481 100644 --- a/src/analysis/souffle/examples/simple_canSayDowngrades/ok_claim_propagates_downgrade_granted_by_non_owner.authlogic +++ b/src/analysis/souffle/examples/simple_canSayDowngrades/ok_claim_propagates_downgrade_granted_by_non_owner.authlogic @@ -2,5 +2,5 @@ .decl removeTag(path : AccessPath, principal : Principal, tag : Tag) .decl hasTag(path : AccessPath, principal : Principal, tag : Tag) "EndUser" says ownsAccessPath("EndUser", "R.P1#0.foo"). -"P1" says "P1" canSay hasTag(accessPathX, "EndUser", "userSelection") :- isAccessPath(accessPathX). -"P1" says "P2" canSay removeTag(accessPathX, "EndUser", "userSelection") :- isAccessPath(accessPathX). +"P1" says "P1" canSay hasTag(accessPathX, "EndUser", "userSelection"). +"P1" says "P2" canSay removeTag(accessPathX, "EndUser", "userSelection"). diff --git a/src/analysis/souffle/examples/simple_canSayDowngrades/ok_claim_propagates_downgrade_not_granted.authlogic b/src/analysis/souffle/examples/simple_canSayDowngrades/ok_claim_propagates_downgrade_not_granted.authlogic index cdbb2d8cd..d16327586 100644 --- a/src/analysis/souffle/examples/simple_canSayDowngrades/ok_claim_propagates_downgrade_not_granted.authlogic +++ b/src/analysis/souffle/examples/simple_canSayDowngrades/ok_claim_propagates_downgrade_not_granted.authlogic @@ -3,4 +3,4 @@ .decl hasTag(path : AccessPath, principal : Principal, tag : Tag) "EndUser" says ownsTag("EndUser", "userSelection"). "EndUser" says ownsAccessPath("EndUser", "R.P1#0.foo"). -"EndUser" says "P1" canSay hasTag(accessPathX, "EndUser", "userSelection") :- isAccessPath(accessPathX). +"EndUser" says "P1" canSay hasTag(accessPathX, "EndUser", "userSelection"). diff --git a/src/analysis/souffle/examples/simple_canSayHasTag/ok_claim_propagates_delegation_granted.authlogic b/src/analysis/souffle/examples/simple_canSayHasTag/ok_claim_propagates_delegation_granted.authlogic index 927158944..bf407f1e4 100644 --- a/src/analysis/souffle/examples/simple_canSayHasTag/ok_claim_propagates_delegation_granted.authlogic +++ b/src/analysis/souffle/examples/simple_canSayHasTag/ok_claim_propagates_delegation_granted.authlogic @@ -5,4 +5,4 @@ //TODO(#220): We should claim ownership at the level of handles that correspond // to stores where ownership makes more sense. "EndUser" says ownsAccessPath("EndUser", "R.P1#0.foo"). -"EndUser" says "P1" canSay hasTag(accessPathX, "EndUser", "userSelection") :- isAccessPath(accessPathX). +"EndUser" says "P1" canSay hasTag(accessPathX, "EndUser", "userSelection"). diff --git a/src/analysis/souffle/examples/simple_may_will/simple_may_will_fail.authlogic b/src/analysis/souffle/examples/simple_may_will/simple_may_will_fail.authlogic index 0201d485a..64f07cb7b 100644 --- a/src/analysis/souffle/examples/simple_may_will/simple_may_will_fail.authlogic +++ b/src/analysis/souffle/examples/simple_may_will/simple_may_will_fail.authlogic @@ -18,13 +18,12 @@ .decl ownsTag(prin : Principal, tag : Tag) .decl ownsAccessPath(prin : Principal, path : AccessPath) .decl hasTag(path : AccessPath, prin : Principal, tag : Tag) -.decl isAccessPath(path : AccessPath) .decl will(action : Action, path : AccessPath) "EndUser" says { ownsTag("EndUser", "rawVideo"). ownsAccessPath("EndUser", "R.P1#0.foo"). - "P1" canSay hasTag(PathX, "EndUser", "rawVideo") :- isAccessPath(PathX). + "P1" canSay hasTag(PathX, "EndUser", "rawVideo"). } // It would be better if we could change the manifest frontend and write it diff --git a/src/analysis/souffle/examples/simple_may_will/simple_may_will_pass.authlogic b/src/analysis/souffle/examples/simple_may_will/simple_may_will_pass.authlogic index f6597ee4c..243a8a9c8 100644 --- a/src/analysis/souffle/examples/simple_may_will/simple_may_will_pass.authlogic +++ b/src/analysis/souffle/examples/simple_may_will/simple_may_will_pass.authlogic @@ -17,13 +17,12 @@ .decl ownsTag(prin : Principal, tag : Tag) .decl hasTag(path : AccessPath, prin : Principal, tag : Tag) -.decl isAccessPath(path : AccessPath) .decl may(prin : Principal, action : Action, tag : Tag) .decl will(action : Action, path : AccessPath) "EndUser" says { ownsTag("EndUser", "rawVideo"). - "P1" canSay hasTag(PathX, "EndUser", "rawVideo") :- isAccessPath(PathX). + "P1" canSay hasTag(PathX, "EndUser", "rawVideo"). may("P2", "doLocalComputation", "rawVideo"). } diff --git a/src/xform_to_datalog/authorization_logic_datalog_facts.cc b/src/xform_to_datalog/authorization_logic_datalog_facts.cc index ba3de38a5..0252ff9d2 100644 --- a/src/xform_to_datalog/authorization_logic_datalog_facts.cc +++ b/src/xform_to_datalog/authorization_logic_datalog_facts.cc @@ -40,21 +40,13 @@ AuthorizationLogicDatalogFacts::create(const std::filesystem::path &program_dir, // into the Rust code with StrJoin to make the code a bit more readable and to // prevent typos changing the interpretation of the list. const std::vector kRelationsToNotDeclare{ - "Principal", - "Tag", - "Action", - "AccessPath", - "says_isAccessPath", - "says_isTag", - "says_isPrincipal", - "says_ownsTag", - "says_ownsAccessPath", - "says_hasTag", - "says_removeTag", - "says_may", - "says_will", - "isAccessPath", - "isTag", + "Principal", "Tag", + "AccessPath", "says_isAccessPath", + "says_isTag", "says_isPrincipal", + "says_ownsTag", "says_ownsAccessPath", + "says_hasTag", "says_removeTag", + "says_may", "says_will", + "isAccessPath", "isTag", "isPrincipal"}; int res = GenerateDatalogFactsFromAuthorizationLogic( diff --git a/src/xform_to_datalog/datalog_facts_test.cc b/src/xform_to_datalog/datalog_facts_test.cc index 4655512e1..c63472c20 100644 --- a/src/xform_to_datalog/datalog_facts_test.cc +++ b/src/xform_to_datalog/datalog_facts_test.cc @@ -105,8 +105,9 @@ saysWill(w, x, y) :- says_will(w, x, y). // Authorization Logic .type DummyType <: symbol -.decl says_canActAs(speaker: Principal, p1: Principal, p2: Principal) .decl grounded_dummy(dummy_param: DummyType) +.decl says_canActAs(speaker: Principal, p1: Principal, p2: Principal) +.decl says_isNumber(speaker: Principal, x: number) grounded_dummy("dummy_var"). )"), @@ -154,15 +155,21 @@ says_hasTag("particle", "recipe.particle.out", owner, "tag") :- ownsAccessPath(o // Authorization Logic -.type SomeType <: symbol .type DummyType <: symbol -.decl says_fact1(speaker: Principal, someType: SomeType) -.decl says_cond1(speaker: Principal, someType: SomeType) -.decl says_canActAs(speaker: Principal, p1: Principal, p2: Principal) +.type SomeType <: symbol .decl grounded_dummy(dummy_param: DummyType) -says_fact1("prin1", thing_x) :- says_cond1("prin1", thing_x). -says_cond1("prin1", "foo"). +.decl says_canActAs(speaker: Principal, p1: Principal, p2: Principal) +.decl says_cond1(speaker: Principal, someType: SomeType) +.decl says_fact1(speaker: Principal, someType: SomeType) +.decl says_isNumber(speaker: Principal, x: number) +.decl says_isSomeType(speaker: Principal, x: SomeType) grounded_dummy("dummy_var"). +says_cond1("prin1", "foo"). +says_fact1("prin1", thing_x) :- says_cond1("prin1", thing_x), says_isSomeType("prin1", thing_x). +says_isPrincipal("prin1", "prin1"). +says_isPrincipal("prin1", "prin1"). +says_isSomeType("prin1", "foo"). +says_isSomeType("prin1", "foo"). )"))); diff --git a/src/xform_to_datalog/testdata/empty_auth_logic.dl b/src/xform_to_datalog/testdata/empty_auth_logic.dl index e03682265..61a23335d 100644 --- a/src/xform_to_datalog/testdata/empty_auth_logic.dl +++ b/src/xform_to_datalog/testdata/empty_auth_logic.dl @@ -1,4 +1,5 @@ .type DummyType <: symbol -.decl says_canActAs(speaker: Principal, p1: Principal, p2: Principal) .decl grounded_dummy(dummy_param: DummyType) +.decl says_canActAs(speaker: Principal, p1: Principal, p2: Principal) +.decl says_isNumber(speaker: Principal, x: number) grounded_dummy("dummy_var"). diff --git a/src/xform_to_datalog/testdata/ok_claim_propagates.dl b/src/xform_to_datalog/testdata/ok_claim_propagates.dl index 9d9add2a2..ce6c10eea 100644 --- a/src/xform_to_datalog/testdata/ok_claim_propagates.dl +++ b/src/xform_to_datalog/testdata/ok_claim_propagates.dl @@ -45,11 +45,18 @@ edge("R.handle1", "R.P3#2.bar"). // Authorization Logic .type DummyType <: symbol +.decl grounded_dummy(dummy_param: DummyType) .decl says_canActAs(speaker: Principal, p1: Principal, p2: Principal) .decl says_canSay_ownsTag(speaker: Principal, delegatee1: Principal, prin: Principal, tag: Tag) -.decl grounded_dummy(dummy_param: DummyType) -says_ownsTag("EndUser", "P1", "userSelection") :- says_ownsTag(x___1, "P1", "userSelection"), says_canSay_ownsTag("EndUser", x___1, "P1", "userSelection"). +.decl says_isNumber(speaker: Principal, x: number) +grounded_dummy("dummy_var"). says_canSay_ownsTag("EndUser", "P1", "P1", "userSelection"). +says_isPrincipal("EndUser", "EndUser"). +says_isPrincipal("EndUser", "P1"). +says_isPrincipal("P1", "EndUser"). +says_isPrincipal("P1", "P1"). +says_isTag("EndUser", "userSelection"). +says_isTag("P1", "userSelection"). +says_ownsTag("EndUser", "P1", "userSelection") :- says_ownsTag(x___1, "P1", "userSelection"), says_canSay_ownsTag("EndUser", x___1, "P1", "userSelection"). says_ownsTag("P1", "P1", "userSelection"). -grounded_dummy("dummy_var"). diff --git a/src/xform_to_datalog/testdata/says_owns_tag.dl b/src/xform_to_datalog/testdata/says_owns_tag.dl index 10fbd209d..927e4d769 100644 --- a/src/xform_to_datalog/testdata/says_owns_tag.dl +++ b/src/xform_to_datalog/testdata/says_owns_tag.dl @@ -1,5 +1,9 @@ .type DummyType <: symbol .decl grounded_dummy(dummy_param: DummyType) .decl says_canActAs(speaker: Principal, p1: Principal, p2: Principal) +.decl says_isNumber(speaker: Principal, x: number) says_ownsTag("prin1", "particle", "foo"). +says_isPrincipal("prin1", "prin1"). +says_isTag("prin1", "foo"). +says_isPrincipal("prin1", "particle"). grounded_dummy("dummy_var"). diff --git a/src/xform_to_datalog/testdata/simple_auth_logic.dl b/src/xform_to_datalog/testdata/simple_auth_logic.dl index 42a719066..2cb78b9ae 100644 --- a/src/xform_to_datalog/testdata/simple_auth_logic.dl +++ b/src/xform_to_datalog/testdata/simple_auth_logic.dl @@ -2,8 +2,14 @@ .type DummyType <: symbol .decl says_cond1(speaker: Principal, someType: SomeType) .decl grounded_dummy(dummy_param: DummyType) +.decl says_isSomeType(speaker: Principal, x: SomeType) +.decl says_isNumber(speaker: Principal, x: number) .decl says_fact1(speaker: Principal, someType: SomeType) .decl says_canActAs(speaker: Principal, p1: Principal, p2: Principal) -says_fact1("prin1", thing_x) :- says_cond1("prin1", thing_x). +says_fact1("prin1", thing_x) :- says_cond1("prin1", thing_x), says_isSomeType("prin1", thing_x). says_cond1("prin1", "foo"). +says_isPrincipal("prin1", "prin1"). +says_isSomeType("prin1", "foo"). +says_isPrincipal("prin1", "prin1"). +says_isSomeType("prin1", "foo"). grounded_dummy("dummy_var").