1. Start with a few simple but non-trivial terms and axioms

2. Define "universal constructions" as procedures for building uniquely identifiable structures on top of that substrate

3. Prove that various assemblages of these universal constructions satisfy the axioms of the substrate itself

4. "Lift" every theorem proven from the substrate alone into the more sophisticated construction

I'm not a mathematician (I just play one at my job) so the language I've used is probably imprecise but close enough.

It may be true that you can't prove the axioms of a system from within the system itself, but that just means that you need to make sure you start from a minimal set of axioms that, in some sense, simply says "this is what it means to exist and to interact with other things that exist". Axioms that merely give you enough to do any kind of mathematics in the first place, that is. If those axioms allow you to cleanly "bootstrap" your way to higher and higher levels up the tower of abstraction by mapping complex things back on to the simple axiomatic things, then you have an "open" or infinitely extensible system.

The original PSOS paper makes a few claims that are in tension with one another, and then buries the lede about how that tension can be addressed. Here's a few passages, directly quoted from the paper:

> [...] there are several important pragmatic reasons why PSOS capabilities are useful as a naming and protection mechanism for supporting abstract objects.

> 1. The capability mechanism has a very simple implementation. This allows capabilities to be built into the system at the lowest level of abstraction, thus making capabilities available for the most primitive objects.

> 2. Capabilities are uniform in size, making them easy to manage.

> 3. The inclusion of access rights in capabilities permits efficient fine-grained control of access to objects.

> 4. Capabilities can be written into storage (including secondary storage) and retrieved from storage in the same manner as other data, and therefore have many of the properties of other data.

Item 4 above is the one that should draw the most attention. I don't think anyone would contest the claim that PSOS has wonderful ergonomics for managing access to resources, but the moment you want to impose a system-wide access control policy then you must add another security mechanism, completely outside the capability abstraction, that adds some friction. This is fully acknowledged by the PSOS authors, although frankly they buried the lede since this is the only thing that the secure systems folks really cared about at the time. From the section on Store permissions:

> Because simplicity of the basic capability mechanism is extremely important to achieve the goals of PSOS, any means for restricting the propagation of capabilities should not add complexity to the capability mechanism. [...] A few access rights (only one is currently used by PSOS itself) are reserved as store permissions. This is the only burden placed on the capability mechanism.

> By properly choosing the segments that are capability store limited, some very useful restrictions on the propagation of capabilities can be achieved. The restriction used in PSOS is not allowing a process to pass certain capabilities to other processes or to place these capabilities in storage locations (e.g., a directory or interprocess communication channel) accessible to other processes. [...] The store permission mechanism has been selected as primitive in the system because it achieves the desired result with negligible additional complexity or cost.

This appears as claim 8 in the summary section of the paper near the end:

> Propagation of capabilities can be restricted by use of capability store permissions. The passage of a capability to other users can be prevented by not including process store permission in that capability's access rights.

Ok, so that's the PSOS paper and it's claims. Boebert's paper--really a note, since it is a mere 3 pages--states its argument in fairly direct terms:

> The attack is made possible by an inherent attribute of pure capability machines: the right to exercise access carries with it the right to propagate that access. Thus even if an omniscient oracle correctly creates capabilities, it cannot control their further propagation. If extra mechanisms are imposed to impose this control, the machine is no longer an unmodified capability machine.

The only issue here is, perhaps, semantic: Boebert (correctly) states that an unmodified capability machine cannot provide what is considered a very basic mandatory security policy, but the PSOS folks already acknowledged this by stating that the system needs a capability store permission manager for mandatory security policy enforcement. The phrasing that they used--"the store permission mechanism has been selected as primitive in the system"--is the bait-and-switch where they treat it like part of the capability model rather than making it clear that it is an entirely distinct mechanism that must be composed with pure capabilities to achieve the (genuinely difficult) security properties that systems designers were seeking.

I suspect the horse is already dead it's worth double-tapping to make sure, so let's continue. The Myths paper muddies the waters further by making this claim after supposedly debunking Boebert:

> Boebert’s result is valid in any capability system that cannot distinguish between data transfer and capability transfer. But partitioned and type-enforced capability systems do not have this problem, and password capability systems have been engineered to avoid this problem [1, 11].

> Moreover, it has been formally verified that any capability system enforcing independent controls on data transfer and capability transfer can enforce both confinement and the *-Property [22].

We'll focus on reference [22] since that is the stronger claim here. That paper is Shapiro & Weber (2000) "Verifying the EROS Confinement Mechanism": https://flint.cs.yale.edu/cs428/doc/eros-verify.pdf

This is the motivation for their paper, which is stated unambiguously:

> Boebert [1] and Karger [9] have argued that unmodified capability systems cannot enforce even basic mandatory access controls such as the *-property. Both have proposed solutions in the form of hybrid protection architectures. Karger has also argued that unmodified capability systems cannot enforce confinement [8]. Given that EROS is a pure capability system, and that its security design rests on its ability to enforce confinement, a rigorous verification of the EROS confinement mechanism is necessary.

For some reason, they decide to respond to these claims in the Related work section, just before their conclusion, although they do address them head-on:

> Boebert [1] and Karger [9] show that pure capability systems cannot enforce the *-property. While their conclusion is correct, capability systems do provide sufficient strength to construct mandatory policies at a higher level of abstraction with reasonable performance, as has been done in KeySafe [14].

> Karger has also shown that unmodified capability systems cannot enforce the confinement policy [8]. The apparent discrepancy results from differences in term definition. Karger’s confinement policy is a mandatory access control policy: "this piece of information must not be disclosed to that set of unauthorized parties." That is, it is a policy concerning the flow of information to subjects. Lampson’s confinement problem [10] imposes a weaker constraint: information can flow out of the subsystem only through authorized channels. That is, in the Lampson definition the channels define an encapsulation boundary to be enforced.

> We believe that the KeySafe architecture can enforce both the *-property and Karger’s confinement policy, but this does not directly contradict their claims. KeySafe is a reference monitor built on top of a more primitive capability mechanism; such a reference monitor constitutes a modified capability system in the sense of Karger’s discussion.

It's worth questioning whether the Myths authors were justified in citing this paper the way they did. But either way, I think it's pretty clear that once you pin down a precise definition of the terms used in the discussion, there is little disagreement among any of these authors. However, in casual arguments this precision is lost and you end up with a situation where two things are true at the same time but people choose to talk about only one at a time and think they're winning arguments:

1. An unmodified capability machine cannot enforce the *-property or mandatory access control confinement policies.

2. Modifying a capability machine to enforce such policies (and provide proof of enforcement) is straightforward because there is a single clearly-defined interface through which the systems may be composed.

My stance is that the PSOS folks screwed up their marketing. They really do have a superior product, so to speak, but they tried to downplay the fact that it did not provide a solution to the genuinely difficult problem of enforcing MAC policies (which was really about reference monitor discipline, not capabilities or ACLs). The right pitch for ocap design is "we offer a cleaner, more compositional, more auditable substrate for authority management--which is itself a substantial contribution and worth caring about--and on top of that substrate you can build the same MAC policies you'd build on any other substrate, but with better starting axioms and clearer proof structures." That's a contribution that doesn't need to be defended against Boebert because it doesn't claim (or appear to claim) what Boebert showed couldn't be claimed.

So yeah, the next stage is models that basically do what humans do: encode causal models of the world in a composable, symbolic form that can be falsified and refined through interventional experiments.

Boebert’s objection is about whether Alice can transmit unauthorized authority to Bob across a security boundary that’s supposed to prevent that flow. Your SCM_RIGHTS example is a case where the kernel is deliberately providing a sanctioned channel for authority transfer, with the kernel’s blessing, between two processes that the kernel does not consider to be on opposite sides of a mandatory access control boundary. Unix has no (*)-property. There is no “high” and “low” in the Bell-LaPadula sense on a standard Unix system. So of course the kernel mediates the transfer cleanly; it’s not enforcing any policy that would be violated by the transfer.

The moment you try to extend this to the actual case under dispute—Alice is “high,” Bob is “low,” and the security policy says high-to-low information flow is forbidden—then if the kernel refuses to deliver the fd across the boundary, the security property was enforced by the separate MAC layer, not the capability mechanism.

The conflation which is endemic in this whole debate is between “capabilities as a kernel-mediated authority mechanism” and “capabilities as a property that holds across all observable behavior of the system.” Unix file descriptors are the former. Boebert’s objection is about the latter.

Declarative state and reactivity, lexical lifetimes and ownership, etc. Really curious how you set it all up and what prior art was your primary inspiration.

If this is the right framing, then the two systems aren't really competitors despite solving the same problem--they're going to appeal to fundamentally different developer sensibilities. Rama is for people who want to think like Jay Kreps or Martin Kleppmann: the event log is sacred, physical data layout is a first-class design decision, and the programmer earns the performance benefits by understanding the system deeply. Cambra (if these assumptions hold) will be for people who want to think like database users: describe what you want, let the optimizer figure out how, intervene only when necessary. These are both defensible positions and both have historical track records of working. SQL's history shows the declarative camp has ecosystem advantages once the optimizer is good enough; Kafka/Rama's history shows the log-centric camp has correctness and observability advantages for event-heavy domains.

Comments URL: https://news.ycombinator.com/item?id=47342817

Points: 2

# Comments: 0

- Through the last two decades of the 20th century, Moore’s Law held and ensured that more transistors could be packed into next year’s chips that could run at faster and faster clock speeds. Software floated on a rising tide of hardware performance so writing fast code wasn’t always worth the effort.

- Power consumption doesn’t vary with transistor density but varies with the cube of clock frequency, so by the early 2000s Intel hit a wall and couldn’t push the clock above ~4GHz with normal heat dissipation methods. Multi-core processors were the only way to keep the performance increasing year after year.

- Up to this point the CPU could squeeze out performance increases by parallelizing sequential code through clever scheduling tricks (and compilers could provide an assist by unrolling loops) but with multiple cores software developers could no longer pretend that concurrent programming was only something that academics and HPC clusters cared about.

CS curricula are mostly still stuck in the early 2000s, or at least it feels that way. We teach big-O and use it to show that mergesort or quicksort will beat the pants off of bubble sort, but topics like Amdahl’s Law are buried in an upper-level elective when in fact it is much more directly relevant to the performance of real code, on real present-day workloads, than a typical big-O analysis.

In any case, I used all this as justification for teaching bitonic sort to 2nd and 3rd year undergrads.

My point here is that Simon’s assertion that “code is cheap” feels a lot like the kind of paradigm shift that comes from realizing that in a world with easily accessible massively parallel compute hardware, the things that matter for writing performant software have completely shifted: minimizing branching and data dependencies produces code that looks profoundly different than what most developers are used to. e.g. running 5 linear passes over a column might actually be faster than a single merged pass if those 5 passes touch different memory and the merged pass has to wait to shuffle all that data in and out of the cache because it doesn’t fit.

What all this means for the software development process I can’t say, but the payoff will be tremendous (10-100x, just like with properly parallelized code) for those who can see the new paradigm first and exploit it.

Could I speak Japanese at that point? No not really… I even had a Japanese spouse! But we spoke mostly English at home. I could read quite well, but conversation was very challenging.

Then we moved to Japan. Despite not having a job that requires me to speak Japanese, I got enough live exposure just from chatting with people at the gym or in social activities that now, a few years later, I’ve backfilled all that conversational fluency that was missing. No special extra effort required, just living in an environment where I used the language reasonably often.

Anyways, the point is that all the time spent in Anki laid a rock-solid foundation that merely needed activation in the right environment for active fluency to emerge. Of course I no longer do my daily flashcard drills (and I’ve forgotten how to write quite a few kanji as a result) but the work paid off.

From my own personal experience, this realization came after finally learning a difficult foreign language after years and years of “wanting” to learn it but making little progress. The shift came when I approached it like learning martial arts rather than mathematics. Nobody would be foolish enough to suggest that you could “think” your way to a black belt, but we mistakenly assume that skills which involve only the organs in our head (eyes, ears, mouth) can be reduced to a thought process.

Early resistance to high-level (i.e. compiled) languages came from assembly programmers who couldn’t imagine that the compiler could generate code that was just as performant as their hand-crafted product. For a while they were right, but improved compiler design and the relentless performance increases in hardware made it so that even an extra 10-20% boost you might get from perfectly hand-crafted assembly was almost never worth the developer time.

There is an obvious parallel here, but it’s not quite the same. The high-level language is effectively a formal spec for the abstract machine which is faithfully translated by the (hopefully bug-free) compiler. Natural language is not a formal spec for anything, and LLM-based agents are not formally verifiable software. So the tradeoffs involved are not only about developer time vs. performance, but also correctness.

It is the miracle of modern capital markets that enables almost anyone to quickly and easily invest their savings in productive assets, but of course capital markets aren’t perfect. The availability of “none of the above” options (like gold) that remove savings from the pool of active investment capital is the essential feedback loop that balances risk and return.