blob: ad85ae679cc1f26f900f91ea68f854bfa309403e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
|
(.module:
[lux #*
[control
[functor (#+ Functor)]
[apply (#+ Apply)]
[monad (#+ Monad)]]
[type
abstract]])
(abstract: #export (Private value label)
{#.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 by 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
(type: #export (Close label)
(All [value] (-> value (Private value label))))
(type: #export (Open label)
(All [value] (-> (Private value label) value)))
(signature: #export (Privilege label)
(: (Close label)
conceal)
(: (Open label)
reveal))
(def: Privilege<_>
Privilege
(structure (def: conceal (|>> :abstraction))
(def: reveal (|>> :representation))))
(type: #export (Delegation from to)
(All [value] (-> (Private value from) (Private value to))))
(def: #export (delegation open close)
(All [from to] (-> (Open from) (Close to) (Delegation from to)))
(|>> open close))
(type: #export (Context scope label)
(-> (Privilege label)
(scope label)))
(def: #export (with-privacy context)
{#.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 [scope]
(Ex [label]
(-> (Context scope label)
(scope label))))
(context ..Privilege<_>))
(def: (privatize constructor)
(-> Type Type)
(type (All [label] (constructor (All [value] (Private value label))))))
(structure: #export Functor<Private>
(:~ (privatize Functor))
(def: (map f fa)
(|> fa :representation f :abstraction)))
(structure: #export Apply<Private>
(:~ (privatize Apply))
(def: functor Functor<Private>)
(def: (apply ff fa)
(:abstraction ((:representation ff) (:representation fa)))))
(structure: #export Monad<Private>
(:~ (privatize Monad))
(def: functor Functor<Private>)
(def: wrap (|>> :abstraction))
(def: join (|>> :representation)))
)
|
