Several times over the past couple of weeks, I have wanted to make some sort of assertion about an invariant in Mozilla. Now, some invariants are easier to prove than others. For example, if I wanted to prove that a particular variable (such as nsHTMLDocument::mWriteState) only ever has one of four values, I can enlist the C++ type system and an enum to help check and enforce that for me. To me, the important point is not how the invariant is proven, just that it is proven.

For a more difficult example, I might want to show that, in a web page’s <script> tags, all scripted functions are allowed to access their scope chains. This might seem like a vacuous invariant to prove, but given that whether we either do or don’t perform security checks depends on this invariant, it seems worth the exercise. However, if you get the point and don’t want to slog through a fairly involved example involving JS and caps you might want to skip to the last paragraph for the punchline.

Unlike the first example, the C++ type system cannot help us here. Instead, we first make an assumption: any time we compile JS code, the principal we compile that code with is equal to the principal of the scope chain (you can check this assumption by reading nsScriptLoader::EvaluateScript). Now, we note that in nsScriptSecurityManager, to compute the privileges (principals) of a function, there are two cases: functions are either cloned (in which case they inherit the principal from their parent) or not (in which case, we use the principal of their script). So, we can say that our invariant holds true for any non-cloned function (thanks to our assumption earlier).

Now, what about cloned functions? Well, since we only care about functions in the <script> element, we only have to see how these functions are cloned. Scanning through js/src/*.cpp we can see that the parent argument to js_CloneFunctionObject is always cx->fp->scopeChain. Great! To finish, we go check what a scripted function’s scope chain is set to when it’s called. A quick glance at jsinterp.cpp verifies that the function’s parent is used as the scope chain, and we’re done. For extra credit (and to make this particular example useful) you can also prove that functions cloned by jsinterp.cpp keep the same principal (which, with what we’ve shown here, tells us that it’s OK to not do security checks when looking stuff up on the scope chain).

Whew, so that wasn’t so bad, right? (Hah!) I have the advantage of having worked on this code for the past 3 years, I made some gigantic assumptions (that I can back up) and was able to do most of that without cracking open my editor. Furthermore, I don’t think that it’s possible to usefully put that invariant (and why it’s true) into the source code, either as a comment or as part of the code. I say this because there are millions of these assertions, some that cross module boundaries, like this one, and some that only hold true for single functions. As a programmer working on this code, fixing bugs and adding features requires figuring out which invariants are being broken, or which ones I might affect by adding new code.

And finally, this brings me to my question. How can we write code that makes answering a question like “can a scripted function always access its scope chain?” easier? Is it more comments? Better variable names? I ask because these two examples were relatively easy compared to some of the invariants I’ve been dealing with lately, and when you’re writing code in C++ (and when that code implements a security system for a web platform) they don’t get less important.

Comments are off for this post