JSONSerializer review, further study of reviewable coding techniques

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.

The idea: Add a marker interface, Library.  The intended semantics
are that, if C implements Library, then C is not subclassable by Joe-E
code.  The Joe-E verifier would need to be extended, so that it rejects
any Joe-E code that attempts to define a class that is a subtype of
Library.  Then org.joe_e_.ConstArray could be marked to implement Library.
Similarly, we could look whether there are other relevant parts of the
Joe-E library or Java library that can be usefully be marked Library.
In the case of Java libraries, specific Java classes could be marked
honorarily Library.  For instance, it might be useful to mark
java.math.BigInteger as honorarily Library, so that code which accepts
a BigInteger from an untrusted source can trust the behavior of the
BigInteger object.

I believe we've discussed this idea before.  This has previously been
discussed in the context of using the type system to make it easier to
reason about behavior of certain objects.  However, it would also be
applicable to your particular goal: if ConstArray were marked Library
and Joe-E code were forbidden from subclassing subtypes of Library, then
it might be slightly easier to verify that method calls on a ConstArray
cannot transfer control to application code.  You might still need the
implementation comment, but it might be easier for auditors to verify
the correctness of the implementation comment, and this would generalize
neatly beyond ConstArrays.

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


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?