Re: JSONSerializer review, further study of reviewable coding techniques

Hi David,

Responses inline below...

On Sat, Aug 16, 2008 at 6:32 PM, David Wagner <[email protected]> wrote:
> The goal: verify these two security claims about JSONSerializer:
>
>  SECURITY CLAIM: Only the immutable root of the application object
>  tree provided by the values argument is serialized.  [...] repeated
>  serialization of an object tree produces identical JSON text
>  (assuming the Exporter behaves deterministically).
>
>  SECURITY CLAIM: Iteration of the immutable root is done without
>  causing execution of application code. This constraint ensures that
>  serialization has no effect on the application object tree.

Just keeping the link here for the archives...

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

> Tyler Close writes:
>>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?
>
> These are great questions.  I don't have any useful answers.
>
> I failed to come up with any way to structure this code to make it
> easier to verify.  For serialize(), it seems there are three cases:
>
>  (a) value is a non-application type.  In this case the behavior
>      of method calls on it is predictable, so we can check that
>      the behavior will be deterministic and will satisfy the claims.
>
>  (b) value is Frozen.  In this case, the claim is that the code
>      only accesses fields one level deep, and never calls methods
>      on value.  This requires manual code inspection.
>
>  (c) remaining cases.  In this case, all we do is pass it to the
>      Exporter, which is presumed to have deterministic behavior.
>
> Even if the Joe-E verifier provided a Frozen marker interface, you'd
> still have to verify that the code doesn't call methods and only accesses
> fields one level deep and uses them only as arguments to a recursive
> invocation of serialize().  That doesn't sound terribly amenable to
> general-purpose verification support.

I think this problem is still tractable. Let's say our goal is for a
reviewer to be able to judge the validity of the noted security
claims, using only the method signature of JSONSerializer.write(), and
so ignoring its implementation.

Let's assume the existence of a variable annotation: "@inert". For
variables with this annotation, the Joe-E verifier checks that:
1. On access to a field of the referent, the field MUST be final and
the accessed value MUST be assigned to another variable that either:
    a. has the @inert annotation,
    b. or is of type Immutable.
2. On invocation of a method of the referent, the referent MUST be Immutable.

Let's assume the Exporter interface is:

public interface
Exporter {
    public String
    run(@inert Object value);
}

and that we change the signature of the JSONSerializer.write() method to:

static public String
write(final Exporter export, final @inert ConstArray<?> values);

Given this API, a security reviewer can determine:
- the value of the returned string is determined solely by the state
of the Exporter and the final state of the values argument; therefore,
a repeated call to JSONSerializer.write() with the same arguments will
result in identical JSON text, if the Exporter is deterministic.
- JSONSerializer.write() is unable to mutate any state reachable via
the values argument; therefore, execution of JSONSerializer.write()
can have no effect on these arguments.

This meets our stated goal for the reviewer, but we don't yet have the
implementation flexibility we need. The Exporter's job is to hold onto
a map of [ exported URL string => value ]. The values in this map may
at some later time be subjected to mutations, and so cannot be @inert.
Since the caller of JSONSerializer.write() possesses non-@inert access
to the values argument, it should be able to get non-@inert access to
anything passed to the Exporter. Let's say the caller looks like:

final ConstArray<?> values = ...
final String text = JSONSerializer.write(new Exporter() {
    public String
    run(final Object value) {
         ...
    }
}, values);

Since Joe-E can tell that JSONSerializer.write() does not have access
to any state for which the @inert annotation must be enforced, it can
determine that it is OK for the instantiated Exporter to not apply the
@inert annotation to its value parameter, since any argument to this
method could not be @inert from the perspective of this lexical scope.
For this logic to work, the @inert annotation MUST ONLY be applicable
to local variable declarations and parameter declarations. It MUST NOT
be applied to field declarations. Java annotations support this
distinction.

We'll also need a way for Joe-E to know it's OK to iterate over an
@inert ConstArray and to access the value of a final field via Joe-E's
reflection API. We could just special case these.

QED?

> Other things a code reviewer needs to confirm about this code:
>
>  * Type is honorarily immutable.

Why is that needed?

>  * ValueWriter behaves deterministically (unless it throws
>   IOException or Error)
>  * this code never catches IOExceptions

Nice "catch". I think I've rectified this by having the method return
a string, instead of writing to an output stream.

> Two clarifications on the first security claim:
>
>  * write() is deterministic only in the absence of exceptions.
>   If you call write() multiple times with the same arguments,
>   it's possible that it might non-deterministically choose to
>   throw for some of those cases (presumably producing no JSON text
>   in those cases, I hope).  But for all the non-throwing executions,
>   you should get the same JSON text.
>
>  * If you call write() twice with two different Exporter objects,
>   even if each Exporter is individually deterministic, then the
>   first security claim can still be violated if the behavior of
>   those two Exporters differs.  Thus you need to assume that all
>   Exporters behave identically.
>
> I suspect the requirement to verify that code cannot trigger
> execution of application code (or some other code that is untrusted
> for purposes of the particular security goals in scope) is a common
> one.  It would be nice to have support for this.  I don't have any
> concrete suggestions, merely a belief that this kind of security
> claim may be fairly common in object capability programming.

With a little more tweaking, the @inert annotation might be what's
needed here. For example, if we add the following rules:

If a caller provides an @inert argument to a constructor or method,
the returned object MUST be assigned to either an @inert variable, an
Immutable variable, or be the caller's return value. A constructor can
initialize a field using an @inert argument.

For example, given the following API:

class Foo {
    public final Object x;
    Foo(@inert final Object x) {
        this.x = x;
    }
}

static public Foo
bar(@inert final Object x) {
    return new Foo(x);
}

the following code is valid:

final Object a = ...
final Foo aFoo = new Foo(a);
final Foo aBar = bar(a);
return new Foo(a);
return bar(a);
final @inert Object b = ...
final @inert Foo bFoo = new Foo(b);
final @inert Foo bBar = bar(b);
return new Foo(b);
return bar(b);

the following code is invalid:

final Foo bFoo = new Foo(b);
final Foo bBar = bar(b);
return new Foo(b);
return bar(b);

Given the above, I think I could also use the @inert annotation to
enforce many of the security claims in the ref_send library that say
they won't pass the flow of control to a given argument.

--Tyler