[cap-talk] Backwater (was: Language-based OS domain separation)

[Jonathan S. Shapiro]

On Tue, 2007-06-19 at 11:10 -0700, Marc Stiegler wrote:
> Singularity's security architecture, as nearly as I can tell, is
> acls-on-steroids-leaping-new-heights-of-complexity.

That may be; I don't know. At the primitive level of inter-process
communication, it is a descriptor architecture. This is the part that
interested me about the security model.

> And It is all built on the dotnet virtual machine, which I have never
> heard described as "elegant simplicity".

This is incorrect. While the Singularity compilers *do* compile to CIL,
they then do native code generation. To the best of my knowledge,
Singularity binaries are native-code binaries that have NO reliance
on .NET (well, the compilers run under .NET, but that isn't what you
meant here). The Singularity TCB is actually very small, and is almost
entirely written in Sing#.

>   And it is all built with Sing#, a more-bells-and-whistles version of
> Spec#, which is itself a more bells-and-whistles version of C#, all as
> if C# didn't already have enough enough bells and whistles for the
> Rose Parade. 

On this point, at least, I think you missed the boat rather completely.
My understanding is that there are a very small number of language
changes relative to C#, primarily to add support for a few low-level
representation issues. Most of the other things I know about at the
programming language level were *restrictions* on C# in order to improve
program analysis.

The interesting differences between C# and Spec#/Sing# all concern
property capture and verification, which is pushing hard in the
direction of formal verifiability. Think "eiffel
preconditions/postconditions on steroids." While those changes add to
the burden of the programmer, they do so in a way that consistently
yields *much* more reliable code. They do not add to the intrinsic
conceptual complexity of the underlying programming language. The net
effect is to enforce a moderately higher level of specification capture
in a way that the compiler can check (strictly speaking: in a way that a
property checker can check, and the compiler can then rely on).

> So from here it looks like Singularity suffers the traditional
> microsoft disease: pile features on a weak foundation, rather than
> build a powerful foundation.

Concerning ACLs, yes, I think they missed the boat, and I have said so
to Jim Larus. My understanding of Singularity may not be entirely right
either, but I did spend a fair bit of time talking with Tarditi and
Larus to try to understand what was novel there. It's not necessarily
the answer to the question you are trying to pose, but it's good work
nonetheless.

Of course, any fundamental architectural error that survives into the
product is now Ravi Pandya's responsibility. Since Ravi is one of your
(MarcS's) proteges, you share some of that responsibility. :-)


shap