Re: JSONSerializer review, further study of reviewable coding techniques

Hi David,

On Fri, Aug 8, 2008 at 10:07 PM, David Wagner <[email protected]> wrote:
> Tyler Close writes:
>>The JSONSerializer has some security relevant constraints to enforce
>>in its implementation, that, AFAICT, aren't readily expressible in the
>>language provided by Joe-E. So this produces some questions:
>>
>>1. Is there an alternate design where the documented constraints could
>>be verified by Joe-E?
>>2. Is there some extension of the Joe-E verifier that would enable
>>this verification?
>>3. If verification is not feasible, what's the best way to explain how
>>the constraints are enforced?
>
> I'm still reading this code, but I noticed the following comment:
>
>  // Application code cannot extend ConstArray, so iteration of the
>  // values array will not transfer control to application code.
>
> If this is an example of a security property you'd like to express,
> I think we do have an idea for how one might verify this, with a simple
> extension to the Joe-E verifier.

Joe-E already provides mechanisms to prevent application code from
extending a class. You can either declare the class to be 'final', or
not declare a public constructor. The ConstArray class already makes
use of the latter technique and so cannot be extended by application
code. I used the quoted comment as a reminder that the JSONSerializer
implementation is relying on this property of ConstArray.

> The idea: Add a marker interface, Library.

...

> What do you think?  Do you think this extension to Joe-E would be
> helpful, or does this miss the essential issue?

So far, I've found the existing techniques for creating non-extensible
classes sufficient.

The security properties I was interested in getting better Joe-E
support for are the ones documented on lines 60 and 69 of the current
JSONSerializer.java implementation:

http://waterken.svn.sourceforge.net/viewvc/waterken/server/trunk/waterken/syntax/src/org/waterken/syntax/json/JSONSerializer.java?view=markup

Before getting into what that support might be, it might be useful to
first come up with a commenting convention for highlighting where an
implementation is making a claim that must be checked by a reviewer.
Your email shows that I currently don't have a good enough distinction
between comments that make a claim that must be checked versus ones
that document their reliance upon something that Joe-E is already
verifying.

For verifier support, first consider this thought experiment. If the
values parameter to the JSONSerializer.write() method were of type
ImmutableArray, it would not be necessary for a reviewer to read the
implementation of the write() method in order to know that the
properties documented on lines 60 and 69 were being enforced. The
Joe-E verifier would be guaranteeing these properties. Now the
question becomes, is there some less stringent verification that could
be done to enforce the documented properties, without requiring the
values parameter to be Immutable? The current implementation of
JSONSerializer implements the documented properties by only accessing
the Immutable sub-graph of the values argument, and not invoking any
method of any object in the graph. I think this is also a stronger
requirement than is necessary to ensure that the documented properties
are being implemented. All we need is to ensure that the code only
accesses final fields, or calls methods that access only final fields.
This seems like a condition that the Joe-E verifier could check.

> P.S. I wonder if it might be useful to have an IDE that provided some
> kind of visualization support to make it easy to spot transfer of control
> to "untrusted" code, e.g., by marking method calls that transfer control
> in red or something.  Of course, there would have to be some way to
> describe to the IDE which objects have "trusted behavior" (hence we're
> not concerned about transferring control to them) vs which objects are
> not, so that the IDE can distinguish usefully.  Do you think this might
> make it easier in a security review to keep an eye out for plan
> interference hazards?

I suspect something along these lines could be very useful.

--Tyler