On Thu, May 20, 2010 at 8:49 AM, Mark S. Miller <[email protected]> wrote:
> 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. > I had meant to link to < http://www-cs-students.stanford.edu/~ataly/#publications> above. > > 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 <[email protected]> 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 >> [email protected] >> https://mail.mozilla.org/listinfo/es-discuss >> > > > > -- > Cheers, > --MarkM > -- Cheers, --MarkM
_______________________________________________ es-discuss mailing list [email protected] https://mail.mozilla.org/listinfo/es-discuss
