[E-Lang] Reliance & Static Security Checking
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.
"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