Lambda the Ultimate

Most OSes run processes in user mode, in their own address space, and let them affect the world outside themselves only by making system calls. Any such OS "works because code running in a process basically has no ability to do anything at all". By making system calls, a process asks "the kernel to do the task on its behalf." All interesting questions of OS design start after this much is established.

SELinux adds to Linux so-called "Posix Capabilities". As explained by Capability Myths Demolished, these aren't capabilities at all, and the protections they provide are terribly coarse grain.

In both AppArmor and SELinux, privileges are granted by static configuration. The principle of least privilege demands that a program be given only those privileges needed to carry out its duties. As explained throughout my dissertation and demonstrated by many of the examples, a program's duties change dynamically as requests are made. Until these requests are made, it is not possible to determine the least privileges that would be adequate to carry out these requests. When privileges can only be granted ahead of time by static configuration, you end up granting excess privilege just in case, rather than least privilege just in time.

Terminology note: The term "privilege" has no clear definition, and prior usage is ambiguous. We distinguishe "permission" and "authority". Some prior efforts to provide "least privilege" clearly sought (in our terms) "least permission". Others clearly sought "least authority". We argue that "least authority" is the sensible goal for improving safety and robustness.

All interesting questions of OS design start after this much is established.

This is, of course, correct. This raises another issue, which isn't directly language related as far as I can tell, but might be of interest.

On MVS (but the story is applicable elsewhere), when we wrote APF authorized programs, which are the ones that are authorized to change memory protection keys, and use privileged instructions, it was well known that you want to run in this higher state for as short a time as possible, to reduce security risks. But that wasn't enough. A key idea is that when you run on behalf of a user, you want to use the premissions that specific user has, not the secuirty setting of the program. A "trick" that ensures that this is what really happened, was to spawn a task, which had the security settings of the specific user, and run the code under that task, and not under the system task that had more permissions. Thus, if you wrotea TP monitor, for example, it might need many system level permissions, but when it needed to execute a transaction on behalf of users, you just created a task with that represented that user (you do that by setting the ACEE to be that of the user). Note that when you do this, the OS will ensure that this taks will not be able to bypass the permissions the specific user have, as was described in the previous comments.

That's not the whole story, and there's nothing new here to those in the security and system programming world, but I think it is important to keep in mind some of these details.

Is there any good reference comparing/contrasting actors vs. pi calculus vs. join calculus from the viewpoint of someone implementing systems?

...but after just finishing reading the thesis, I have an urge to try and create a toy implementation of E-like system... Given my interest towards learning Haskell and STM I have a clear idea of what the target platform will be :-)

Hopefully, if I have enough time, I will share my findings on whether intuitions from join, pi, and actors helped me or not.

By "STM", are you referring to the paper on monad-based transactional memory in Haskell? I found this paper interesting but difficult. Perhaps again out of ignorance, it's not clear to me what the relationship is with E. What connection do you see?

Please do try your experiment. I'd be happy to help and give advice.

Hi Mark!

The comments so far seem to be concentrating on E's approach to concurrency vs. the foundational calculi for concurrency such as the Join Calculus, ignoring the relationship you explicate in your thesis between support for concurrency and support for security. Given that the process calculi I'm familiar with say nothing about security, and that security appears to be a principal concern of the E project, it seems quite reasonable not to see the connection between E and the Join Calculus.

The project that seems to me to target much the same space as E, except in a typed setting, is Acute. The missing piece is, of course, the object-capability security model. My outstanding question/open research project is determining whether Flow Caml represents an effective launching-off point for exploring object-capability security in a typed setting. If you read the Flow Caml materials, you'll note, quite rightly, that it misses the major point of your work: that least authority can only be determined dynamically, so a purely-static lattice such as that introduced by Flow Caml might be a necessary, but not sufficient, basis for a typed object-capability system. I would agree with that argument, and ask whether An extension of HM(X) with bounded existential and universal data-types (entry 5 on the page) provides sufficient dynamic support to close the gap. In particular, I'd love to open a discussion as to how (if possible!) to map the Auditors taxonomy onto a modern type system, perhaps HMG(X) (entry 1 on the above page), or System F with Type Equality Coercions.

...the process calculi I'm familiar with say nothing about security...

Although I'm not all that familiar with it myself, I believe that the ambient calculus is a process calculus that does address security. In particular, the ambient calculus deals in dynamic capabilities and boundaries.

For that matter, even process calculi with static process topologies may have something to offer on the security front. For example, there's been a large amount of work on using CSP for modelling and analysing security protocols (resulting in a new break in the Needham-Schroeder public-key protocol). Granted, that's not quite the same as looking at capabilities. But it may be possible to adopt a similar approach to modelling dynamically-determined capabilities as the protocol work takes to the passing of "secrets" between agents (I really haven't thought about it in depth though).

By STM I meant both the Composable memory transactions paper, and the specific implementation available in GHC version of Haskell.

I do not see STM as overlapping E, on the contrary, it seems complementary to it. While transactions might be encoded in the kernel language without them, the encoding would be cumbersome (in the way encoding of asynchronous pi calculus in core join calculus is cumbersome). That's why I suspect I would use STM for implementation of any "process-calculus" language - though not sure yet how transactions will get exposed to the object language.

You should look at the HAppS framework. It is intended for writing web apps in Haskell. As part of the framework, there is a transaction monad.

I'm at significant risk of being flat wrong here. Hopefully Mark Miller will set things straight.

I've been following the E work for several years now, as well as exploring the various new (and old, for that matter) results in type theory, and I can't help but observe that E is dynamically typed, and its principals—Mark and others—come from the Smalltalk tradition, even though the primary implementation is in Java, a statically-typed language. So I suspect that one reason the Join Calculus doesn't show up is that apart from the untyped lambda calculus, most computational calculi come from (subsets of) the type theory community. Mark and friends don't live there, and I seem to recall Mark expressing the usual sort of skepticism that the dynamic typing community generally does about static typing being effective towards solving the problems they wish to solve.

To me, the greatest concentrated contribution of the E project—and there are very many—is the Auditors concept and its taxonomy of object properties that can be expressed and checked. This, along with the Ode to the Granovetter Diagram, is the culmination of many decades of the best thinking in digital security that's been done. I first raised the question of how we might apply the lessons of auditors to a statically-typed language—UnrealScript—here. Tim Sweeney's reply was extremely educational for me, engendering my own self-education into modern type theory (ongoing), a wonderful Socratic dialogue with Tim via e-mail (thanks, Tim!), and further questions with a bit (but only a bit!) more focus, the best starting point probably being my "Wayback Machine" comment here.

You correctly characterize my history and my skepticism about static types. However, this of course does not excuse my leaving out the Join Calculus if it is indeed relevant.

On static types, section 5.7 of my dissertation states the forms of robustness E is and is not built to achieve. The relevant issue here is "fail safe" vs. guaranteed progress. Compared with dynamically type safe systems, static type checking only prevents the dynamic occurence of message-not-understood errors, which would still fail safe. For systems unable to support guaranteed progress, which include all implicitly allocating languages, what problem does static type checking solve? OTOH, excess authority errors, if not caught statically, cannot be caught dynamically, and would fail unsafe. I revisit this theme briefly in sections 6.3, 26.6, and especially 26.4.

Thanks for singling out the work on auditors and smart contracts. I do indeed think that both are important. Unfortunately, even though the dissertation may be the only paper document I'll ever write that has no page limit, I didn't feel I could do justice to either topic within the space I was willing to take.

Mark, thanks for this. I will go over your thesis with a fine-toothed comb and reply at greater length when my sense of understanding and available time converge. :-) For now, suffice it to say that I'm inclined to believe that object-capability security in a typed setting will indeed require something like an Ontic or dependent types behind it.

Hi Paul!

I'm especially curious how one would statically type the membrane of my Figure 9.3 (p. 71).

I remember being fascinated by Ontic once upon a time. Now that I know more, I would like to take another look at it. Unfortunately the link on the page you link to is broken. Do you have a current link? Thanks.

Never mind. I found one here.

The Join Calculus didn't appear on my radar mostly out of ignorance. Thanks for the pointer to the "reflexive CHAM" paper. I'm printing it now. I've also found one of the multi-function papers you mention here.

I had heard of the Join Calculus, and had wondered whether it was relevant. Since I learn programming language concepts best by learning languages which embody these concepts, I had read one of the papers on C-omega (or perhaps polyphonic C#). From this paper, I didn't see anything I thought was related. I also had a brief look at JoCaml, and also didn't see much relevance. In both cases, I may have been premature. I'll look at the papers you mention and post my reactions. Thanks again for the pointers!

The Wikipedia entry, which I admit I authored, has some pointers to join-calculus relevant material:

• I believe you already have this one.
• Here's a more recent one (2000).
• The Join-calculus programming language, since you mentioned that you learn better by examining a language.
• Join-calculus home page.

I also found Functional nets papers by Martin Odersky improving my understanding of inner power of join calculus.

The implementation of Funnel is pretty stale, though, that being one of the reasons I look forward to write some myself.

I suspect that join calculus is not absolutely better than E-Kernel.
My suggestion would be to compare whether their expressive power is comparable for the purposes of E, and if not, then what lessons do we learn.

By the way, I agree with Paul on importance of auditors. However, I think the main contribution of the thesis (to me, at least) is the analysis of the higher-level interaction patterns (caretaker, promise, stub) and distinction between permission and authority. On the other hand, I feel that the presentation would benefit from a separation into a theoretical (robustness?) framework and semantics of specific E-like languages. This would enable comparison between different PL design ideas in light of robustness.
Another idea would be presenting these languages in layers (in the manner popularized by CTM). Thus, the language could start from single-vat, closed creation subset; then acquire more features, possibly built as syntactic extensions on top of the simpler subsets. I realize this is broader in scope than a single thesis can cover - but why not write a book? ;-)

I am starting to sound like I didn't like the thesis, which is far from the truth. It is a great exposition to the ideas of E community! Thanks for writing that!