Lambda the Ultimate

But seriously, both erights.org and cypherpunks.to are valuable resources of capability-related information.

If I were to construct a more or less serious language (or even a toy), I would make sure it's capability-tight.

Andrew, a challenge for you - prove formally whether your language enables capability security :-)

So which languages do?

1. Makes it impossible to forge references to entities.
2. Disallows mutable global variables.
3. Follows object-oriented principles of encapsulation and polymorphism.
4. Has either structural equality or rights amplification (e.g. Sealer/Unsealer pairs) as a primitive.

This means that a good many languages are almost capability-secure: Java, upon which E is based; Scheme; Smalltalk; Oz... It turns out that an abstract store and lexical scoping get you something like 80% of the way there.

As of this writing, the only languages I know that are consciously, deliberately aiming for capability security are E and Oz.

ok, i looked at this anyway. kragen's intro is nice - http://www.canonical.org/%7Ekragen/3-sec-arch.html - and the emphasis on namespaces, rather than objects, is useful. i think it might be possible. now i must work...

From the documentation:

"Flow Caml is an extension of the Objective Caml language with a type system tracing information flow. Its purpose is basically to allow to write real programs and to automatically check that they obey some security policy. In Flow Caml, usual ML types are annotated with security levels chosen in a suitable lattice. Each annotation gives an approximation of the information which the expression that it describes may convey. Because it has full type inference, the system verifies, without requiring source code annotations, that every information flow performed by the analyzed program is legal w.r.t. the security policy specified by the programmer."

Ehud, the site search is broken.

hmm, yeah it seems that eros-os.org hosts the e-lang list http://www.eros-os.org/pipermail/e-lang/ which just makes me wonder, what is the connection. is eros written in E as would seem to be the most logical assumption? On Edit: answer would seem to be no, although there is a historical relationship not described yet: http://www.erights.org/history/eros.html http://www.erights.org/related.html

Lately, Shap has mothballed EROS for a variety of reasons, some technical, some not. He's currently engaged in discussions with developers of the L4 microkernel who are interested in crafting a secure system also. I think Shap and the L4 community see a great deal of value in starting with L4's extremely well-designed basis and leveraging Shap's experience in developing EROS (hmm, I don't mean to imply that EROS isn't extrenely well-designed too; it is, just along different dimensions than L4). It will be exciting to see what the future holds for capability-secure L4.

In the meantime, E is very nice. Play with CapDesk and the DARPA Browser and Den to see what I mean.

is the following a reasonable set of features to support capabilities?

• some way of expressing capabilities in the languages (object, name, token, whatever) that cannot be faked
• support for trees of capabilities (when you give a capability to someone else you generally give them a child of your capability)
• revoking nodes in the tree that you have capabilities for (which revokes all the child copies too)
• a way of composing capabilities (combining them into a new capability, which must therefore be opaque, revokable, etc)
• suitable library design (parameterise interfaces with capabilities, not strings, for example).
• suitable support for saving capabilities (difficult).
• suitable separation of "systems" - different threads (for example) should not be able to observe each other and so "see" capabilities unless explicitly allowed (this has nasty consequences for some meta-programming).

anything else? is there a reference list somewhere?

[edited to simplify a bit, and refutable -> revokable(!)]

One thing that always bugged me about the ending of that movie. OK, so where was skynet? Distributed across the dorms and office buildings, infecting the computers therein. So it started a nuclear war, which promptly destroyed all the dorms and office buildings, and the computeres therein. Um. All I could think was, given the usual (oxymoronic) state of Military Intelligence, I shouldn't be surprised Military Artificial Intelligence is not that much better off.

Seriously, the number one problem with increasing security is that there is absolutely *no* incentive on the parts of commercial software vendors to do so. Consider the story of two software products- product A is more secure (and robust), and product B ships sooner and has more features. Which product wins in the market place? Hint: how many people here are still running Microsoft? Make all the excuses you want, Microsoft is learning that being an object lesson in bad computer security doesn't hurt them (financially) in the least, and as such there is no reason for them to improve.

Until some form of product liability is instituted, and some software makers are sued out of existance for selling bad software, there will be no improvement in software security or reliability. In fact, I predict there will be ongoing degredation in both.

Such an opinion is generally greeted by shocked and dismayed exclamations of "are your INSANE?" I am resoundly assured that if software companies were held as liable for their products as automakers (which, I comment, doesn't mean you can't make mistakes, just that if you do, you have to fix them for free, and you have to make good faith efforts to make a good product in the first place), no one would be willing to write software. Why the same logic doesn't apply to cars (and every other consumer good imaginable) is never expounded on.

Of course, the computer industry isn't going to be who decides wether software makers are responsible for their products or not- society as a whole (or at least the legal system) is going to be making that call. The only question is when such legal liability will be enforced. Hopefully, the info-diaster that gives rise to that decision will be somewhat less catastrophic than accidentally kicking off global nuclear war.

Brian

It's precisely this calculus that efforts like EROS and E are attempting to address. Everyone understands that right now, as things stand, developing anything remotely like robust, high-security software is too time-consuming, and therefore too costly. But what if your OS and programming languages made developing robust, secure software tantamount to just using lexical scoping well, or "objects" well? That is, what if the most obvious design of your software was also the most secure? That's the capability security perspective: it addresses the economic question head-on.

Mark Evans: Trusted Computing Group

Run, don't walk, in the opposite direction! "Trusted Computing," as Microsoft and the other members of the "Trusted Computing Group" define the term, has nothing to do with protecting the user of the device in question and everything to do with propping up content industries faced with the challenge of evolving their business models in the digital age and, in the limit, moving to a software-and-content-rental vs. ownership model. This snake oil has nothing whatsoever to do with capability security, as becomes immediately apparent when you read their literature and find all the references to the already-known-useless security infrastructure: VPNs, PKI, "trusted third parties," ad nauseam.

To a first approximation, anyone who talks about "trusted third parties" isn't talking about capability security. The whole point of capability security is to enable what Mark Miller evocatively describes as "patterns of cooperation without vulnerability." If I have to trust a third party to a transaction, by definition I'm more vulnerable than if I don't have to, so a great deal of work has been done to remove such a necessity. The ERights.org site has many excellent documents and references to learn more from.

Jonathan Rees' A Security Kernel Based on the Lambda Calculus

Wow, thanks, the text is great!

Besides many other useful things it answers the question we discussed with Andrew recently about what is capability-unsafe in Scheme. It shows how to deal with define's and set!'s... One wonders, how did we miss the memo.

Paul Snively: It's precisely this calculus that efforts like EROS and E are attempting to address. Everyone understands that right now, as things stand, developing anything remotely like robust, high-security software is too time-consuming, and therefore too costly. But what if your OS and programming languages made developing robust, secure software tantamount to just using lexical scoping well, or "objects" well? That is, what if the most obvious design of your software was also the most secure? That's the capability security perspective: it addresses the economic question head-on.

My response:

Personally, I think the situation is worse than you can possibly imagine. I think if the IDE came with a check box button labeled "make this program secure", at least half the programs out there wouldn't click on it. Why should they? What do they get out of it? Nothing- currently, security has no commercial value. You don't lose any sales if you don't have it, you don't gain any sales if you do have it. Therefor, it's not worth the effor to click on a checkbox. Any major changes- like requiring programmers to think differently, change their habits, or even just learn a new programming language- are right out.

What needs to happen is for there to be a commercial value to security. There needs to be some upside, or at least the lack of some downside, to writting secure software. Some reason to not only click the checkbox, but learn the new language and the new way of thinking about software. Of course, we programmers are opposed to this. And especially the businesses and managers that employee us are opposed to this. It's much easier to beat our chests and screech than it is to think.