[cap-talk] Announcing "Analysing Object-Capability Security" Paper and Authodox v. 0.2.0

[Toby Murray]

On Wed, 2008-05-21 at 10:33 +0200, Matej Kosik wrote:

Firstly, thanks for the latex advice Matej. I never understood the
purpose of \mathit{} until now. Cheers.

> Can you give me an example written in CSP which would model the powerbox pattern?
> 
> That is, there are two processes: Host and Guest.
> - the Guest can interact only with the Host
>   (the Guest is "invited" to the system but does not have to be fully trusted)
> - the Host can interact with the Guest and also with some other processes
> How would you express these processes so that:
> - the Host would choose some of its capabilities and send it to the Guest (in a way that noone else
> can catch it---over some private channel or something analogous)
> ?
> 

OK. I'll try to model a host, Host, passing a guest, Guest, a capability
that allows it to access a particular device, Printer1, and only that
device. The system will contain a second device, Printer2, that the
guest should not be able to access (i.e. should not be able to obtain a
capability to.)

The following script is valid machine-readable CSP that can be passed to
FDR which will verify the refinement expressed in the final "assert"
line:


-- the "datatype" statement declares an enumerated type. The name of the
-- enumerated type evaluates to a set containing the type's values
datatype Object = Host | Guest | Printer1 | Printer2 

-- we define a single data (non-capability) value, null
datatype Data = null                    

-- a parameter is either an object name (a capability) or a data value
Param = union(Object,Data)

-- in machine-readable CSP, all events must occur over some declared
channel
-- we'll use the channel 'do'. the event o1.o2.arg represents object
-- 'o1' invoking object 'o2' passing the argument 'arg'
channel do : Object.Object.Param

-- (The Host simply invokes its "guest" capability, passing its 
-- "printer1" capability with the invocation, and then stops.)
HostBehaviour(guest,printer1,printer2) = do.Host.guest.printer1 -> STOP


-- The printer, with identity me which is either Printer1 or Printer2, 
-- is defined as 
PrinterBehaviour(me) = do?any!me?arg -> PrinterBehaviour(me)
-- It simply continuously accepts artibrary invocations from anyone.

-- We'll make the guest as hostile as possible, by defining it to
exhibit 
-- maximum possible behaviour, in which it initially possesses no 
-- capabilities. The Guest is defined, thus, as GuestBehaviour({}),
where

GuestBehaviour(caps) = do?any!Guest?arg ->
GuestBehaviour(union(caps,inter(Object,{arg}))) []
                       do.Guest?target:caps?arg:union(caps,{null}) ->
GuestBehaviour(caps)


-- The system, System, is then the parallel composition of the behaviour
of
-- each object, given by the following function:
behaviour(Host) = HostBehaviour(Guest,Printer1,Printer2)
behaviour(Printer1) = PrinterBehaviour(Printer1)
behaviour(Printer2) = PrinterBehaviour(Printer2)
behaviour(Guest) = GuestBehaviour({})

-- The alphabet of each object, o, is given by alpha(o), where
alpha(o) = {do.o.other.arg, do.other.o.arg | other <- diff(Object,{o}),
arg <- Param }
System = || o:Object @ [alpha(o)] behaviour(o) 

-- We can test whether in the parallel composition (System), Guest can
-- ever obtain any capabilities other than the capability it receives
-- from Host to Printer1, by testing whether the System can ever
-- perform an event representing Guest invoking one of these other
-- capabilities,

-- i.e. whether System can ever perform an event from the set

BAD = {do.Guest.badCap.arg | badCap <- diff(Object,{Printer1}), arg <-
Param}

-- assert that System (trace) refines the most general process that
-- never performs an event from the set BAD
assert CHAOS(diff(Events,BAD)) [= System



Passing it to FDR reveals that the refinement holds, i.e. the Guest can
never obtain a capability that would allow it to invoke anything other
than Printer1.

> As it is expressed above it does not sound very exciting that scheme is very practical. I believe it
> cannot be expressed in CCS and (unless CCS and CSP are significantly different in this aspect)
> neither in CSP. Is that false? It would be a surprise for me so I would be interested to know that I
> am wrong.

I'll let you judge whether the model above meets your criteria.

Cheers

Toby