[cap-talk] Implementing Capabilities in functional languages (esp type classes_

[David Barbour]

On Sat, Apr 16, 2011 at 12:26 AM, Ben Kloosterman <bklooste at gmail.com>wrote:

> I would like to ask what is the best way to implement capabilities in a
> type class

based language which does not  hide internals of data structures / records.


> Can we use the pair as Sandro indicated  , if its not an "oCap" what are
> its
> weaknesses.
>

Using the Pair<T,T->void> is a bad idea. Once you get two such pairs with
the same 'T' type in a subprogram, you can start crossing the streams and
get rights amplification. Unfortunately, the potential for this rights
amplification is not obvious to whomever is granting the pair.


> Can we define a type class for the cap and treat the type class as an
> interface ?
>

You can use something like:
  (Cap c) => buildMain :: Args -> c ()  -- monadic c
or
  (Cap' c) => buildProg :: c Args () -- arrow c

The monadic or arrow typeclasses provide the essential composition and
attenuation features. Any toplevel capabilities can be provided via Args. A
few reflective features might also be provided via Args (where 'reflect :: c
x -> Data') though I'd keep reflection minimal. I'm assuming that 'Cap c' is
simply shorthand for all the universally available typeclasses:

class (Monad c, HasVar c, HasSealerUnsealer c, etc.) => Cap c where
   -- just a class collection

Assuming type-families you could do stuff like:

class (Monad m) => HasVar m where
    type Var m :: * -> *  -- type family
    newVar :: a -> m (Var m a)
    readVar :: Var m a -> m a
    writeVar :: Var m a -> a -> m ()

But you can also do most such things in a pure capability manner:

-- return a reader/writer capability pair
class (Monad m) => HasVar m where
    newVar :: a -> m (m a, a -> m ())

That said, something like 'HasSealerUnsealer' is vastly cleaner to model
using a type family.

class (Monad m) => HasSealerUnsealer m where
  type Sealed m :: * -> * -- one could also add a 'Brand' phantom type here.
  newSealerUnsealer :: m (a -> Sealed m a, Sealed m a -> Maybe a)

Anyhow, careful discipline would be important. While you can build a large
capability-secure program internally to 'buildMain', you would not be
assured of maintaining any real security with external composition (i.e.
when you start combining 'buildMain' with other functions) unless they are
constructed under the same (Cap c) restriction. And you'd want to be careful
about what features are granted to buildMain via 'Args' (where Args might be
a record or powerbox of capabilities). Also, I'd certainly exclude MonadIO
from 'Cap c' - any IO should be via the Args.


> Are we forced to create some TCB ( either a module or kernel) and access
> that via a capID ?
>

No. Well, not quite. You're already assuming a TCB: the type and typeclass
system. To the extent this TCB is violated (e.g. via unsafePerformIO or
 divergence), your solution will be compromised. Still, it can be convenient
to structure programs in a capability-disciplined manner even if it isn't
truly capability-secure.


> Should we only "secure" major components like resources or should it apply
> to most data / types/modules similar or oCaps .
>

You should certainly target any security-sensitive resources or
side-effects. Among those, securing non-termination, delay, synchronization,
and allocation can be interesting to tackle, though you'd need something
much more constrained than a Monad typeclass or even Hughes's Arrows; Adam
Megacz's Generalized Arrows should work.

Beyond that, it's up to you, really. I'd suggest taming your libraries,
minimizing use of ADTs (beyond a few for language features like Sealed
values), or explicitly modeling the ADTs you do need (using
sealers/unsealers rather than the type system). Explicitly modeling ADTs is
more expressive, secure,  composable, and lowers risk of confused deputy
issues (since you need to explicitly unseal the ADT). If your type-system
isn't powerful enough to model sealed values and sealers/unsealers, though,
you'll have a lot of trouble expressing most of the richer security policies
and patterns.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.eros-os.org/pipermail/cap-talk/attachments/20110416/3c0723ae/attachment.html