[cap-talk] Information Flow in Object-Capability Systems

Toby Murray toby.murray at comlab.ox.ac.uk
Tue Mar 31 04:50:07 EDT 2009


Hi cap-talk,

I recently submitted a paper to CSF, "Information Flow in
Object-Capability Systems", which was unfortunately rejected. I thought
it would be useful to post the paper at this point to solicit feedback
for improvement and to gain some further context on the reviews it
received. 

The paper can be found here:
http://web.comlab.ox.ac.uk/people/toby.murray/tmp/infoflow_capsystems.pdf

The reviews are appended to this email.

I have some suspicion that the first reviewer is on-list. If that's the
case, I'd very much like to take him or her up on their offer to further
explain the points raised in their review. 

In particular 
- how SCOLL could be used to detect the covert channels detected by the
approach in the paper, including how it can deal with the sorts of
concurrency that exist in all known object-capability operating systems
(the focus of this paper).  
- what is meant by the comments on E order etc. I thought I understood
all that stuff OK but I guess I don't because I can't see how this is
relevant to the context on which this paper is focused, ocap OSes with
synchronous messaging like seL4 or KeyKOS.
- whether the paper contain other misconceptions or misrepresentations
aside from its treatment of SCOLL.

Without wanting to enter into a debate, allow me to apologise to the
reviewer for misrepresenting SCOLL's capabilities in the paper. Space
restrictions prevented me from covering SCOLL in more detail, forcing me
to equate its capabilities with what were demonstrated in Fred's thesis
in the context of the analysis of this data diode pattern -- i.e. to
equate its capabilities with what had been publicly demonstrated in the
application area I was focused on. I should also thank them for pointing
me to other related work of which I should have been aware. I've got
some reading to do.

My thanks in advance for all and any feedback. I'd like to fix the
objections raised to this paper and resubmit somewhere else. 

Cheers

Toby


---------------------------------------------

Paper: 1
Title: Information Flow in Object-Capability Systems


-------------------- review 1 --------------------

PAPER: 1
TITLE: Information Flow in Object-Capability Systems
    

In this paper the author presents a solid and well founded CSP-based
formal analysis of the *-property (MLS) in object-capability systems,
that covers both overt and (some) covert channels. The paper shows that
this approach is useful when building systems that provide abstractions
for access control such as actual object capability systems. The work
relates to the Scoll approach, which it claims to extend in several
ways.
Note that where the paper refers to "covert" channels in general, it
largely focusses on the storage channels emerging in concurrent systems
that support shared state.
While the content of the paper is interesting, formally sound, and to a
considerable degree also new, the author seems to confuse its actual
contributions in respect to related work. The paper fails to mention and
situate the relevant work of others on data-flow analysis that was done
outside the specific context of capabilities, more specifically the work
about non-interference in a general language-based context.  The concept
called "Information flow by causation or prevention" is largely covered
under different names in existing work on language-based information
flow for concurrent languages, for instance by Sabelfeld, Myers, and
others that are active in that field. This paper thus effectively
applies established non-interference results from data-flow research to
object-capability systems, which is OK and valid and represents a
valuable contribution, but it should be explicitly situated in this
context.
Moreover,  the author's following explicit claims about the approach of
Spiessens (Scoll) are incorrect:
- that it covers only capability propagation
- that it is not suitable for covert (in-model, causal) data-flow
analysis
- that it cannot precisely model (a-synchronous)
concurrency-with-shared-state  (two facets of an object-capability
accessing a shared but otherwise encapsulated state)
Some of these incorrect assumptions may have been inappropriately
extrapolated from a simple example about Boebert's conjecture in
Spiessen's thesis, where the analysis is indeed restricted to overt
message-based communication.
The author claims that buffered data-diodes (concurrent facets with
shared state) would be the "natural" way to implement data-diodes in
(a-synchronous) concurrent systems. That claim can be contradicted by
example.  Simply stateless, message-forwarding capabilities for either
reading or writing to a file capability (via synchronous or
a-synchronous message passing) can be provided in many languages. Such
simple forwarding-capabilities are immune to plan-interference if the
language's concurrency mechanism respects the causal order of messages,
like E does (explained in Miller's "Robust Composition"). Of course, the
author considers building object-capability systems rather than
programming languages, but then:
- either an E-like causal order should be imposed to the asynchronous
messages at the OS level (which is fairly easy to do)
- or else the state should be shared only at the OS level and its
effects should be completely hidden to the application layers
(non-interfering).
The author provides a useful and interesting solution for the latter
approach.
Because of the many misconceptions, the paper misses the opportunity to
compare the real pro's and con's of a  CSP-based analysis versus the
Scoll-based approach, and to discover their complimentary features. Like
CSP, Scoll is a language in which many models (not just capabilities)
can be expressed and many forms of authority propagation can be
examined.  I will be glad to explain upon request, how to model the
author's problems in Scoll and how to use Scoll to find the necessary
corrections to a flawed implementation. The main differences between
both approaches may well be one of practical considerations rather than
expressive power. Scoll requires that all considered forms of authority
and causal influence be modeled explicitly before the analysis, whereas
the author's approach has no such strict requirements. That can be a
considerable advantage over Scoll is certain situations, even if it is
also a disadvantage in others.  Similarly, the inherently non-monotonic
approa!
 ch presented by the author can have considerable advantages, again in
certain situations (e.g. when conservative approximation can be
guaranteed in other ways).
Because the paper makes incorrect claims, misinterprets some related
works, and fails to consider other important related work, I cannot but
firmly reject it. However, in general I do appreciate the author's ideas
and approaches a lot, especially the clear and formal foundations that
made me understand what the author wanted to express. I therefore would
like to suggest to the author to seek deeper understanding of the
related work on data-flow interference, plan-interference, and Scoll,
and reuse the work done in an adapted version for re-submission in the
correct context. 


-------------------- review 2 --------------------

PAPER: 1
TITLE: Information Flow in Object-Capability Systems
    

This paper explores the properties of "data diodes", a mechanism
for controlling information flow in object-capability systems.
Data diodes are modeled in CSP. It's found that the original
versions of the data diode introduce an unsurprising covert channel
resulting from its mutual exclusion properties.
I found it difficult to extract from this presentation interesting new
principles or ideas. Perhaps this partly is because of the
presentation.  The paper has the flavor of a travelogue: first we try
this, then we try that. The sections even have names like "first pass"
and "second pass". Odd.
There is a lot of formalism in this paper, defining various
information flow properties, but when we get down to it, it's easy to
see why there is a covert channel. This felt like unnecessary
obfuscation. The fix also seems straightforward.  There is also no
evaluation of whether the revised mechanism is expressive enough.
I am a bit allergic to papers that present many different versions of
what secure information flow is, all with subtly different definitions
that may or may not correspond to security and accompanying text that
may or may not correspond to the formal definition.  This is one of
those papers.
The actual contribution above previous papers on this (already
rather esoteric topic) seems to be small. I'm not enthusiastic. 


-------------------- review 3 --------------------

PAPER: 1
TITLE: Information Flow in Object-Capability Systems
    

This paper investigates techniques for modeling and testing
noninterference properties for capability systems using CSP 
and its model checker FDR. It revolves around a case study for a data
diode, which nominally passes data in one 
direction only and requires use of capabilities to control access. The
paper notes, as expected, that there is a back 
channel through the diode because it has a finite (unit-size) buffer and
refuses access until the high side has emptied 
the buffer.  This channel is detected by testing (using FDR) a
particular CSP formulation of noninterference that came 
from a previous paper. A revised diode that accepts or refuses low data
input on the basis of a fixed discipline that is 
not affected by high behavior is then shown to satisfy the
noninterference property.

Although there is some interesting discussion about the NI property to
motivate it, and relate it to previous work and to 
the needs of the case study, the paper would be useful primarily to CSP
experts. The paper does not appear to provide 
general observations about the impact of capabilities on NI modeling;
capabilities are simply a detail in a particular case 
study. The work is well done but the paper is not high on novelty. 




 




More information about the cap-talk mailing list