From 9471b31d008fa0bf727a91a9632c404d16077f33 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Wed, 5 Dec 2018 00:01:31 -0400 Subject: Added privacy typing for information-flow control. --- stdlib/source/lux/control/security/privacy.lux | 69 +++++++++++++++++++ stdlib/test/test/lux/control/security/privacy.lux | 80 +++++++++++++++++++++++ 2 files changed, 149 insertions(+) create mode 100644 stdlib/source/lux/control/security/privacy.lux create mode 100644 stdlib/test/test/lux/control/security/privacy.lux 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 + (All [label] (Functor (Private label))) + + (def: (map f fa) + (|> fa :representation f :abstraction))) + + (structure: #export Apply + (All [label] (Apply (Private label))) + + (def: functor Functor) + + (def: (apply ff fa) + (:abstraction ((:representation ff) (:representation fa))))) + + (structure: #export Monad + (All [label] (Monad (Private label))) + + (def: functor Functor) + + (def: wrap (|>> :abstraction)) + + (def: join (|>> :representation))) + ) diff --git a/stdlib/test/test/lux/control/security/privacy.lux b/stdlib/test/test/lux/control/security/privacy.lux new file mode 100644 index 000000000..14ef98a15 --- /dev/null +++ b/stdlib/test/test/lux/control/security/privacy.lux @@ -0,0 +1,80 @@ +(.module: + [lux #* + [control + [hash (#+ Hash)] + [monad (#+ do)] + [security + ["@" privacy (#+ Private Policy with-privacy)]]] + [data + ["." text ("text/." Equivalence) + format]] + [math + ["r" random]]] + lux/test) + +(signature: (Password %) + (: (Hash (Private % Text)) + &hash) + + (: (-> Text (Private % Text)) + password)) + +(def: (Password<%> _) + (Ex [%] (-> Any (Password %))) + (with-privacy + (: (Policy Text Password) + (function (_ (^open "%/.")) + (structure + (def: &hash + (structure + (def: eq + (structure (def: (= reference sample) + (text/= (%/reveal reference) + (%/reveal sample))))) + (def: hash + (|>> %/reveal + (:: text.Hash hash))))) + + (def: password + %/conceal)))))) + +(context: "Policy labels." + (do @ + [#let [Password<%>0 (Password<%> 0)] + raw-password (r.ascii 10) + #let [password (:: Password<%>0 password raw-password)]] + ($_ seq + (test "Can work with private values under the same label." + (and (:: Password<%>0 = password password) + (n/= (:: text.Hash hash raw-password) + (:: Password<%>0 hash password)))) + ## TODO: Figure out some way to test type-checking + ## failures, so the following code can be tested, instead + ## of being commented out. + ## (let [Password<%>1 (Password<%> 1)] + ## (test "Cannot mix labels." + ## (:: Password<%>1 = password password))) + ))) + +(context: "Structures." + (do @ + [#let [duplicate (: (-> Text Text) + (function (_ raw) (format raw raw))) + Password<%>0 (Password<%> 0)] + raw-password (r.ascii 10) + #let [password (:: Password<%>0 password raw-password)] + #let [check (:: Password<%>0 = + (:: Password<%>0 password (duplicate raw-password))) + (^open "@/.") @.Functor + (^open "@/.") @.Apply + (^open "@/.") @.Monad]] + ($_ seq + (test "Can use Functor." + (check (@/map duplicate password))) + (test "Can use Apply." + (check (@/apply (@/wrap duplicate) password))) + (test "Can use Monad." + (check (do @.Monad + [raw-password' (:: Password<%>0 password raw-password)] + (wrap (duplicate raw-password'))))) + ))) -- cgit v1.2.3