[E-Lang] Reliance & Static Security Checking

Karp, Alan alan_karp@hp.com
Tue, 2 Jan 2001 08:04:14 -0800


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.

What, then, could "rely" mean?  Well, where can I put my checks?  I see only
two places, inside the object or where its result is used.  Let's say that
"rely" means that I'm depending on the object to do all checking (type,
error, security, whatever); "suspect" means that I'll take care of verifying
the part of the result that I need for this use of the function.  Thus,
"rely" means that the object has been debugged, or maybe even proven
correct; suspect means I'll check myself.

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.

_________________________
Alan Karp
Principal Scientist
Decision Technology Department
Hewlett-Packard Laboratories MS 1U-2
1501 Page Mill Road
Palo Alto, CA 94304
(650) 857-3967, fax (650) 857-6278
 

> -----Original Message-----
> From: Mark S. Miller [mailto:markm@caplet.com]
> Sent: Friday, December 22, 2000 1:22 PM
> To: E Language Discussions
> Subject: [E-Lang] Reliance & Static Security Checking
> 
> 
> The coincidence at the EROS workshop of the discussion of 
> "rely" as a useful 
> abstraction for reasoning about security, and meeting Scott 
> Smith and Chris 
> Skalka, who are interested in using static checking machinery 
> (as in type 
> checking, but not necessarily types) to statically verify security 
> properties, as well as some old intriguing static security 
> checking ideas 
> from an unpublished paper by Marc Stiegler ("Trust and the Rules of 
> Engagement"), lead me to the following partially baked idea.  
> Don't worry, 
> I'm not planning to put the following into E in the 
> foreseeable future.
> 
> Let's say that every time we would have declared a variable, 
> for example, 
> "s : Stack", we instead had to say either "s : rely(Stack)" or 
> "s : suspect(Stack)".  Similarly, where we would have 
> declared a return type 
> "def foo(...) : Stack" we instead had to say either 
> "def foo(...) : rely(Stack)" or "def foo(...) : suspect(Stack)".
> 
> (Ignore for a moment that this would be a miserable piece of 
> notational 
> engineering -- an actual system would need some defaulting 
> rules.  However, 
> the design of safe defaulting rules carries their own issues, 
> which I would 
> like to postpone.  Depending on our defaulting rules, we may 
> find we only 
> need one of these keywords.)
> 
> 
>                            Checkable vs Informal Type-based 
> Correctness
> 
> 
> We start with the notion of "rely" explained in previous 
> messages: "A relies 
> on B" means "A's correctness depends on B's correctness."  
> However, what 
> does it mean for B to be correct or not correct?  In OO 
> programming, we 
> conventionally use types as contracts (not in the "smart 
> contracts" sense, 
> but in the program precondition-postcondition, etc, sense).  
> A static type 
> system can ensure conformance with the signature of a type -- 
> that something 
> claiming to implement a Stack in fact has push() and pop() 
> methods -- but 
> usually nothing more.  In the case of "Stack", the contract 
> itself can be 
> formalized, and often is as an undergraduate exercise.  
> Likewise, one often 
> statically proves simple implementations to be correct by 
> this contract.  
> 
> However, this is the exception rather than the rule.  For 
> most types in an 
> OO program, for example "Window", beyond signature checking, 
> the contract 
> exists in no machine understandable form, and is usually only 
> partially 
> captured in the type's documentation.  Rather, the type 
> itself serves as the 
> hook on which a community of interest hangs a partially 
> articulate shared 
> understanding of what that type is supposed to mean.  This 
> understanding is 
> nevertheless often adequate to meaningfully judge code to be 
> correct or not 
> at implementing that type.  Since "rely" and "suspect" are 
> only about the 
> propagation of correctness, they can successfully leverage 
> this informal 
> real-world notion of type-based correctness.
> 
> 
>                                  Taxonomy of Reliance Declarations
> 
> Instance Variables
> 
> As an instance variable, "s : rely(Stack)" means that the 
> containing object 
> relies on the object designated by "s" to be a correct Stack 
> -- to correctly 
> implement the Stack contract.  This does not imply any static 
> checking that 
> "s" actually does so.  OTOH, an object with instance variable "s : 
> suspect(Stack)" can assume "s" designates an object 
> satisfying the checkable 
> conformance to "Stack", but nothing further.  We say that "s" 
> is suspected 
> of not really being a Stack.  (Conventionally "checkable 
> conformance" means 
> static signature checking.  In E, it would be whatever 
> property the guard 
> "Stack" checks for.  This may be a dynamic or an audited 
> property, but it 
> can still only be a property we can formalize, and will 
> therefore fall far 
> short of informal correctness.)  
> 
> A "rely" instance variable corresponds to an unchecked 
> invariant, while 
> further allowing us to capture the notion of invariants that 
> are uncheckable 
> because they are unformalizable, or at least that no one has 
> bothered to 
> formalize them yet.  A "suspect" instance variable 
> corresponds to a checked 
> invariant -- an attempt to cause "s" to designate an object 
> that doesn't 
> satisfy checkable conformance to Stack must blow up -- either 
> statically or 
> dynamically.  Unlike a "rely" declaration, a "suspect" 
> declaration enforces 
> the constraints it expresses.
> 
> It's plausible that an object will typically rely on its 
> instance variables. 
> To rely on an object is to rely on the source of the object.  
> An object 
> necessarily relies on its immediate creator, so there will be 
> no cause for 
> alarm if an object relies on an instance variable in its 
> initial endowment 
> that its creator also relied on.  OTOH, if the creator 
> creates an object to 
> rely on an instance variable the creator suspects, then the 
> creator should 
> (must?) suspect the created object as well.
> 
> 
> Parameter Variables
> 
> As a parameter variable, "s : rely(Stack)" means that the 
> receiving object 
> is relying on its caller to provide an argument that behaves 
> as a correct 
> stack.  OTOH, given parameter variable "s : suspect(Stack)" 
> the receiving 
> object can assume that "s" satisfies the checkable 
> conformance to Stack, but 
> not that it is a correct Stack.  A "rely" parameter corresponds to an 
> unchecked precondition.  A "suspect" parameter is a checked 
> precondition.
> 
> To rely on an object is to rely on the source of the object.  
> Normal objects 
> in a capability system are engineered to be suspect of their 
> clients.  
> Following "Logical Secrets" (by Ken Kahn & myself, in The Ecology of 
> Computation, 1988), we refer to such objects as "servers".  
> For a server to 
> be correct, it must continue to provide correct service to 
> well behaved 
> clients despite arbitrary behavior from other clients.  A server must 
> therefore suspect all parameter variables, and rely on none.  
> Let's call a 
> non-server a "delicate" object.  Someone who relies on a 
> delicate object 
> should not (must not?) give access to this object to an 
> object that he does 
> not rely on.  In our standard example, If Carol is delicate 
> and Alice relies 
> on Carol, then Alice may only give Bob access to Carol if 
> Alice relies on 
> Bob.  If Carol is a server or is suspected by Alice, then 
> Alice may give a 
> suspect Bob access to Carol.
> 
> 
> Return Types
> 
> "def foo(...) : rely(Stack)"  means that "foo" is vouching for the 
> correctness of the returned value as a Stack.  If the 
> returned value is not 
> correct, then "foo" is not correct.  OTOH, "def foo(...) : 
> suspect(Stack)" 
> means "Don't blame me".  "foo" is not vouching for the 
> correctness of the 
> returned value.  For example, consider a collection of Stack objects:
> 
>     def StackMap {
>         to put(name : String, stack : suspect(Stack)) {...}
>         to get(name : String) : suspect(Stack) {...}
>     }
> 
> This collection stores and retrieves Stacks by name.  In 
> order to provide 
> the hypothetically useful guarantee that the collection only contains 
> objects that satisfy the checkable conformance to Stack, put 
> insists on this 
> as a checked precondition.  However, this is the extent of 
> what it can 
> check, so this is the extent of what it promises to ensure.  When you 
> retrieve a Stack, you get what you put in.  GIGO.  If the 
> returned Stack 
> isn't correct, that is not a claim against the correctness of 
> StackMap.
> 
> It's plausible that an object will typically stand behind the 
> correctness of 
> it returned values, by declaring its return types "rely".
> 
> What about the "name : String" declaration above?  Well, 
> besides "rely" and 
> "suspect", there is a third case: checkable conformance (and possibly 
> coercion) to a particular implementation.  "name : String" is 
> like "name : 
> suspect(String)" in that it only expresses what it can 
> enforce, but it's 
> like "name : rely(String)" as name will now be guaranteed as being as 
> correct as this particular implementation is.  In this case, 
> in E, the 
> implementation is part of the UTCB, and so is implicitly 
> assumed to be correct.
> 
> 
>                                          Static Checking Rules
> 
> 
> This area wide open, and I've only scratched the surface.  As 
> a starting 
> point, in order to reuse type checking machinery, 
> "suspect(Foo)" might 
> effectively be considered a supertype of "rely(Foo)".  For 
> example, given:
> 
>     def a : rely(Foo)
>     def b : suspect(Foo)
> 
> then
> 
>     b := a
> 
> looks ok, but
> 
>     a := b
> 
> is cause for alarm.  It looks plausible that we might be able 
> to sound this 
> alarm at static checking time.  This would break important 
> new ground, 
> especially in the ability for such code to remain secure 
> under maintenance. 
> 
>         Cheers,
>         --MarkM
> 
> _______________________________________________
> e-lang mailing list
> e-lang@mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/e-lang
>