Added privacy typing for information-flow control.

1 files changed, 69 insertions, 0 deletions

diff --git a/stdlib/source/lux/control/security/privacy.lux b/stdlib/source/lux/control/security/privacy.lux
new file mode 100644
index 000000000..eeccbd57e
--- /dev/null
+++ b/stdlib/source/lux/control/security/privacy.lux
@@ -0,0 +1,69 @@
+(.module:
+  [lux #*
+   [control
+    [functor (#+ Functor)]
+    [apply (#+ Apply)]
+    [monad (#+ Monad)]]
+   [type
+    abstract]])
+
+(abstract: #export (Private label value)
+  {#.doc (doc "A value that is regarded as 'private'."
+              "The special 'label' parameter exists to distinguish private values of the same basic type."
+              "This distinction is necessary when such values are produced in different policies."
+              "This matters, as different policies will have different means to deal with private values."
+              "The main way to deal with private values is to produce 'public' values from them, by calculating values which do not reveal any private information."
+              "An example of a computation which may produce a public value from a private value, would be a hashing function.")}
+
+  ## Only the public 'value' is necessary, as the 'label' is only
+  ## there to prevent confusing private values from different origins.
+  value
+
+  (signature: #export (Privilege label value)
+    (: (-> value (Private label value))
+       conceal)
+    
+    (: (-> (Private label value) value)
+       reveal))
+
+  (type: #export (Policy value scope label)
+    (-> (Privilege label value)
+        (scope label)))
+
+  (def: #export (with-privacy policy)
+    {#.doc (doc "Takes a function that will operate in a privileged/trusted context."
+                "Within that context, it will be possible to label values as 'private'."
+                "It will also be possible to downgrade private values to 'public' (un-labelled) values."
+                "This function can be used to instantiate structures for signatures that provide privacy-sensitive operations."
+                "The context should not, under any circumstance, reveal any private information it may be privy to."
+                "Make sure any functions which produce public values from private values are properly reviewed for potential information leaks.")}
+    (All [value scope]
+      (Ex [label]
+        (-> (Policy value scope label)
+            (scope label))))
+    (policy (structure (def: conceal (|>> :abstraction))
+                       (def: reveal (|>> :representation)))))
+
+  (structure: #export Functor<Private>
+    (All [label] (Functor (Private label)))
+    
+    (def: (map f fa)
+      (|> fa :representation f :abstraction)))
+
+  (structure: #export Apply<Private>
+    (All [label] (Apply (Private label)))
+    
+    (def: functor Functor<Private>)
+
+    (def: (apply ff fa)
+      (:abstraction ((:representation ff) (:representation fa)))))
+
+  (structure: #export Monad<Private>
+    (All [label] (Monad (Private label)))
+    
+    (def: functor Functor<Private>)
+
+    (def: wrap (|>> :abstraction))
+
+    (def: join (|>> :representation)))
+  )