[coyotos-dev] Thoughts on (non)persistence
norm at cap-lore.com
Thu Jan 27 01:51:29 EST 2005
Excuse previous mis-fire!!! Cancel previous mail.
On Jan 26, 2005, at 6:12 PM, David Hopwood wrote:
> Eric Northup wrote:
>> On Mon, 2005-01-24 at 17:12, Norman Hardy wrote:
>> The main goal for removing persistence was to simplify the kernel.
>> additional line of code increases the burden of verification. Each
>> additional invariant that must be maintained significantly increases
>> difficulty. Persistence adds non-trivially to both code and
> Most security flaws in existing systems are in code that is outside
> the kernels of those systems, but that is nevertheless relied on by
> Removing orthogonal persistence does not reduce overall system
> on the contrary, the overall complexity is increased. It does not
> reduce the
> size of the TCB that users actually rely on. The goal should be to
> confidence in the security of a whole system, not the kernel in
I want to amplify David's points:
If persistence is done outside the kernel and is yet in the TCB then
is more complex because abstraction has been lost.
Abstraction divides up and simplifies proofs as well as code.
A program correctness proof must always start from program function
Kernel hooks to restore state will be an immense sore thumb in such
I grant that correctness proof of even a kernel without persistence and
without such hooks would be a tremendous achievement and milestone.
But is it indeed a step towards a "certified yet usable system"?
>> We may eventually be able to add persistence back to the kernel. If
>> succeed in verifying a non-persistent kernel, that would be a time to
>> consider adding persistence. We have been careful not to make any
>> changes to the design that would preclude persistence.
> If we intend to support orthogonal persistence, then the *easiest* way
> do that is to design it in from the beginning. Whether it is part of
> kernel or not is a secondary issue.
The Keykos kernel banished the migrator from the kernel as it sorted
and this could be done in user mode without a permanent kernel space
allocation for the sort.
(The kernel was too simple to admit malloc and stay correct.)
is where we made our best excuse for this part of the architecture.
If persistence were designed in but initially omitted, and eventually
included under compile-time switch, then you might have the
best compromise even if you never succeeded in a proof with persistence.
The folks from NCSC (about 1987) were very enthusiastic about a simple
restart theory for they had evidently struggled to understand how
certain previous systems managed secure restart.
Sometimes it is more important to be abstractly simple even if this
the implementation isn't.
At least with that sort of complexity it is possible to understand the
and possible to know what the code should do.
But I preach to the choir.
> David Hopwood <david.nospam.hopwood at blueyonder.co.uk>
> coyotos-dev mailing list
> coyotos-dev at coyotos.org
Norm Hardy: <http://cap-lore.com>
Nothing has an uglier look to us than reason, when it is not on our
More information about the coyotos-dev