I'd just like to express my enthusiasm for taking a formal approach to the kernel language. For everything outside the kernel, defining it by self-hosting, by a meta-circular interpreter (where the interpreter is written only in the kernel subset of the language) or by desugaring is fine. These other techniques may or may not be ideal for expressing the semantics of these non-kernel constructs, but it does ensure that an adversary's code cannot take any action beyond those actions allowed by the kernel language.
All security reasoning is reasoning about limits on what an adversary may do. Thus, all security arguments rest on an induction over all the actions available to the adversary. I think it is no accident that both prominent attempts to formalize the semantics of JS (LambdaJS and < http://www-cs-students.stanford.edu/~ataly/Papers/>) took security as their driving motivation. The related pressing issue is how to tighten up the chapter 16 exemptions. So long as these exemptions are this broad, the induction is broken and all security arguments are unsound. I do not yet have concrete suggestions about how we can tighten these up in ways that JS vendors will agree to. But until we do, we are just as vulnerable to disasters such as having "foo[-6]", for function foo, give foo's caller. By ch16, the major browser that did indeed ship this cannot even be said to have violated the spec. This simple extension allowed by ch16 simultaneously broke all secure JS subsets (Caja, FBJS, WebSandbox, ADsafe, Jacaranda) and all proof about security of any possible subsets. On Wed, May 19, 2010 at 7:03 PM, Joseph Politz <j...@cs.brown.edu> wrote: > > d) If you're serious about suggesting lambda-JS as a basis (or starting > point, anyway) for future editions of ECMA-262, may I make a suggestion? Do > a proof-of-concept by taking the ES5 document and rewriting some of it in > your suggested style. > > If I understand your suggestion right, this is exactly what's going on > here: http://github.com/arjunguha/ML-LambdaJS/blob/master/data/es5-lib.es5 > > In the repo Arjun pointed to > (http://github.com/arjunguha/ML-LambdaJS), there is: > > 1. An updated LambdaJS for ES5, with an interpreter; > 2. An implementation of desugaring (elaboration) from JavaScript > source to ES5-LambdaJS; > 3. A start at writing down built-in objects and functions from the > specification in ES5-LambdaJS. > > The implementation passes around 5-6% of the tests at > http://es5conform.codeplex.com/, predominantly those that test the > object model (e.g. Object.defineProperty, > Object.getOwnPropertyDescriptor). We're on our way to implementing > more of the built-in objects' functionality. > > We are serious about using LambdaJS to model real JavaScript, and > we're quite focused on getting the abstractions right at the levels of > semantics, libraries, and elaboration. I'd love for people to check > out the implementation and give feedback on this and any other issues > as we move forward with it. > > Joe > _______________________________________________ > es-discuss mailing list > es-discuss@mozilla.org > https://mail.mozilla.org/listinfo/es-discuss > -- Cheers, --MarkM
_______________________________________________ es-discuss mailing list es-discuss@mozilla.org https://mail.mozilla.org/listinfo/es-discuss
