Skip to content

Latest commit

 

History

History
130 lines (82 loc) · 10.7 KB

proxies.md

File metadata and controls

130 lines (82 loc) · 10.7 KB

Integrity checks on Proxies

This page aims to identify minimal invariant checks needed on trapped internal methods of Proxies in order to maintain the invariants of internal methods as modelled in invariants.md.

Fundemental observation methods

The following internal methods are intended to be purely observational. We called them the fundamental observation methods

  • [[IsExtensible]] ()
  • [[GetPrototypeOf]] ()
  • [[OwnPropertyKeys]] ()
  • [[GetOwnProperty]] (P)

They are used to observe the characters of Objects without modifying them, according to the following table:

Character Internal method
prototype [[GetPrototypeOf]] ()
extensible [[IsExtensible]] ()
exists(P) (all keys) [[OwnPropertyKeys]] ()
configurable(P)
exists(P) (single key)
enumerable(P)
type(P)
writable(P)
value(P)
getter(P)
getter-undefined(P)
setter(P)
setter-undefined(P)		 [[GetOwnProperty]] (P)

Nonquantum objects

We first concentrate on Proxies whose target object can be observed without disturbing the state of the program. Specifically we define a nonquantum object as an Object whose fundemental observation methods satisfy the two following conditions:

  1. Running a fundemental observation method of the object will not observably modify the state of the program.

We exclude from this criterion states depending on the time passing, like the returned value from Date.now(). The returned completion of the method is not part of that criterion.

  1. The results returned by calling successively (i.e., without other operation done inbetween) fundemental observation methods of the object are consistent.

Here, consistency means:

  • the value of a nonabrupt completion returned by the same fundemental observation method will always be the same;
  • if the value of a nonabrupt completion of [[GetOwnProperty]] (P) is not undefined, respectively is undefined, then the value of a nonabrupt completion of [[OwnPropertyKey]] () shall be a List containing P, respectively not containing P, and conversly.

Note that abrupt completions are irrelevant for our purpose.

Every standard built-in object is nonquantum. This is probably true for most, if not all, built-in objects provided by a given ECMAScript implementation such as a web browser.

On the other hand, Proxy objects may be quantum. Although it is probably not a good idea for a non-malicious user to create quantum Proxies, we cannot rely on that.

Integrity checks of trapped Proxy internal methods

When an internal method [[Method]] for which a trap is defined is called on a Proxy, the following steps are taken:

  1. The trap is invoked, and the result is transformed in order to comply with the form of the value that should be returned from the internal method (e.g., for [[OwnPropertyKeys]](), the result is coerced to a List of property keys).
  2. An integrity check is made by comparing that result with results returned by different invocations of the fundemental observation methods on the target object.

If the integrity check is not passed, a TypeError exception is thrown. Also, any abrupt completion terminates the algorithm immediately and is forwarded.

Let IntegrityCheck_Method(arguments, result, target) denotes the abstract operation defining the integrity check associated to [[Method]], where arguments is the List of the arguments with which the [[Method]] was invoked, result is the value that the Proxy wants to return, and target is the target object of the Proxy. When terminating nonabruptly, that operation shall return either true or false, depending on whether the integrity check is passed.

We want to define the various IntegrityCheck_Method algorithms so that the two following conditions are satisfied.

I. IntegrityCheck_Method_(arguments, result, target) shall return true if all observations that would be made on the Proxy by returning result, may be made on target by invoking fundamental observation methods on it.

For example, let P be a Proxy with target object T. Suppose that the trap triggered by calling P.[[PreventExtensions]] () wants to return true. That would trigger the observation “extensible: false” on P. Then, if the same observation can be made on T, e.g. by calling T.[[IsExtensible]]() and getting the value false, the integrity check is passed.

II. If the target of a Proxy is a nonquantum object that observes the Invariants of internal methods, then the Proxy shall observe those invariants.

We restrict ourself to nonquantum target objects, because quantum objects would lead to inextricable complications in edge cases; that issue will be discussed somewhere else (TBW).

Necessary and sufficient conditions for the integrity checks

We want to prove the following:

Given Condition I above, in order to satisfy Condition II, it is necessary and sufficient that the IntegrityCheck_Method(arguments, result, target) abstract operations return false (or an abrupt completion) unless the two following conditions hold:

A. For any observation “character: value” that would be made on the Proxy by returning result, if a lock “@character: valueT” may be put on target (by invoking fundemental observation methods on it), then valueT must be the same as value.

B. Assuming that all the locks that may be put on target (by invoking fundemental observation methods on it) are also put on the Proxy, for any lock “@character: value” that would be put on the Proxy by returning result, if the observation “character: valueT” may be performed on target, then valueT must be the same as value.

proof

See proxies-proof.md.

Algorithm for the Integry Check methods

As an application of the previous section, we can derive algorithms for IntegrityCheck_Method(arguments, result, target):

  1. Determine the characters that would be observed on the Proxy if the method returned result.
  2. For each “character: value” that would be observed:
    1. Observe “character: valueT” on target by invoking the corresponding fundemantal observation method.
    2. If valueT is different from value,
      1. Check whether the lock “@character: valueT” can be put on target, by invoking the fundemantal observation methods corresponding to the characters involved in the chain of locks it depends on. If yes, return false (Condition A).
      2. Check whether the lock “@character: value” could be put on target if it were observed on it, by invoking the fundamental observation methods corresponding to the characters involved in the chain of locks it depends on. If yes, return false (Condition B).
  3. Return true.

Because we have assumed that target is nonquantum, changing the order and the number of calls to its fundemental internal methods is not observable (except when terminating abruptly), so we can avoid to repeat calls of same internal methods with same arguments, and we can reorder them at will (even if, formally, putting a lock on target would need that the methods are called in particular order).

Example: The integrity check for the [[Delete]] method

The following algorithm is a valid implementation for IntegrityCheck_Delete(arguments, result, target).

Steps 4-7 of the algorithm mirror steps 8-11 of the currently specced [[Delete]] internal method of Proxies (where “throw a TypeError exception” is replaced by “return false”, meaning that the integrity check is not passed, and, similarly, “return result” is replaced by “return true”.)

Steps 8-9 correspond to steps 12-13 in the ES spec; historically, they were the missing check that was added in PR 666.

  1. Assert: result is a Boolean.
  2. Assert: arguments is a List containing a unique element, which is a property key.
  3. Let P the unique item of arguments.
  4. If result is false, return true.
  5. Let targetDesc be ? target.[[GetOwnProperty]](P).
  6. If targetDesc is undefined, return true.
  7. If targetDesc.[[Configurable]] is false, return false.
  8. Let extensibleTarget be ? target.[[IsExtensible]]().
  9. If extensibleTarget is false, return false.
  10. Return true.

Let us analyse that algorithm. Steps 1-3 extract the relevant values, namely result and P.

Step 4: if result is false, no observation would be made on the Proxy, so that the integrity check is passed.

Otherwise, result is true, and the following observation would be made on the Proxy:

exists(P): false

Steps 5 and 6 checks whether the same observation “exists(P): false” may be made on the target. If so, the integrity check is passed.

Otherwise, the observation “exists(P): true” is performed on target. At this point, we should check whether this is not contradicted by a potential lock “@exists(P): true” on target (condition A) or “@exists(P): false” on the Proxy (condition B).

In step 7, if targetDesc.[[Configurable]] is false, then the lock “@configurable(P): false” is put on target, from which it follows that the lock “@exists(P): true” is also put on target. By Condition A, the integrity check is not passed.

Steps 8-9: If the observation “extensible: false” is made on target, then we have the lock “@extensible: false” on target. Now, assuming that such a lock is put on the Proxy, observing “exists(P): false” on the Proxy would put the lock “@exists(P): false”. By Condition B, the integrity check is not passed.

Step 10. Otherwise, no potential lock of the character “exists” may be put, either on the Proxy or on target. Therefore the integrity check is passed.