Handling multiverses (#386)

Closes #386

PiperOrigin-RevId: 432963473

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",
     ],
 )
 

rust/tools/authorization-logic/raksha_examples/multimic-no-overrides/multimic.authlogic

@@ -1,19 +1,11 @@
-.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)
 .decl hasTag(x : symbol, y : symbol)
 .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 {

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 {

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.