[e-lang] JSONSerializer review, further study of reviewable coding techniques

David Wagner daw at cs.berkeley.edu
Sat Aug 16 20:32:16 CDT 2008

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.

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.

Other things a code reviewer needs to confirm about this code:

 * Type is honorarily immutable.
 * ValueWriter behaves deterministically (unless it throws
   IOException or Error)
 * this code never catches IOExceptions

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.

More information about the e-lang mailing list