discussion: LLL and Security

[Francois-Rene Rideau]

>>    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 [1] 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 [2] 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 -- rideau@clipper.ens.fr -- 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                                    /|\ /|\ /