Specification Language

Mark S. Miller erights at google.com
Thu May 20 08:51:43 PDT 2010

On Thu, May 20, 2010 at 8:49 AM, Mark S. Miller <erights at google.com> 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 <joe at 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 at mozilla.org
>> https://mail.mozilla.org/listinfo/es-discuss
> --
>     Cheers,
>     --MarkM

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.mozilla.org/pipermail/es-discuss/attachments/20100520/c76cb3a8/attachment-0001.html>

More information about the es-discuss mailing list