[E-Lang] Reliance & Static Security Checking

Tyler Close tclose@oilspace.com
Sat, 6 Jan 2001 19:49:18 -0000


Markm wrote:
> This means that the correctness of orderedTable depends on the
correctness
> of the provided keys are being correct Orders, ie, at correctly
implementing
> the order contract.  If a key is provided that isn't a correct
Order, for
> example, its compare() isn't transitive, then orderedTable may
deviate from
> its contract without being considered incorrect.  This is like a
> precondition, except we are not presuming to be able to formalize
the Order
> contract.

com.waterken.canal.Order is actually the interface to the comparison
predicate that the ordered table (or sorted map) is born with. The
sorted map "relies" on its creator providing it with a valid Order
implementation.

> Since orderedTable relies on at least one of its arguments, it
therefore
> relies on its clients, ie, it's vulnerable to its client's
misbehavior.
> Earlier, we defined such objects as "delicate", as opposed to being
a
> "server".  E's Maps are servers, as will be Hydro's hashtables as
presented
> to the E programmer, once Hydro is properly integrated into E.  E's
> ordered tables (which will also appear with the Hydro integration)
are
> delicate because we know of no affordable way to make ordered tables
be
> servers.

Whether or not a sorted map is "delicate", or a "server", depends on
the ability of the contained Order predicate to validate the input
arguments. If the Order implementation can verify that the arguments
are members of the expected irreflexive partial order, then the sorted
map is a "server". If the Order implementation cannot provide this
verification, then the sorted map is "delicate".

The only case that I can think of where the Order predicate would not
provide the needed verification is when the Order implementation
delegates the comparison to one of the argument objects via the
object's "compareTo" method, without knowing the concrete type of the
object. I suspect that most Order implementations need to know the
concrete type of the argument objects in order to calculate the
comparison, thus implicitly providing the needed verification of the
"suspect" arguments.

So, how do we propagate this information into the sorted map's method
declaration?

> humans.  Here's Bill's transformed hashtable:
>
>     def orderedTable {
>         to put (key :rely(Order), value :suspect) :void { ... }
>         to get(key :rely(Order)) :suspect { ... }
>         to delete(key :rely(Order)) :suspect { ... }
>     }

The general case is that the "put" operation "relies" on the key
(since the Order might "rely" on the key), but the common case is that
the key is merely "suspect". To support static reliance checks, the
"key" argument would have to be declared "rely", although it's
probably only "suspect". If you declare it as "suspect", then valid
programs might set off a static reliance checker.

Tyler