When is a JavaScript program "correct"? (was: Setting a property in the prototype chain?)

# Dmitry A. Soshnikov (14 years ago)

On 11.04.2011 18:07, Mark S. Miller wrote:

On Sun, Apr 10, 2011 at 11:21 PM, David Herman <dherman at mozilla.com <mailto:dherman at mozilla.com>> wrote:

I wondered if someone was going to make this point.

> That should be
>
>          while (!{}.hasOwnProperty.call(obj, key))
>
> which works even if obj has an own property named 'hasOwnProperty'.

Not if someone mutates Object.prototype.hasOwnProperty or
Function.prototype.call. I don't think we need to polish a proof
of concept.

First, I agree that for the original purpose of this thread, this polishing is irrelevant, so I have changed the subject. But your counter-examples do help to highlight something I've been thinking about. Because of such pervasive mutability, we really haven't had a clear notion of "correctness" for JavaScript. For normal JavaScript programs, if run after some other code has already mutated that environment's primordials arbitrarily, there's so little they can count on that very few programs could be written "correctly" under these onerous assumptions[1]. For the notion of "correctness" in JavaScript to be useful, I think we must allow JavaScript programs to rely on the primordial at least continuing to obey their original contract. However, the use of objects as maps from strings to values is pervasive, e.g., in JSON unserialization, so we should not allow general purpose JavaScript programs to rely on, for example, 'hasOwnProperty' not being overridden.

Retrofitting a reasonable theory of correctness after the fact is a tricky exercise. The above theory represents a practical compromise between the assumption that common programs make (primordials obey their original contracts) vs. the assumptions that common programs break (hasOwnProperty is not overridden). Thus, I claim that the original program should not be considered "correct", while the modified program should, despite the problematic cases raised by your counter-example.

As I see it, you address the "issue" of unstratified meta-programming (note, I take the "issue" in quotes, since there's no a single meaning whether the unstratified meta-level is so bad).

It depends on how to look on the issue. On one hand, why if a user changes the behavior of the hasOwnProperty of his object in his program, then the program should be considered as incorrect? The user knows how to handle hasOwnProperty for the particular object and the ability to override it is the ability to control unstratified meta-level via simple reassigning to meta-hooks.

On the other hand, yes, since we have the ability to modify any JS code via console or even via browser address bar (using pseudo-protocol javascript:), then it can be viewed as the issue and as a security program.

But the salvation by the big deal should not be found in making a dynamic language as a completely frozen and static, but in the disallowing of code modification (code injection, code poisoning if you will) via such a simple tools as the console or address bar.

Having the ability to inject the needed code via console just makes e.g. browser scripting as just an addition for the server code. This is in case if we have combined client-server application. It's obvious, that if we have some validation tool, then the validation on the client side should be done only as the convenient addition. But the same validation will be done on the server, since we understand that the client code can be easily injected (the simplest example e.g. utils.validate = function () { return true; } which always will return positive result).

If we have only client-side application, then the user, if breaks some code via injection just breaks his own page and therefore just refuses the convenience we wanted to give him. He doesn't break anything besides his own page.

So that's the language is dynamic and allow to change objects in runtime is not in my view about "correctness" of a program. A programmer, having control of his code, knows how and why he wants to augment and modify his current runtime objects and code.

From this viewpoint I don't think we need to disallow modifying of hasOwnProperty and similar. Better then to reuse ES5 approach and separate this meta-operation to Object.hasOwnProperty(foo).

The fact that a language is static perhaps doesn't cancel the fact that the code still can be injected, etc. So again, IMO a "correct program" is not about "let's freeze everything here". And "predefined and predicted contract" also relates to statics mostly. In "duck typing" exactly this contract can be achieved during the runtime -- one line before an object cannot pass the "duck-test", on the other line (after some mutations) it already can do this, it satisfies the contract -- and it's achieved not via statics in the language.

Dmitry.

# Mark S. Miller (14 years ago)

On Sun, Apr 10, 2011 at 11:21 PM, David Herman <dherman at mozilla.com> wrote:

I wondered if someone was going to make this point.

That should be

     while (!{}.hasOwnProperty.call(obj, key))

which works even if obj has an own property named 'hasOwnProperty'.

Not if someone mutates Object.prototype.hasOwnProperty or Function.prototype.call. I don't think we need to polish a proof of concept.

First, I agree that for the original purpose of this thread, this polishing is irrelevant, so I have changed the subject. But your counter-examples do help to highlight something I've been thinking about. Because of such pervasive mutability, we really haven't had a clear notion of "correctness" for JavaScript. For normal JavaScript programs, if run after some other code has already mutated that environment's primordials arbitrarily, there's so little they can count on that very few programs could be written "correctly" under these onerous assumptions[1]. For the notion of "correctness" in JavaScript to be useful, I think we must allow JavaScript programs to rely on the primordial at least continuing to obey their original contract. However, the use of objects as maps from strings to values is pervasive, e.g., in JSON unserialization, so we should not allow general purpose JavaScript programs to rely on, for example, 'hasOwnProperty' not being overridden.

Retrofitting a reasonable theory of correctness after the fact is a tricky exercise. The above theory represents a practical compromise between the assumption that common programs make (primordials obey their original contracts) vs. the assumptions that common programs break (hasOwnProperty is not overridden). Thus, I claim that the original program should not be considered "correct", while the modified program should, despite the problematic cases raised by your counter-example.

[1] SES initialization freezes the primordials, so SES programs can safely assume they are frozen. But the point I'm making here are not specific to SES.

# David Bruant (14 years ago)

Le 10/04/2011 23:27, Dmitry A. Soshnikov a écrit :

On 11.04.2011 18:07, Mark S. Miller wrote:

On Sun, Apr 10, 2011 at 11:21 PM, David Herman <dherman at mozilla.com <mailto:dherman at mozilla.com>> wrote:

I wondered if someone was going to make this point.

> That should be
>
>          while (!{}.hasOwnProperty.call(obj, key))
>
> which works even if obj has an own property named 'hasOwnProperty'.

Not if someone mutates Object.prototype.hasOwnProperty or
Function.prototype.call. I don't think we need to polish a proof
of concept.

First, I agree that for the original purpose of this thread, this polishing is irrelevant, so I have changed the subject. But your counter-examples do help to highlight something I've been thinking about. Because of such pervasive mutability, we really haven't had a clear notion of "correctness" for JavaScript. For normal JavaScript programs, if run after some other code has already mutated that environment's primordials arbitrarily, there's so little they can count on that very few programs could be written "correctly" under these onerous assumptions[1]. For the notion of "correctness" in JavaScript to be useful, I think we must allow JavaScript programs to rely on the primordial at least continuing to obey their original contract. However, the use of objects as maps from strings to values is pervasive, e.g., in JSON unserialization, so we should not allow general purpose JavaScript programs to rely on, for example, 'hasOwnProperty' not being overridden.

Retrofitting a reasonable theory of correctness after the fact is a tricky exercise. The above theory represents a practical compromise between the assumption that common programs make (primordials obey their original contracts) vs. the assumptions that common programs break (hasOwnProperty is not overridden). Thus, I claim that the original program should not be considered "correct", while the modified program should, despite the problematic cases raised by your counter-example.

As I see it, you address the "issue" of unstratified meta-programming (note, I take the "issue" in quotes, since there's no a single meaning whether the unstratified meta-level is so bad).

It depends on how to look on the issue. On one hand, why if a user changes the behavior of the hasOwnProperty of his object in his program, then the program should be considered as incorrect? The user knows how to handle hasOwnProperty for the particular object and the ability to override it is the ability to control unstratified meta-level via simple reassigning to meta-hooks. From what I understand of Mark's definition of correctness, this case is

not excluded. My understanding is that Mark tries to provide a uniform meaning to answers to questions like "is this piece of code /correct/?". I interpret what he said as "a program can be considered as correct if it does what we expect it to do within a fresh ES environment". With that interpretation in mind, if the program you want to evaluate redefines Object.prototype.hasOwnProperty and uses consistently this new definition to achieve its goal, then it will be considered correct.

One property of this definition must be noted. Appending two independently "correct" programs may result in an incorrect program (if the first one changes a piece of environment on which the second relies).

Most of what you said afterward regarded dynamic validation, I think, which wasn't part of Mark's definition as I understand it (I agree on what you said, though).

# Mark S. Miller (14 years ago)

On Sun, Apr 10, 2011 at 5:27 PM, Dmitry A. Soshnikov < dmitry.soshnikov at gmail.com> wrote:

As I see it, you address the "issue" of unstratified meta-programming (note, I take the "issue" in quotes, since there's no a single meaning whether the unstratified meta-level is so bad).

It depends on how to look on the issue. On one hand, why if a user changes the behavior of the hasOwnProperty of his object in his program, then the program should be considered as incorrect? The user knows how to handle hasOwnProperty for the particular object and the ability to override it is the ability to control unstratified meta-level via simple reassigning to meta-hooks.

Hi Dmitry, your response makes clear two issues I failed to explain well:

By "program", I do not mean a whole program, i.e., the totality of all code run within a given JS environment. David's original getDefiningObject function and variations are clearly not whole programs. Rather, they are reusable program fragments that could be packaged in reusable libraries, meant to be link into and used from within larger programs that the author of getDefiningObject should not need to know about.

Since we're not worried here about programming under mutual suspicion, it could very well be valid for getDefiningObject to assume that various methods are overridden in a contract preserving manner. For example, a Java hashtable that calls a key's "hashCode" method could be correct. The key's hashCode method might be incorrect, in which case the hastable would function incorrectly, but we'd say that this incorrect behavior is the key's fault rather than the hashtable's fault.

We would like a notion of correctness that allows us to reason in a modular manner: A correct composition of individually correct components should yield a correct composite, where the correctness of the composition depends only on the contracts of the components to be composed -- not on their implementation. The Java composite above is incorrect because the key is incorrect. This does not contradict the notion that the hashtable abstraction by itself is correct even though in this case it behaves incorrectly.

The problem here is specifically with the methods on Object.prototype vs the pervasive use of objects as string->value maps in JavaScript. What are we to

do about

getDefiningObject(JSON.parse(str), 'foo')

? Even without mutual suspicion within the program code, we would like to reason about the correctness of this as quantified over all strings, for example, even if the string is received from an external untrusted or unreliable source.

# Mike Samuel (14 years ago)

2011/4/11 Mark S. Miller <erights at google.com>:

We would like a notion of correctness that allows us to reason in a modular manner: A correct composition of individually correct components should yield a correct composite, where the correctness of the composition depends only on the contracts of the components to be composed -- not on their implementation. The Java composite above is incorrect because the key is incorrect. This does not contradict the notion that the hashtable abstraction by itself is correct even though in this case it behaves incorrectly. The problem here is specifically with the methods on Object.prototype vs the pervasive use of objects as string->value maps in JavaScript. What are we to do about     getDefiningObject(JSON.parse(str), 'foo') ? Even without mutual suspicion within the program code, we would like to reason about the correctness of this as quantified over all strings, for example, even if the string is received from an external untrusted or unreliable source.

Would you agree with the following?:

Given that stackoverflow.com and user-commenting documentation sites ( www.php.net/manual/en/ref.pcre.php ) encourage teaching by sharing copy/pasteable snippets of source code, we would like experienced devs to be able to compose succinct snippets that can be shared without an accompanying page of caveats that few will read or know how to check.

# Mark S. Miller (14 years ago)

On Mon, Apr 11, 2011 at 2:48 PM, Mike Samuel <mikesamuel at gmail.com> wrote:

2011/4/11 Mark S. Miller <erights at google.com>:

We would like a notion of correctness that allows us to reason in a modular manner: A correct composition of individually correct components should yield a correct composite, where the correctness of the composition depends only on the contracts of the components to be composed -- not on their implementation. The Java composite above is incorrect because the key is incorrect. This does not contradict the notion that the hashtable abstraction by itself is correct even though in this case it behaves incorrectly. The problem here is specifically with the methods on Object.prototype vs the pervasive use of objects as string->value maps in JavaScript. What are we to do about getDefiningObject(JSON.parse(str), 'foo') ? Even without mutual suspicion within the program code, we would like to reason about the correctness of this as quantified over all strings, for example, even if the string is received from an external untrusted or unreliable source.

Would you agree with the following?:

Given that stackoverflow.com and user-commenting documentation sites ( www.php.net/manual/en/ref.pcre.php ) encourage teaching by sharing copy/pasteable snippets of source code, we would like experienced devs to be able to compose succinct snippets that can be shared without an accompanying page of caveats that few will read or know how to check.

Excellent. +1

# Dmitry A. Soshnikov (14 years ago)

On 11.04.2011 22:37, Mark S. Miller wrote:

On Sun, Apr 10, 2011 at 5:27 PM, Dmitry A. Soshnikov <dmitry.soshnikov at gmail.com <mailto:dmitry.soshnikov at gmail.com>> wrote:

As I see it, you address the "issue" of unstratified
meta-programming (note, I take the "issue" in quotes, since
there's no a single meaning whether the unstratified meta-level is
so bad).

It depends on how to look on the issue. On one hand, why if a user
changes the behavior of the `hasOwnProperty` of _his_ object in
_his_ program, then the program should be considered as incorrect?
The user knows how to handle `hasOwnProperty` for the particular
object and the ability to override it is the ability to control
unstratified meta-level via simple reassigning to meta-hooks.

Hi Dmitry, your response makes clear two issues I failed to explain well:

By "program", I do not mean a whole program, i.e., the totality of all code run within a given JS environment. David's original getDefiningObject function and variations are clearly not whole programs. Rather, they are reusable program fragments that could be packaged in reusable libraries, meant to be link into and used from within larger programs that the author of getDefiningObject should not need to know about.

Since we're not worried here about programming under mutual suspicion, it could very well be valid for getDefiningObject to assume that various methods are overridden in a contract preserving manner. For example, a Java hashtable that calls a key's "hashCode" method could be correct. The key's hashCode method might be incorrect, in which case the hastable would function incorrectly, but we'd say that this incorrect behavior is the key's fault rather than the hashtable's fault.

We would like a notion of correctness that allows us to reason in a modular manner: A correct composition of individually correct components should yield a correct composite, where the correctness of the composition depends only on the contracts of the components to be composed -- not on their implementation. The Java composite above is incorrect because the key is incorrect. This does not contradict the notion that the hashtable abstraction by itself is correct even though in this case it behaves incorrectly.

Yes, thanks for clarification, Mark, I understand this and generally agree. Though, the issue of combining two "correct" chunks of a code which may cause then "incorrect" behavior by the meaning of one of the them (or both) is generic. I can even say it's a problem of a "shared state". One chunk thinks that it uses this value from the shared state, meanwhile another chunk has already change it. And it may appear everywhere when we have such a combination of source which can differ in semantics.

E.g. the example I used in explaining "hoisting" with using function declarations. Suppose we have two files foo.js and bar.js. Thus, the code of foo.js is:

function foo() { alert(1); }

foo(); // 2

why does it alerts 2? We tested the code and saw that it alerted 1. But -- it was before we combined foo.js with bar.js (normal practice on the web to combine several sources in one and to obfuscate/minimize it) which contains:

function foo() { alert(2); }

This program now became incorrect while both chunks were correct. And this is because we got "shared state collision". The similar with that hasOwnProperty -- the function which analyze whether an object has a property shares the whole prototype chain in respect of where hasOwnProperty is found -- either original Object.prototype.hasOwnProperty or the injected one, own.

The problem here is specifically with the methods on Object.prototype vs the pervasive use of objects as string->value maps in JavaScript. What are we to do about

getDefiningObject(JSON.parse(str), 'foo')

? Even without mutual suspicion within the program code, we would like to reason about the correctness of this as quantified over all strings, for example, even if the string is received from an external untrusted or unreliable source.

Yeah, but unfortunately to support "nearly correct" behavior we should:

  • to avoid inheritance at all;
  • to make objects as simple hash-tables without prototypes (consequence from the first point);
  • to move all meta- and system- operations to the separate space.

We can argue why to avoid inheritance? Because then we can say, that "foo.js" expected that some method called on instance would behave in a way we expect, but the object defined in "bar.js" has already overwritten it and uses own implementation. Is the program still correct or incorrect? Which chunk has decided it so -- foo.js or bar.js? Or their combined version? If it's incorrect, then there should be no inheritance with ability to shadow -- but this is a casual code reuse today.

Or we can remove from inheritance only meta-operations (this is from what I've started) -- stratified and unstratified meta-levels. Again, objects are just simple hash-tables without any meta-operation (btw, e.g. toString -- whether it's a meta-operation?) but have prototypes.

So in general this issue of "mutable shared state" applied to this particular case isn't solve directly. Just with big limitations which reduce convenience of the usage -- I remember I argued that:

Object .create(...) .defineProperty(...) .freeze()

is much more elegant than this with indention hazard and repeating over and over again this Object. - Object. - Object -

Object.freeze( Object.defineProperty( Object.create( ... ) ) )

But this is a solution to fix somehow this "unstratified meta-level with possible injection or shared sources" issue.

Dmitry.

# David Herman (14 years ago)

Sure, I'll buy that. There's a qualitative difference in how uncooperatively your program is behaving if it mutates primordials to violate their usual contracts, as opposed to simply creating an object that overrides hasOwnProperty, which ought to be allowed.

The word "theory" might be a little loaded, but at least "practical advice on how to write reasonable/cooperative code" is important for programmers to know how to avoid unintended (i.e., not malicious) interactions between different interacting bits of JS code. I think this is part of what good JS programmers have to learn, and to date there's sadly not enough good, authoritative material with that kind of advice ("how not to be anti-modular").