discussion: LLL and Security
Thu, 17 Nov 94 20:01:07 MET
>> There is a big problem with a LLL: Security. [...]
>> be ok may be more difficult to prove as computing the argument; i.e.
>> requiring that the argument be a prime number or any such thing).
> Erm  I don't think its difficult, I think it's _impossible_ to be
> certain (Analogy, it's not always possible to determine whether a
> particular program will even _terminate_, let alone whether it will screw
> the system). You could also spice this with a bit of Godel, if you wish,
> and sorry about the neglected umlaut!
I don't agree that it be impossible. That's what program correction proofs
are all about, which is my field of study.
I do not mean that every program running on the system should have a full
proof of its correctness (though in the long run, I'm sure this will be the
case, if our system is to last).
I mean that arbitrary security is arbitrarily complex to express, and that
we should *allow* such complexity in the system.
But we should also *allow* simplicity, and when we can't prove the full
correctness of a program, prove that at least it won't crash the system
(i.e. won't forge object IDs, won't mess the garbage collector, etc).
>> * external object specifications in a high-level specification language are
>> given with the low-level equivalents
> Erm  If the hi-lang has corresponding lo-lang specs, for whom/what are
> we providing the hi-level specs ?
We admit axiomatically that we have such hardware behaviour, then we prove
that such low-level programs fullfill such hi-level specification. Then,
until we need performance problems that the available compiler can't solve,
we don't bother with low-level implementation an use only high-level
constructs. What's the problem ? Of course, before we have a proof, we can
still use hacked programs with a permission from root (that is ourselves).
> Or am I being a complete twit?
Your skepticism is welcome. Proofs are *hard* to make. But most of the time,
we need simple proofs. And they are the best security ever to be.
My paper (in design phase) about the goals and means of a New OS stress that
security *is* a *must* for computer users, and not what Bullshix call security
(i.e. stubborn permission rights), or not even ankward capabilities, but *any*
kind of security. The NASA should be more concerned about its multi-billion
dollar spaceships not exploding than about their multi-million dollar plans
being read by foreign countries (who do not even have money to build such
spacecrafts !). And this is precisely some kind of security that only a
full-powered proof system only may give.
Of course, you'll say, why not have a *separate* proof program, why integrate
it to the OS ?
Because *ANY USEFUL FEATURE MUST BE (POTENTIALLY) PART OF THE SYSTEM, OR ELSE
ONE WON'T USE THE SYSTEM, BUT USE ANOTHER SYSTEM, BUILT ON TOP OF IT*, and
this means, another system will have to be written, with much more difficulty
and much less security, as the underlying system will have to be trusted.
-- , , _ v ~ ^ --
-- Fare -- email@example.com -- Francois-Rene Rideau -- +)ang-Vu Ban --
-- ' / . --
MOOSE project member. OSL developper. | | /
Dreams about The Universal (Distributed) Database. --- --- //
Snail mail: 6, rue Augustin Thierry 75019 PARIS FRANCE /|\ /|\ //
Phone: 033 1 42026735 /|\ /|\ /