monads, modules, sandboxes

[Alastair Reid]

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/