HLL semantics -- introduction

[Francois-Rene Rideau]

[These messages answer both Mike's "Fare's meta-protocol" and
Chris' "HLL: Guiding Concept" messages]

About my meta-protocol ideas, Mike asks:
> What I'm really asking is what's the format?  And all I keep hearing is
> we'll specify it later.  I'd like to see some pseudo-format for how
> exactly you plan to do it.  Everything above is really gray.  It also
> looks like it would balloon the size of objects in transit.  It also
> looks complicated and would require more resources that other
> alternatives.  Please propose a format so we can evaluate it.

   The low-level format is *not* important because it should be optimized
in an implementation dependent way (i.e. compressed for static files,
transformed into fast processor-dependent in-memory objects for dynamic
objects in fast physical memory). To please you (Mike), I'll propose some
low-level formats for both in-file and in-memory objects for the i386 and
POSIX implementations; but remember that it is only a draft, and that what
imports is the semantics on one side, and the way it integrates to other
low-level objects on the other.
   What is important is the semantics, i.e. how the objects interact, up to
some isomorphism; not the exact name of such object, or its exact encoding.
And this *is* HLL semantics, even if the kind of syntax you want is
arbitrary binary rather than linear text.

   Firstly, there is always a meta-protocol, even if it's hardwired in a
kernel, completely powerless, and need unsecure "user-level" meta-protocols
implemented on top of it to do anything, like executable file loaders
from unix & co & derivatives. What I propose is a system in which objects
come with their full specs (at least the ones respective to system crash),
and won't be used unless the system checked the security, while conversely
will be sure that they won't be cheated with parameters that don't fulfill
their requirements; such system is the most secure and the freest ever
possible (we'll see why later in this message).

   Now, you talk about other alternatives. What are they ? What kind of
actual user security do they allow, if they allow some at all ? My system
allows just *any kind* of security through proof checking. What kind of
system do you propose ? A unix-like finite security system, that must be
unsecurely user-extended to do anything new ? A VSTa-like pro-finite
security system (which is isomorphic to order-zero propositional calculus) ?
A *decidable* strong typing system, that will disallow low-level crashes, but
will always allow some high-level crashes, as no decidable algorithm can
prove security in a powerful enough system ? Truely, these are no
alternative.
   You seem to admit that module-local security is needed, but seem to
want a check at invocation time. Such check is both unefficient (can't be
skipped even when useless) and unsecure (you have to trust the called module
anyway). There's a chicken-and-egg problem. We have to admit that we need
some security axioms to found the system. This does *not* mean that the axioms
will be an unreplaceable kernel; you may very well change/upgrade/downgrade
the axioms if you have enough rights; different modules could use different
axioms. But no module may run if it requires unverified axioms, theorems, or
parameters, in the context it is invoked.
   I propose a reflexive higher-order logic based security system; just *any*
security system that's programmable otherwise is specifiable inside this one
as first class object, while the converse is obviously completely false.
   What is such logic system like, and how to implement it ?
   That's what my next message is all about...