[E-Lang] Reliance & Static Security Checking

Ben Laurie ben@algroup.co.uk
Tue, 02 Jan 2001 16:56:58 +0000


"Karp, Alan" wrote:
> 
> I know even less about this topic than does MarkM.  However, my limited
> experience with provable correctness leaves me pessimistic of the prospects
> of using it in operational systems in the near future.  MarkM's proposal
> would seem to rely on this goal being achievable.  Never one to let
> ignorance stand in my way, I'd like to make a half-baked suggestion.
> 
> There is one aspect that I think is immediately implementable, and he has
> given an example of it.
> 
> >
> >     def a : rely(Foo)
> >     def b : suspect(Foo)
> >
> > then
> >
> >     b := a
> >
> > looks ok, but
> >
> >     a := b
> >
> > is cause for alarm.
> 
> Just this amount of static checking would prevent errors involving reliance
> on data declared unreliable; things can only get less reliable, not more so,
> sort of like entropy.

I'm sure this is obvious to everyone, but this is rather like Perl's
"tainting" mechanism. Just thought I'd mention it.

> Here's an example from an early e-speak implementation in Java.  I wanted to
> have a homogeneous collection, but Java 1.1 collections only take Object.
> In my first implementation, I made every effort to put the same kind of
> thing into a particular instance of the collection, but then I had to check
> that I had the right type every time I pulled something.  I'd call this
> collection "suspect" with respect to result type.  I hated that approach and
> eventually found a way to guarantee that the collection could only hold the
> right type of object.  (Override the add() method so the compiler does the
> checking.)  I was able to eliminate all the checking.  I'd call this second
> version "reliable" with respect to return type.

A parallel idea, but not the same one, IMO. The idea behind "rely" was
that if A relies on B, then A's security is dependent on B's correct
functioning (and security). In your example A would simply throw a
run-time error which would not (normally) compromise security.

Cheers,

Ben.

--
http://www.apache-ssl.org/ben.html

"There is no limit to what a man can do or how far he can go if he
doesn't mind who gets the credit." - Robert Woodruff