monads, modules, sandboxes

[Richard Uhtenwoldt]

this will be my last message on this topic as I need to stop
reading this list for a few months.

Alastair Reid writes:

>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.

seems to me capabilities can do that:

you just pass to X a capability (pointer) to an object that will
return either a read-only capability to the filesystem or a capability
to the network inferface but not both.

either that or use the revocable-capability pattern twice in such a
way that before the first network access happens, the
filesystem capability is revoked and before the first filesystem read
happens the network access capability is revoked.

to flesh out that first alternative a little, the object passed to X
could probably be coded up by modifying the following E language
function (found at http://www.erights.org/elang/concurrency/race.html)
for making "use-once" capabilities.  and yes I realize this code is
not exactly the essence of conciseness and brevity.

>   A "once" of a function is a use-once version of that function. Ie,
>   "once(func)" returns a object that will forward no more than one "run"
>   message to "func". The two argument form "once(verb, target)" is a
>   generalization which will forward no more than one "verb" message to
>   the target.
>
>   For the Miranda Methods, the result of the once (the forwarder
>   below) must make good decisions about whether to override them and
>   possibly forward them, or not override them and let them default to
>   methods on the forwarder. For non-Miranda methods other than the
>   suppressed method, they are simply forwarded.
>
> def once {
>     to (verb, target) :any {
>         var used := false
>         def forwarder {
>             # use the Miranda order/3, though it shouldn't matter
>
>             # use the Miranda optSealedDispatch/1 to protect the target
>
>             # forward getAllegedType/0, though one could argue that, once
>             # used up, the type shouldn't include the supressed verb
>             to getAllegedType() :any {
>                 target getAllegedType()
>             }
>
>             # forward respondsTo, but supress verb.  One could argue that res
pondsTo
>             # and getAllegedType() should be consistent with each other.
>             to respondsTo(verb2, arity) :boolean {
>                 verb != verb2 && target respondsTo(verb2, arity)
>             }
>
>             # forward printOn/1
>             to printOn(out) { target printOn(out) }
>
>             # forward reactToLostClient
>             to reactToLostClient(problem) {
>                 target reactToLostClient(problem)
>             }
>
>             # use the Miranda whenMoreResolved/1 to protect the target
>
>             # use the Miranda whenBroken/1 to protect the target
>
>             # use the Miranda yourself/0 to protect the target
>
>             # handle all other messages
>             match [verb2, args] {
>                 if (verb == verb2) {
>                     if (used) {
>                         throw("used up")
>                     }
>                     used := true
>                 }
>                 E call(target, verb2, args)
>             }
>         }
>     }
>
>     # default to suppressing "run"
>     to (target) :any { once("run", target) }
> }

what follows is not so much an explanation as a series of disconnected
points that a bright and motivated reader might infer real knowledge
from.

point 1.  I observe that type-systems work is very abstract and
formal and if I were doing a type system for secure programming I
would definitely look to the capability literature for conceptual
guidance.  too easy when doing formal work to lose sight of where the
juicy "wins" (opportunities) lie and more generally to lose sight of
the economic and social implications of the technical work and to
start playing a sterile "glass bead game".

insight and vision is where the capability literature is very fertile.
here I'm speaking of the capability PL literature (much of which is
ultimately based on Hewitt) not the older capability OS literature (eg
Butler Lampson's paper from the early 1970s) which is all intertwined
with hairy OS implementation issues and takes forever to learn, it
seems to this languages geek.

point 2.  Alastair Reid writes:

>>  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.
>
>Can you say more about why you think OOP works better in this regard?
>Is it because:

>- the only way to act on them is via methods (I'm ignoring most
>  C++ features and public Java fields here)

that is one of the things I like.  on the E language list they say
that certain languages have the AYCDISAM -- All You Can Do Is Send A
Message -- property, which means you can always interpose a new object
of arbitary behaviour between any two extant objects --a next level of
modularity beyond the ADT.  many capability PLs have the AYCDISAM
property.

the question comes up under AYCDISAM of how can you ever be sure you
are talking to the real Bank of America (say) when there can be an
arbitrary number of objects on the Network between you and the thing
you think is the Bank of America object.  note that simply asking a third
object, eg, the Federal Reserve object, simply moves the problem.

the solution is all elegant and subtle.
in fact, ISTR it took bright folk years to figure out.

"took years to figure out" is a big turn off to practical programmers,
but to me, who would rather be a theoretical physicist than a
programmer except programming is more economically important, it is a
reccommendation when I can learn relatively few very subtle concepts
(of the quality that they took years for a bright group to figure out)
rather than many many many tedious uninspiring  ungeneralizable details
as in say most Linux software.

point 3.  I judge that it would be much easier (than say
Linux)  to be the system administrator of a complex "software
environment" written to capability principles.   you have more
control over the environment because each individual software package
(each of which is a kind of "guest of the system admin") has less
control.  for more see http://cap-lore.com/CapTheory/Politics.html

point 4.   the intellectual framework that underlies much of the 
capability PLs --Hewitt's Actors model -- is protean enough
so that people have written articles that "redo" much of *physics*
in Actors terminology and primitives.  such protean-ness speaks
well for fertility.


in summary, I plan to keep on concentrating on the pure FP world
because I calculate that it is more certain to gain (slowly: FP is not
the Internet of 1993 by a long shot) in economic importance than the
capability PL world is.

the capability (PL and OS) stuff is either going to explode or remain
obscure with obsure being the more likely fate next 6 years, and that
makes for unreliable career planning.  oh how cynical I have become!

-- 
Richard Uhtenwoldt
"It's a mammal thing; you wouldn't understand."