Comments requested on paper: functional purity in Joe-E

[Adrian Mettler]

Resending with URL instead of attachment, as it appears moderator
approval isn't happening:
http://www.cs.berkeley.edu/~amettler/purecomp.pdf

-

David Wagner and I have recently submitted our first paper relating to
our work on Joe-E, an object-capability subset of Java.  It focuses on a
simple pattern that ensures that a method is side-effect free and
behaves as a deterministic function of its arguments (i.e. invocations
with equivalent arguments will yield equivalent return values) and how
this property can be used to verify security properties.  We would be
interested in comments from more people in order to improve the paper.
There's a fair amount of time before any camera ready would be due (it's
still a while before committee decision comes back).

Thanks,
Adrian



_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang

[Toby Murray-4]

That's a seriously interesting paper. It never occurred to me how useful
the Joe-E overlay type system could be for program verification until
now.

(It looks like this work leverages some of the "best of both worlds"
between work on languages and process calculi. Lots of work on process
calculi, such as those derived from the pi-calculus, has focused on
developing type systems for verifying similar properties. This work
appears to "lift" that to a real-world language, leveraging properties
of the object-capability model (e.g. references can only be passed on
other references) to ensure the type system is sound. This is comparable
with the process calculi work which often leverages properties of the
underlying calculus (e.g. names can only be communicated via other names
in pi-calculus) to ensure their type systems are sound. However, your is
inherently more useful since people actually happen to write real code
in Java.)

Some comments as I'm reading, mostly small nitpicks:

Sect 3:

"In particular, references serve as capabilities, and capabilities can
be granted only be explicitly passing references. For instance, the
global scope must not cantain any capabilities."

That second sentence sounds problematic. Surely the global scope does
contain capabilities, e.g. capabilities to constructors to safe classes
and those to immutable objects, right?


Sect 4.3:

Consider changing "Similarly, we treat null pointers as references to a
canonical null object belonging to every type." to
"Similarly, we treat null pointers as references to a single coninical
null object that belongs to every type.". When I read the original
sentence, I misinterpreted it to mean that there was a different
canonical null object for every type -- not that there was a single
canonical null object that could be considered to be of every type.
Perhaps this was just me not paying close attention...


Sections 3 to 5:

The paper states, informally, what immutability is. It also informally
defines side-effect freeness. It formally defines determinism in terms
of equivalence of reference lists, which is itself fairly formally
defined. It then says that functional purity (which requires both
determinism and side-effect freeness) can be enforced by ensuring access
to only immutable objects.

I don't see why the formal definition of determinism is given at all,
since it is never connected with the idea of immutability via
equivalence. Instead, only informal arguments are given in Section 5
that having access only to immutable objects (and the rules of the
object-capability language) gives rise to determinism. Unless
immutability is defined in terms of equivalence, one cannot use access
only to immutable arguments to imply determinism -- at least not
formally. This problem doesn't exist with side-effect freeness since it
is only defined informally. However, it makes the argument that
side-effect freeness is enforced only an informal one.

Instead you could

 -- define immutability in terms of equivalence
 -- use this and the properties of the object-capability model to prove
that a method with access to only immutable arguments is in fact
deterministic, or at least sketch out this argument
 -- define side-effect freeness in terms of immutability
 -- use this and the properties of the object-capability model to prove
that a method with access to only immutable arguments is in fact
side-effect free, or at least sketch out this argument

As the paper is, the reader must make this connection themselves. It
also makes (to me) the trouble of defining determinism formally a bit of
a distraction, since this formal definition is not used in the arguments
that immutability implies functional purity. It is a logical and natural
one to make, but I would argue that it should be being made explicitly
and formally by the paper and not implicitly by the reader.

That said, I'm probably being far too picky here. I expect you've
included as much of the details as you can without going over budget on
length and understand that these sorts of tricky trade-offs always need
to be made.
 

(Am yet to read past Section 6 but might pester with more comments about
later sections as I read them.)

Cheers again for such a cool paper. I'm really enjoying reading it and I
think the ideas it embodies are really powerful -- mostly because of
their inherent usefulness to verifying real properties on real code.
It's a very refreshing alternative to my own work.

Cheers

Toby

On Tue, 2008-06-03 at 23:00 -0700, Adrian Mettler wrote:

> Resending with URL instead of attachment, as it appears moderator
> approval isn't happening:
> http://www.cs.berkeley.edu/~amettler/purecomp.pdf
>
> -
>
> David Wagner and I have recently submitted our first paper relating to
> our work on Joe-E, an object-capability subset of Java.  It focuses on a
> simple pattern that ensures that a method is side-effect free and
> behaves as a deterministic function of its arguments (i.e. invocations
> with equivalent arguments will yield equivalent return values) and how
> this property can be used to verify security properties.  We would be
> interested in comments from more people in order to improve the paper.
> There's a fair amount of time before any camera ready would be due (it's
> still a while before committee decision comes back).
>
> Thanks,
> Adrian
>
>
>
> _______________________________________________
> e-lang mailing list
> e-lang@...
> http://www.eros-os.org/mailman/listinfo/e-lang

_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang

[Mark Miller-2]

On Tue, Jun 3, 2008 at 11:00 PM, Adrian Mettler
<amettler@...> wrote:
> Resending with URL instead of attachment, as it appears moderator
> approval isn't happening:
> http://www.cs.berkeley.edu/~amettler/purecomp.pdf

Hi Toby, sorry about that. I never did see the notification. I just
searched my spam folder and it's not there either. Don't know what
happened. Approved now (though URLs are probably better anyway).

Looks like a great paper -- very glad to see it! Comments later...

--
Text by me above is hereby placed in the public domain

 Cheers,
 --MarkM
_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang

[Sandro Magi-3]

Just skimming the paper at the moment. I noticed this in Section 7.5:

"but was designed and implementing following object-capability principles"

Should be "implemented".

Sandro

Adrian Mettler wrote:

> Resending with URL instead of attachment, as it appears moderator
> approval isn't happening:
> http://www.cs.berkeley.edu/~amettler/purecomp.pdf
>
> -
>
> David Wagner and I have recently submitted our first paper relating to
> our work on Joe-E, an object-capability subset of Java.  It focuses on a
> simple pattern that ensures that a method is side-effect free and
> behaves as a deterministic function of its arguments (i.e. invocations
> with equivalent arguments will yield equivalent return values) and how
> this property can be used to verify security properties.  We would be
> interested in comments from more people in order to improve the paper.
> There's a fair amount of time before any camera ready would be due (it's
> still a while before committee decision comes back).
>
> Thanks,
> Adrian
>
>
>
> _______________________________________________
> e-lang mailing list
> e-lang@...
> http://www.eros-os.org/mailman/listinfo/e-lang

_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang

[Toby Murray-4]

On Wed, 2008-06-04 at 08:39 -0700, Mark Miller wrote:
> On Tue, Jun 3, 2008 at 11:00 PM, Adrian Mettler
> <amettler@...> wrote:
> > Resending with URL instead of attachment, as it appears moderator
> > approval isn't happening:
> > http://www.cs.berkeley.edu/~amettler/purecomp.pdf
>
> Hi Toby,

You mean Adrian ;)

>  sorry about that. I never did see the notification. I just
> searched my spam folder and it's not there either. Don't know what
> happened. Approved now (though URLs are probably better anyway).
>
> Looks like a great paper -- very glad to see it! Comments later...
>
_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang

[Mark S. Miller-2]

On Wed, Jun 4, 2008 at 8:48 AM, Toby Murray <toby.murray@...> wrote:
>> Hi Toby,
>
> You mean Adrian ;)

Indeed!


--
    Cheers,
    --MarkM
_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang

[Toby Murray-4]

On Wed, 2008-06-04 at 14:19 +0100, Toby Murray wrote:
> That's a seriously interesting paper. It never occurred to me how useful
> the Joe-E overlay type system could be for program verification until
> now.

> (Am yet to read past Section 6 but might pester with more comments about
> later sections as I read them.)

Have now finished the paper; comments for remaining sections below.

Section 7.2.2

"The last received serial number was stored as a static field inside the
BallotMessage ..." -- linebreak required before "BallotMessage".

"After refactoring, the method was changed to use a ByteArray instead of
byte[]." Wouldn't the method also need to be changed to return a Ballot
object rather than a boolean and to throw an exception upon error rather
than (presumably) returning false ?

Section 7.3.4

More linebreak failures due to \tt{} fonts on "IsEqualFilter"

"In particular, there cannot be any cycles in immutable data
structures." I don't get this.. What about

public class Bar implements Immutable{
   private Foo _foo;
   public Bar(Foo foo){
      _foo = foo;
   }
}
public class Foo implements Immutable{
   private Bar _bar;
   public Foo(){
      _bar = new Bar(this);
   }
}

Would Foo not be considered Immutable?


Overfull second-to-last line in Section 7.3.4



Again, very cool stuff. Cheers for the good read.

Toby

> On Tue, 2008-06-03 at 23:00 -0700, Adrian Mettler wrote:
> > Resending with URL instead of attachment, as it appears moderator
> > approval isn't happening:
> > http://www.cs.berkeley.edu/~amettler/purecomp.pdf
> >
> > -
> >
> > David Wagner and I have recently submitted our first paper relating to
> > our work on Joe-E, an object-capability subset of Java.  It focuses on a
> > simple pattern that ensures that a method is side-effect free and
> > behaves as a deterministic function of its arguments (i.e. invocations
> > with equivalent arguments will yield equivalent return values) and how
> > this property can be used to verify security properties.  We would be
> > interested in comments from more people in order to improve the paper.
> > There's a fair amount of time before any camera ready would be due (it's
> > still a while before committee decision comes back).
> >
> > Thanks,
> > Adrian
> >
> >
> >
> > _______________________________________________
> > e-lang mailing list
> > e-lang@...
> > http://www.eros-os.org/mailman/listinfo/e-lang
> _______________________________________________
> e-lang mailing list
> e-lang@...
> http://www.eros-os.org/mailman/listinfo/e-lang

_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang

[Tyler Close]

Nice paper! It's great to have something written down that better
motivates use of the Joe-E verifier.

I had a couple of thoughts while reading the paper than seem worth
incorporating.

+Caller beware+

Section 2.3 on "Untrusted code execution" might seem to be making
slightly stronger claims than can be supported. The section might
leave a reader with the impression that untrusted pure code can be
executed without further worry. For example, the section closes with:

"Once verified as pure, any such plug-in could be downloaded and
executed safely; it cannot gain any information about other private
information stored on the system, nor can it corrupt the state of any
other part of the program."

But a security review would be concerned not only with the direct
invocations made by the plug-in, but also with the invocations the
plug-in can induce its caller to make. For example, a PostScript
renderer plug-in may have an intermediate output that specifies the
names of needed fonts, which the caller should load from the local
filesystem. Though the PostScript renderer doesn't have direct access
to the filesystem, which would break purity, perhaps it can induce its
non-pure caller to access the information and provide it to the next
stage of the plug-in's pure computation. Similarly, a non-pure caller
may have access to a source of non-determinism and inadvertently
communicate this non-determinism to the pure plug-in by the sequence
of calls made, or arguments provided.

+Any Joe-E code can be made pure+

Section 8 on "Discussion" almost says it, but not quite. Any code that
passes the Joe-E verifier can be wrapped in a pure method. So if
you've got some Joe-E code that isn't pure, you can make a pure
interface to it that requires more specific, Immutable arguments and
then calls the non-pure Joe-E code, or constructs new instances of
non-Immutable classes. The moral being that if you've got an algorithm
that you think would benefit from being pure, you can always succeed
in making it pure.

--Tyler

"Verifiable functional purity in Java"
<http://www.cs.berkeley.edu/~amettler/purecomp.pdf>
_______________________________________________
e-lang mailing list
e-lang@...
http://www.eros-os.org/mailman/listinfo/e-lang