lack of labels in singularity

[Deian Stefan]

Re-posting discussion with Tahsin:

 

I am wondering whether Singularity systems have the ability to enforce information flow control policies. 

 

It seems that it has fine granular access control through channels and capabilities. But are they sufficient to restrict information flow control?  For example, can a superuser on a singularity system use his privileges to get access to other users' files?
I would like to hear some thoughts on this subject.

In the general case, I don't think so.  First, the linear type system is not enough to enforce something like: after reading from channel A, do not write to channel B.  Second, passing channel end-points over channels makes it hard to reason about transitivity.  Third, the manifest-based approach, as is, is not really friendly to DIFC policies.

That said, I think that the number of changes required to enforce IFC in Singularity is pretty low. The fact that you have non-interference* when you don't have access to any contracts is a huge win. What's left? If you want dynamic IFC: associate a label with every SIP and channel (and make sure that reads are reflected in the SIP label and writing to a channel performs a label check) -- it seems like they already have some functionality in place to do this (section 3.6). To enforce static IFC policies: I'm not sure what the full Sing# looks like, but it's plausible that you can do static analysis to enforce a security type system similar to Jif -- I imagine that the linear type system and contracts will allow for programs that would not otherwise be permitted by more-traditional systems. (In fact, some work on static IFC systems based on pi-calculus rely use similar ideas.)

* Non-interference would basically state that two SIPs cannot influence each other.