a monad for secret information
I finally (think I) understand monads well enough to make one up:
module Secret (Secret, classify, declassify) where
data Secret a = Secret a
classify :: a -> Secret a classify x = Secret x
declassify :: Secret a -> String -> Maybe a declassify (Secret x) "xyzzy" = Just x declassify (Secret x) _ = Nothing
instance Monad Secret where return = classify (Secret x) >>= f = f x
The nice thing about this is that (correct me if I'm wrong) clients of the module can't sneak information out of the monad without either using the right password or by using one of the unsafe*IO methods. (Or by running the program in a debugger. But you get the idea.) The not-so-nice thing is that the literal text of the password is baked into the data definition. I'd like to have a more general version of Secret that allows someone to pass the password in when constructing a secret, and preserves that password when "return" is used, but doesn't let the second argument of (>>=) see the password. Something like this:...
data Classification pw a = Classification pw a declassify (Classification pw a) pw' = case pw' of pw -> Just a _ -> Nothing
type Secret = Classification "xyzzy"
...but that doesn't parse. Is it even possible to have a type like this that still observes the monad rules? Is this the sort of thing that I need to understand arrows to pull off?
On 09/10/06, Seth Gordon
I finally (think I) understand monads well enough to make one up:
module Secret (Secret, classify, declassify) where
data Secret a = Secret a
classify :: a -> Secret a classify x = Secret x
declassify :: Secret a -> String -> Maybe a declassify (Secret x) "xyzzy" = Just x declassify (Secret x) _ = Nothing
instance Monad Secret where return = classify (Secret x) >>= f = f x
The nice thing about this is that (correct me if I'm wrong) clients of the module can't sneak information out of the monad without either using the right password or by using one of the unsafe*IO methods. (Or by running the program in a debugger. But you get the idea.)
The not-so-nice thing is that the literal text of the password is baked into the data definition. I'd like to have a more general version of Secret that allows someone to pass the password in when constructing a secret, and preserves that password when "return" is used, but doesn't let the second argument of (>>=) see the password. Something like this:...
data Classification pw a = Classification pw a declassify (Classification pw a) pw' = case pw' of pw -> Just a _ -> Nothing
type Secret = Classification "xyzzy"
...but that doesn't parse.
Is it even possible to have a type like this that still observes the monad rules? Is this the sort of thing that I need to understand arrows to pull off?
Why not just: secret :: a -> Classification String a secret = Classification "xyzzy" The password string isn't part of the type, it doesn't even necessarily exist at compile time. You might have just got confused between type and data constructors for a moment.
Cale Gibbard wrote:
Why not just:
secret :: a -> Classification String a secret = Classification "xyzzy"
The password string isn't part of the type, it doesn't even necessarily exist at compile time. You might have just got confused between type and data constructors for a moment.
But now I want to be able to process the secret monadically: mySecret = secret "Jimmy Hoffa is buried under the 50-yd line in the Meadowlands" do secretData <- mySecret return (length secretData) How do I define "return" so that it will put the password back, and how do I define "(>>=)" so that the password won't be accessible within the do-block?
Hi,
I'm not sure what you are after, but:
data Secret a = Secret {password :: String, value :: a}
classify :: String -> a -> Secret a
classify = Secret
declassify :: String -> Secret a -> Maybe a
declassify guess (Secret pw v) | guess == pw = Just v
| otherwise = Nothing
Put that in a module, do not export the Secret data type, and you're
good to go. I'm unsure what a Monad is giving you....
Thanks
Neil
On 10/10/06, Seth Gordon
Cale Gibbard wrote:
Why not just:
secret :: a -> Classification String a secret = Classification "xyzzy"
The password string isn't part of the type, it doesn't even necessarily exist at compile time. You might have just got confused between type and data constructors for a moment.
But now I want to be able to process the secret monadically:
mySecret = secret "Jimmy Hoffa is buried under the 50-yd line in the Meadowlands"
do secretData <- mySecret return (length secretData)
How do I define "return" so that it will put the password back, and how do I define "(>>=)" so that the password won't be accessible within the do-block? _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
data Secret a = Secret {password :: String, value :: a}
classify :: String -> a -> Secret a classify = Secret
declassify :: String -> Secret a -> Maybe a declassify guess (Secret pw v) | guess == pw = Just v | otherwise = Nothing
Put that in a module, do not export the Secret data type, and you're good to go. I'm unsure what a Monad is giving you....
I was just curious if I could do that within a monad. If the answer to my question is "no, you can't", then I'll pick up the shattered pieces of my life and move on. :-)
On Oct 10, 2006, at 12:04 PM, Seth Gordon wrote:
data Secret a = Secret {password :: String, value :: a}
classify :: String -> a -> Secret a classify = Secret
declassify :: String -> Secret a -> Maybe a declassify guess (Secret pw v) | guess == pw = Just v | otherwise = Nothing
Put that in a module, do not export the Secret data type, and you're good to go. I'm unsure what a Monad is giving you....
I was just curious if I could do that within a monad.
If the answer to my question is "no, you can't", then I'll pick up the shattered pieces of my life and move on. :-)
I think you can. Your original monad is just a little too simplistic. Try something like this (untested): import Control.Monad.State type Password = String type Secret s a = State (Password -> Maybe s) a classify :: Password -> s -> Secret s () classify pw s = put (\x -> if x == pw then Just s else Nothing) declassify :: Password -> Secret s (Maybe s) declassify pw = get >>= \f -> return (f pw) runSecret :: Secret s a -> a runSecret m = runState m (const Nothing) Note how this relies on "opaque" functions to hide the secret. This wouldn't work if Haskell had intensional observation of functions, although you could still use a newtype in that case. Slightly related: I've sometimes wondered about a monadic API for cryptographic primitives. With compiler support you could do nifty things like make sure to use non-swappable memory for encryption keys and use fancy special purpose hardware for cryptographic primitives, if available. The API would give a nice way to ensure proper information hiding policy. Has anything like this been done or studied? Rob Dockins Speak softly and drive a Sherman tank. Laugh hard; it's a long way to the bank. -- TMBG
On Mon, Oct 09, 2006 at 11:06:35PM -0400, Seth Gordon wrote:
I finally (think I) understand monads well enough to make one up: [...] The not-so-nice thing is that the literal text of the password is baked into the data definition. I'd like to have a more general version of Secret that allows someone to pass the password in when constructing a secret, and preserves that password when "return" is used, but doesn't let the second argument of (>>=) see the password. Something like this:...
data Classification pw a = Classification pw a declassify (Classification pw a) pw' = case pw' of pw -> Just a _ -> Nothing
type Secret = Classification "xyzzy"
Try
module Secret (Secret, classify, declassify) where
data Secret a = Secret String a
classify :: String -> a -> Secret a classify pw x = Secret pw x
declassify :: Secret a -> String -> Maybe a declassify (Secret pw x) pw' | pw' == pw = Just x declassify (Secret _ _) _ = Nothing
instance Monad Secret where return = classify "" (Secret pw x) >>= f = case f x of Secret _ y -> Secret pw y
Now return itself doesn't assign a password, but you can classify something manually, and then perform computations on that data in a safe manner. It's just as safe as your code, because the constructor of secret is hidden which hides the password just as well as the data. Of course, this is run-time checking, and you'd be safer with a phantom type-level password which is statically verified, which is also doable, but not so easily. It wouldn't be very hard either, though. It also wouldn't be Haskell 98. David
David Roundy wrote:
Try
module Secret (Secret, classify, declassify) where
data Secret a = Secret String a
classify :: String -> a -> Secret a classify pw x = Secret pw x
declassify :: Secret a -> String -> Maybe a declassify (Secret pw x) pw' | pw' == pw = Just x declassify (Secret _ _) _ = Nothing
instance Monad Secret where return = classify "" (Secret pw x) >>= f = case f x of Secret _ y -> Secret pw y
Now return itself doesn't assign a password, but you can classify something manually, and then perform computations on that data in a safe manner. It's just as safe as your code, because the constructor of secret is hidden which hides the password just as well as the data.
What should 'q >>= r' mean, when 'q' and 'r x' are secrets with different passwords? In the code above, the result is a secret with the same password as 'q'. This allows you to declassify any secret without knowing its password: break :: Secret a -> a break q = fromJust $ declassify (classify "bloep" () >> q) "bloep" . -- Mr. Pelican Shit may be Willy. ^ /e\ ---
David Roundy wrote:
Try
module Secret (Secret, classify, declassify) where
data Secret a = Secret String a
classify :: String -> a -> Secret a classify pw x = Secret pw x
declassify :: Secret a -> String -> Maybe a declassify (Secret pw x) pw' | pw' == pw = Just x declassify (Secret _ _) _ = Nothing
instance Monad Secret where return = classify "" (Secret pw x) >>= f = case f x of Secret _ y -> Secret pw y
That's just the sort of thing I was looking for. Thanks! Arie Peterson wrote:
What should 'q >>= r' mean, when 'q' and 'r x' are secrets with different passwords? In the code above, the result is a secret with the same password as 'q'. This allows you to declassify any secret without knowing its password:
Yeah, but I think that's easy to fix: make classify and declassify take a set of strings rather than a single string, and then make >>= return a secret containing the union of passwords on both sides.
2006/10/10, David Roundy
declassify :: Secret a -> String -> Maybe a declassify (Secret pw x) pw' | pw' == pw = Just x declassify (Secret _ _) _ = Nothing
Why does this works? "Yet Another Haskell Tutorial" teaches that pattern matching occurs at one stage and guard processing at other, and that there's no back (page 94). -- Felipe.
Hello Felipe, Wednesday, October 11, 2006, 4:47:59 AM, you wrote:
Why does this works? "Yet Another Haskell Tutorial" teaches that pattern matching occurs at one stage and guard processing at other, and that there's no back (page 94).
something is definitely wrong - either book or your understanding. it's very widely used feature, i just took a quick scan of Hugs Prelude and found a lot of its uses: (!!) :: [a] -> Int -> a xs !! n | n<0 = error "Prelude.!!: negative index" [] !! _ = error "Prelude.!!: index too large" (x:_) !! 0 = x (_:xs) !! n = xs !! (n-1) lexmatch (x:xs) (y:ys) | x == y = lexmatch xs ys lexmatch xs ys = (xs,ys) showLitChar c | c > '\DEL' = showChar '\\' . protectEsc isDigit (shows (fromEnum c)) showLitChar '\DEL' = showString "\\DEL" x ^ 0 = 1 x ^ n | n > 0 = .... _ ^ _ = error "Prelude.^: negative exponent" i don't even say that i use this feature every day :) -- Best regards, Bulat mailto:Bulat.Ziganshin@gmail.com
Seth Gordon wrote:
I finally (think I) understand monads well enough to make one up: ... Is it even possible to have a type like this that still observes the monad rules? Is this the sort of thing that I need to understand arrows to pull off?
I think the monads people have given you will work. I even think the monadic formulation helps, in allowing you to calculate derived data while keeping the results classified as well. If you want some fancier information flow policies (falling back to arrows), check out "Encoding Information Flow in Haskell": /www.cis.upenn.edu/~stevez/papers/LZ06a.pdf/ (by Steve Zdancewic and Peng Li, also authors of "A Language-based Approach to Unifying Events and Threads http://www.cis.upenn.edu/%7Estevez/papers/LZ06b.pdf") Brandon
participants (9)
-
Arie Peterson -
Brandon Moore -
Bulat Ziganshin -
Cale Gibbard -
David Roundy -
Felipe Almeida Lessa -
Neil Mitchell -
Robert Dockins -
Seth Gordon