| Safe Haskell | None |
|---|
Data.Faceted
Description
Faceted values with faceted execution
Inspired by Thomas H. Austin and Cormac Flanagan, "Multiple Facets for Dynamic Information Flow."
A faceted value < k ? V_H : V_L> is a triple consisting of a principal k and two values V_H and V_L.
Intuitively, this faceted value appears as V_H to private observers that can view k’s private data,
and as V_L to other public observers. We refer to V_H and V_L as private and public facets, respectively.
This module supports intuitive syntax suger by (?) and (.:) operators.
Use (??) operator instead of (?) when you declare nested faceted values.
In this module, principal is modeled by (ctx -> Bool).
Returning True means ctx is a private observer, False means it is a public observer.
(x -> x > 0) ? 1 .: 0 (x -> x > 0) ?? ((y -> y > 1) ? 4 .: 3) .: ((z -> z < 2) ? 2 .: 1)
To observe faceted value, use observe or runFaceted function.
When observing faceted values, returning True means that the observer is private one, False means public one.
observe ((x -> x =="Me") ? 1 .: 0) "Me" 1 observe ((x -> x ==Me) ? 1 .: 0) "SomeOne" 0
- type Faceted ctx a = Free (Facets ctx) a
- (?) :: (ctx -> Bool) -> (a, a) -> Faceted ctx a
- (??) :: (ctx -> Bool) -> (Faceted ctx a, Faceted ctx a) -> Faceted ctx a
- (.:) :: a -> a -> (a, a)
- constF :: a -> Faceted ctx a
- principal :: Facets ctx val -> ctx -> Bool
- runFaceted :: Faceted ctx a -> ctx -> a
- observe :: Faceted ctx a -> ctx -> a
Documentation
type Faceted ctx a = Free (Facets ctx) aSource
Type for Faceted Value: < k ? V_H : V_L>
Please Note that this type utilizes Free.
(?) :: (ctx -> Bool) -> (a, a) -> Faceted ctx aSource
Constructor for unnested faceted values
(x -> x > 0) ? 2 .: 1
The value in (?) operator will be treated as values in this faceted value.
This means that Faceted ctx (Faceted ctx b) can be possible.
Note that Faceted ctx (Faceted ctx b) is essentially different from nested faceted values.
(??) :: (ctx -> Bool) -> (Faceted ctx a, Faceted ctx a) -> Faceted ctx aSource
Constructor for nested faceted values
(x -> x > 0) ?? ((y -> y > 1) ? 4 .: 3) .: ((z -> z < 2) ? 2 .: 1)
constF :: a -> Faceted ctx aSource
(constF a) is equivalent with (const True) ? a .: a
This would be useful when you declare like below:
( "Me" ?? (constF myLocation) .: "CoWorker" ? "Office" .: "In the City")
runFaceted :: Faceted ctx a -> ctx -> aSource
Evaluator for faceted values. Its semantics is faceted execution denoted in the paper above.
observe ((x -> x =="Me") ? 1 .: 0) "Me" 1 observe ((x -> x ==Me) ? 1 .: 0) "SomeOne" 0