monads, modules, sandboxes
Warning: pseudo-caml below since I don't know Haskell too well. But in trying to learn I came across interesting concept of monad, and that is what inspired the following idea. I would just like to know if anyone thinks it's interesting and if someone has already developed it. Inspired by monads, I had the following idea for controlled sandboxing of an application. I'll give you a very concrete scenario, but maybe it isn't the most interesting use of idea. I download a program off the Internet that claims to do some interesting transformation on my data. But I don't trust the application not to send my secret data back to the web site. I could achieve this by running the program in a sandbox that doesn't allow it to send data over the Internet. But maybe the program has legitimate reasons to send data, e.g., the company charges based on how much data I transform, so the program wants to periodically send messages to the web site saying it performed some units of work. The idea is just that if my data has type t, instead of a program of type t -> t, the website provides a program of type m -> m written in a monadic style. Actually m = t, and the bind operation (>>=) is trivial. But it is run in the sandbox. Here is pseudo-code, where MYDATA is thought of as a well-known signature of a well-known standard, like JPEG or something, with standard implementation MyData (though I could change MyData as long as I think my changes won't break the code I got off the web site) and DataTransformer is the untrusted code from the web site. In some applications, probably you could get away with just bind and return, but for the example I give here, the untrusted code needs a way to find out if the data is done being transformed. I implement that by providing an is_done function, but note that this could be a security hole. A safer way might be to have really_do_100_steps throw an exception when it finishes that would be caught by bind. module MyData = struct type t = ... type m = t let (>>=) mm f = try run_in_sandbox (fun _ -> f mm) with _ -> failwith "gotcha" let return x = x (* functions that only run in the sandbox *) ... things that take t's ... (* functions that can run outside the sandbox *) let is_done = ... ... other things that take m's ... end module type MYDATA = sig type t = ... type m val (>>=) : m -> (t -> m) -> m val return : t -> m is_done : m -> bool ... other stuff ... end module DataTransformer = struct let really_do_100_steps x = ... let do_100_steps x = x >>= (function y -> return (really_do_100_steps y)) let rec doit x = bill_customer_for_100_steps (); let x' = do_100_steps x in if is_done x' then x' else doit x' end _________________________________________________________________ Join the worlds largest e-mail service with MSN Hotmail. http://www.hotmail.com
Daniel Crealer writes:
I came across interesting concept of monad, and that is what inspired the following idea. I would just like to know if anyone thinks it's interesting and if someone has already developed it.
Yes it is interesting, and the fact that you thought of it might mean you have valuable "insight skills" in computing. Similar ideas are already in circulation --since the 70s in the research OS community in fact-- but dressed not in the guise of the monad but rather in the guise of something called a capability as in "capability OSes" like GNOSSIS, KeyKOS, Extremely-Reliable OS, etc, or "capability PLs" like Hewitt's Actors framework, Joule, Mozart/Oz, E and --lately-- dozens of others. A capability is essentially a pointer that is unforgeable because of care taken in implementing the OS or the language runtime. Note that there is something in Unix called a capability which is not a "real" capability and which you can safely ignore.
I download a program off the Internet that claims to do some interesting transformation on my data. But I don't trust the application not to send my secret data back to the web site. I could achieve this by running the program in a sandbox that doesn't allow it to send data over the Internet. But maybe the program has legitimate reasons to send data, e.g., the company charges based on how much data I transform, so the program wants to periodically send messages to the web site saying it performed some units of work.
This is a standard application of capabilities; the downloaded program is said to be "confined" by the local OS or runtime. Unfortunately I am unwilling at this time to learn enough Caml to decipher your pseudo-Caml. If you learn enough Haskell to rewrite it in Haskell I'll take a look. The reason capabilities can do such things as confinement is that they are "totalitarian" in the sense that going through a capability is the *only* way for the programmer to access or consume some interesting set of resources. (In fact, capability OSes and runtimes are carefully audited by security engineers to ensure that property.) Like capabilities, monads can easily be made "totalitarian". In fact, modulo functions with "unsafe" in their name and modulo (the kludge of) semi-closed handles and modulo unintentional "security holes" and modulo maybe one or two other warts I'm not recalling right now, Haskell and GHC's IO monad already is "totalitarian" with respect to most side effects, eg, almost all I/O. While many have suspected a similarity between monads and capabilities, no one to my knowledge has worked out even in principle how to do security engineering of software with monads (so we could be wrong about the similarity). I am uninterested in following up on this similarity, and most capability experts prefer dynamically typed OOPLs in the Smalltalk tradition though in the past a language in the Prolog tradition was used. It is easy to get the impression that OOP is sort of stupid. That's what I thought till I discovered capability PLs. I now think the body of ideas around capability PLs (again mostly dynamically-typed OOPLs these days) is likely to be richer and more scientifically fertile for the long term than FP even. Right now, mostly only security engineers know about it as it is the technically superior way to construct "unhackable" software, but it deserves more attention from computer science researchers. I'm concentrating on on FP for essentially social and economic reasons, not technical superiority to the capability-PL approach. by "social" reason I mean mainly that it is easier to spot (and ignore!) the low-IQ programmers on FP mailing lists whereas on, eg, the average OOP mailing list or newsgroup the low-IQ folks waste a lot of your time. (But the E mailing list mentioned below has a very very bright membership.) A point of intersection between capability PLs and FPLs is that both have been used to formalize financial contracts. Also, E is the only language I know of besides the FPLs where the standard variable-binding construct, namely def foo := bar, introduces an "immutable" variable, namely foo. An "immutable" variable is one that cannot later be assigned a different value. even in the almost-functional language Scheme the variable, namely foo, bound by the standard variable-binding construct, namely (let ((foo bar)) body), can be mutated, namely by (set! foo bar2), and Scheme has no alternative to the let special form that can produce an immutable variable. (In E, there's another construct, namely var foo := bar, that will introduce a mutable variable.) The motivation for E's offering immutable variables is not the standard FP motivation of referential transparency but rather the observation that they make it easier for the programmer to avoid the unintentional creation of certain classes of security holes. The best place on the 'Net to learn about capabilities is on the mailing list (which is at least twice as busy as the Haskell mailing list BTW) for the E programming language at http://www.eros-os.org/pipermail/e-lang/. If you post to this mailing list, please tell them I sent you! I participated on this list till earlier this month. Finally, my favorite intros to capability thinking are: <LI><a href="http://mumble.net/jar/pubs/secureos/">Rees's 1995 paper "Security Kernel"</a> <LI><a href="http://www.sims.berkeley.edu/~ping/sid/ideus.html#design">Design of a Secure Desktop Interface, chapter 5 of Ping's draft paper.</a> -- Richard Uhtenwoldt "It's a mammal thing; you wouldn't understand."
Richard Uhtenwoldt <ru@river.org> writes:
Similar ideas are already in circulation --since the 70s in the research OS community in fact-- but dressed not in the guise of the monad but rather in the guise of something called a capability as in "capability OSes" like GNOSSIS, KeyKOS, Extremely-Reliable OS, etc, or "capability PLs" like Hewitt's Actors framework, Joule, Mozart/Oz, E and --lately-- dozens of others.
A recent PhD from University of Utah looked at what Java's type system has to offer in achieving security: http://www.cs.utah.edu/~gback/ http://www.cs.utah.edu/flux/papers/redline-hotos7-base.html http://www.cs.utah.edu/flux/papers/kaffeos-osdi00-base.html There are many interesting things in these papers (I'd start with the redline paper) but one of the things I learnt was the differences between protection mechanisms in OSs (e.g., capabilities) and what type systems generally offer. One of the main differences is this: Capabilities in OSs can often be revoked asynchronously (e.g., permissions for a page of virtual memory can be changed by the kernel without the process requesting the change first) whereas capabilities implemented via typesystems in programming languages often can't be revoked asynchronously. (Not all OS capabailities can be asynchronously revoked though. For example, one can view a file descriptor as a form of capability but in most Unix kernels changing file permissions does not revoke existing file descriptors.) Indeed, a straightforward encoding of 'capabilities' in a typesystem might not even support _synchronous_ revocation. David Walker's 'capability typesystem' (as used in Vault and Cyclone) is a notable exception to this rule. A potential difference (which Richard Uhtenwoldt hints at) is that it can be hard to control the flow of OS capabilities as the capability is passed from one process to another to another. This gets especially tricky when you want policies like 'X can either read files or use the network but not both' (so X cannot leak secrets learnt from the filesystem). I think this is why capability OSs have fallen out of favour in the OS community. I suspect that typesystems are better able to express and enforce these policies.
While many have suspected a similarity between monads and capabilities, no one to my knowledge has worked out even in principle how to do security engineering of software with monads (so we could be wrong about the similarity).
A possible base on which to explore this is Chih-Ping Chen's and Paul Hudak's work on the relationship between linear types and monads: 3rd bullet item on http://www.cs.yale.edu/homes/hudak-paul.html
It is easy to get the impression that OOP is sort of stupid. That's what I thought till I discovered capability PLs. I now think the body of ideas around capability PLs (again mostly dynamically-typed OOPLs these days) is likely to be richer and more scientifically fertile for the long term than FP even. Right now, mostly only security engineers know about it as it is the technically superior way to construct "unhackable" software, but it deserves more attention from computer science researchers.
Can you say more about why you think OOP works better in this regard? Is it because: - classes are ADTs - the only way to act on them is via methods (I'm ignoring most C++ features and public Java fields here) - you can force people to execute security checks every time they access an object (thus making it possible to asynchronously revoke a capabaility) ? Or for some other reason? -- Alastair Reid alastair@reid-consulting-uk.ltd.uk Reid Consulting (UK) Limited http://www.reid-consulting-uk.ltd.uk/alastair/
participants (3)
-
Alastair Reid -
Daniel Crealer -
Richard Uhtenwoldt