Bumping Up Against Space Quotas

While outlining a formal confinement proof for Keykos we came across a fairly serious covert channel. The channel was that of space allocation; a covert transmitter allocates space so that the covert receiver cannot, thus providing the covert signal. This was known and a variety of hand waving schemes seem plausible to plug this channel. This remains the only covert channel revealed by the formal analysis and perhaps it is time to propose a more detailed solution. This also convinced me and a few others that formal proofs are worth more than we had thought—even outlines of formal proofs.

We collect here notes on allocation patterns that we must avoid disrupting at least for unconfined applications. There may be compromises for confined programs but general programs designed for Keykos should be confinable when not contrary to the purpose of the program.

The design of non-prompt banks must also be completed, or the problem that they were to address must be addressed otherwise. I don’t know whether these problems are antagonistic or synergistic, but they are related! Here is the original general idea for non-prompt banks.

The fixes considered so far require new orders and modifications to less used orders on space banks. There are other features of space banks that may be provided via a new bank keeper mechanism by which the TCB can be shrunk at the same time that we provide for more general space allocation policies.

Signals by using caches that are not allocated by capabilities

Some real cache facilities are administered by hardware; others are managed by low level kernel logic. Cache performance may leak signals and serve as a covert channel which must be dealt with as well, but not here, except to remark that if those channels are broad enough for covert purposes, it may be important to manage those cache resources explicitly for better system performance.

Hand Waving Solutions

The first idea seems to be “Don’t impose shared quotas.”. It is necessary to view “total available real storage” as just another quota and we do this already. There are, however, hard and soft quotas. Exhausting a hard quota leaves the requestor the dilemma of dying or proceeding somehow without the storage. At least there is no suspense in this case. Exhausting a soft quota may be invisible to the requestor when some other space policy module, running perhaps with different authority, arranges for more space. The decision may be indefinitely delayed, however. There remains the question of whether a hard quota should be visible to the requestor. Reading the hard quota seems the natural tool for the covert receiver, but denying read access to the quota hardly denies him the information.

Nuts & Bolts

We must show that a nascent object from a factory holds no capabilities that may be used to send signals from the world that it will create. The factory specs enumerate the keys that the new domain holds as it begins to obey the untrusted .program from the factory builder. One of these keys is the space bank key as provided by the requestor via the factory requestor’s key. The factory code has determined that the bank is official, but the bank has mutable state nonetheless in the form of limits. Actions by confined code can change the limit and the limit can be sensed by unconfined code. As in meter logic, the limit bounds how much net space the bank and the inferior banks, will allocate. Orders for new nodes fail when the limit goes to 0. Orders on some facets of the bank read and change the limits.

This note describes general features of the bank that I think are not part of the problem and I think are necessary to preserve.

A Design Tree

Remove the ability to read limits
Reading the immediate limit in a bank is the tool that space administrators use to determine how much space their customers have used. The only banks whose limits would be affected by the covert transmitter would be the superior banks. Those are sufficiently closely held.
The readMinLim operation on any of many other banks might be affected by a covert transmitter. This feature was included, however, because the information was scarcely unavailable otherwise: “This was included for it was equivalent of buying space until there was no more and then selling it all back.”. While it is true that such a covert receiver is hardly low profile, as covert operators should be, it is nonetheless a non trivial exercise to catch him, convict him, and expel him. I don’t know how.
Don’t share the factory
For each requestor’s key in each factory yield, provide a front end to the factory that buys the space that the real factory will need. These front ends can be installed by the factory as factory components are installed. The factory would accept these as valid factories. It is OK for this front end to get stuck. The front end could perhaps execute all of the factory code to produce the yield. I don’t like this. I think I have found the end of the changes. I don’t like the extra space.
Reserves in banks
The rough idea is that a bank can hold reserve space to sell without going to superior banks and thus revealing purchase patterns. This reserved space is otherwise wasted while it is reserved. It is good for confining minnows. Here is a hand waving intro and here is a start at a design based on reserved but unallocated frames within a bank.
Ignore Factory’s Requirement for Prompt Bank
This won’t be a solution, but it might lead to a solution. Here are the details.
The Stonewall Stance
This introduces a new domain state that a shared factory can take that lets it pretend that it didn’t hear an order for a new widget. This lets it become available to other requestors while space is, or is not, being made available to the original requestor. This lets the factory solve the keeper problem just like the kernel does. See the details.