Re: Security and Vulnerability Assessment of an E Program

On Wed, 2008-09-17 at 13:51 -0500, Jimmy Wylie Jr. wrote:
> But what about the Auditing framework?  Wouldn't this also help in
> this model verification? You could just skip over anything that
> implements Confined or Functional similar to the idea in the paper on
> functional purity in Joe-E.

The Joe-E solution to functional purity creates subgraphs of the entire
object graph that are immutable. One would need to show that a model of
the entire graph is equivalent to a model of its non-immutable parts.
This is indeed an interesting idea. 

> What advantages does the model verification have over some sort of
> static authority analysis along with auditors?  I would think it would
> be the ability to create new patterns and test them with mathematical
> vigor before actually implementing them in the language. And, How is
> this related to a mechanism like Java's Bytecode Verifier? or would E
> not need a mechanism like that, since an Emaker is simply E source
> code imported with no Authority, and would be interpreted by a trusted
> interpreter on your machine? 

I think you're correct here. One must trust the interpreter (or the
Joe-E verifier or whatever) to enforce the object-capability rules.

One advantage of formal verification via model checking over e.g.
auditors is that the former allows us to reason about a pattern in a
number of different contexts -- e.g. between a language and an OS. I
would argue that both techniques are complementary.


> Thanks again for the information.  I particularly liked your membrane
> explanation, I had read the code for it in  E in a Walnut but the
> explanation isn't complete yet. Your explanation definitely clarified
> my understanding of the pattern.

Thanks, I'm glad. Providing succinct descriptions of the patterns was
harder than I thought it was going to be. I hope I've succeeded
somewhat.

Cheers

Toby