On Wed, Sep 25, 2013 at 5:32 PM, Mark S. Miller <[email protected]> wrote:
> Hi François, your goals here have a tremendous overlap with SES. In what > ways is SES not satisfactory for these purposes? > > The best short-but-accurate summary of SES, sufficient for this question, > is <http://research.google.com/pubs/pub40673.html> section 2.3. > I just looked and this section is indeed short -- shorter than your question ;). Here it is: 2.3 SES: Securing JavaScript In a memory-safe object language with unforgeable object references (protected pointers) and encapsulated objects, an object reference grants the right to invoke the public interface of the object it designates. A message sent on a reference both exercises this right and grants to the receiving object the right to invoke the passed arguments. In an object-capability (ocap) language [7], an object can cause effects on the world outside itself only by using the references it holds. Some objects are transitively immutable or powerless [8], while others might cause effects. An object must not be given any powerful references by default; any references it has implicit access to, such as language-provided global variables, must be powerless. Under these rules, granted references are the sole representation of permission. Secure EcmaScript (SES) is an ocap subset of ES5. SES is lexically scoped, its functions are encapsulated, and only the global variables on its whitelist (including all globals defined by ES5) are accessible. Those globals are unassignable, and all objects transitively reachable from them are immutable, rendering all implicit access powerless. SES supports defensive consistency [7]. An object is defensively consistent when it can defend its own invariants and provide correct service to its well behaved clients, despite arbitrary or malicious misbehavior by its other clients. SES has a formal semantics supporting automated verification of some security properties of SES code [9]. The code in this paper uses the following functions from the SES library: - def(obj) def ines a def ensible object. To support defensive consistency, the def function makes the properties of its argument read-only, likewise for all objects transitively reachable from there by reading properties. As a result, this subgraph of objects is effectively tamper proof. A tamper-proof record of encapsulated functions hiding lexical variables is a defensible object. In SES, if makePoint called def on the points it returns by saying “return def({...})”, it would make defensively consistent points. - confine(exprSrc, endowments) enables safe mobile code. The confine function takes the source code string for a SES expression and an endowments record. It evaluates the expression in a new global environment consisting of the SES whitelisted (powerless) global variables and the properties of this endowments record. For example, confine(‘x + y’, {x: 3, y: 6}) returns 9. - Nat(allegedNumber) tests whether allegedNumber is indeed a primitive number, and whether it is a non-negative integer (a natural number) within the contiguous range of exactly representable integers in JavaScript. If so, it returns allegedNumber. Otherwise it throws an error. - var m = WeakMap() assigns to m a new empty weak map. WeakMaps are an ES6 extension (emulated by SES on ES5 browsers) supporting rights amplification [10]. Ignoring space usage, m is simply an object-identity-keyed table. m.set(obj,val) associates obj’s identity as key with val as value, so m.get(obj) returns val and m.delete(obj) removes this entry. These methods use only obj’s identity without interacting with obj. -- Cheers, --MarkM
_______________________________________________ es-discuss mailing list [email protected] https://mail.mozilla.org/listinfo/es-discuss
