PaperlayerView exact revision on arXiv

Source-linked AI summary

The Essence of JavaScript

Arjun Guha, Claudiu Saftoiu, Shriram Krishnamurthi

arXiv:1510.00925v1cs.PL

TL;DR

The paper addresses the lack of a tractable, demonstrably sound account of JavaScript’s unconventional semantics. It defines λJS as a small-step core calculus, gives a desugaring from JavaScript, validates both against implementations, and applies the semantics to security. The interpreter matches Rhino, V8, and SpiderMonkey on the entire test suite, while the type system proves safety for well-typed λJS expressions.

  • Problem

    Existing JavaScript analyses lack demonstrated soundness, while the standard is informal and a major formal semantics is large and difficult to prove about.

  • Method

    The paper defines λJS, desugars JavaScript into it, mechanizes both, tests their behavior against JavaScript implementations, and builds a type system for safety.

  • Results

    The λJS interpreter produces exactly the same output as Rhino, V8, and SpiderMonkey on the entire test suite, and well-typed λJS expressions reduce only to safe expressions.

  • Takeaways & Limitations

    The calculus supports reasoning about JavaScript semantics and provides a basis for defining and proving a runtime security property.

  • Takeaways & Limitations

    The safe-subset development omits with because its desugaring cannot be verified as a program context, though the machinery could be extended for selected cases.

Abstract

from arXiv · show

We reduce JavaScript to a core calculus structured as a small-step operational semantics. We present several peculiarities of the language and show that our calculus models them. We explicate the desugaring process that turns JavaScript programs into ones in the core. We demonstrate faithfulness to JavaScript using real-world test suites. Finally, we illustrate utility by defining a security property, implementing it as a type system on the core, and extending it to the full language.

1 The Need for Another JavaScript Semantics

The paper introduces λJS as a small, tractable core calculus for JavaScript and explains how full JavaScript desugars into it. It validates the approach against implementations and uses the core to develop a safe subset.

  • λJS captures JavaScript’s essential features while fitting on three pages and supporting proof techniques such as subject reduction.
  • JavaScript programs can be desugared into λJS, including features such as this and with, while keeping the core language simple.
  • The paper mechanizes λJS and desugaring, tests them against the Mozilla JavaScript test suite, and builds a safe JavaScript subset.

2 λJS: A Tractable Semantics for JavaScript

λJS models JavaScript with a Felleisen-Hieb small-step operational semantics and explicit mutable references. Its compact core represents object, field, array, and syntactic-sugar behavior through desugaring.

  • λJS uses a Felleisen-Hieb small-step operational semantics with evaluation contexts.
  • Computed field lookup, missing fields, field creation, deletion, and dotted notation are represented explicitly or treated as syntactic sugar.
  • Because JavaScript arrays are objects, deleting a["3"] leaves length unchanged, makes the missing lookup undefined, and causes the sum to evaluate to NaN.
  • Mutable references model both assignable variables and imperative objects, with JavaScript desugared into explicit allocation and dereferencing.

Assignment and Imperative Objects

λJS models prototype-based lookup and desugars JavaScript’s class-like object syntax into direct prototype manipulation. The treatment preserves prototype lookup behavior while separating it from field updates.

  • 2.2 Prototype-Based Objects: Prototype inheritance affects field lookup, allowing dog to obtain length and width from animal.
  • 2.2 Prototype-Based Objects: A derived object can override an inherited field while continuing to inherit other fields and properties through the prototype chain.
  • 2.2 Prototype-Based Objects: Field lookup falls back to prototypes only when the field is missing from the current object.
  • 2.3 Prototypes: JavaScript’s class-like syntax does not enlarge λJS; it is desugared into direct prototype manipulation.

The this Keyword

JavaScript functions, methods, constructors, and this have semantics determined by application syntax rather than conventional method structure. λJS makes this behavior explicit through desugaring.

  • JavaScript function-valued fields are informally called methods, but they differ from conventional methods because this is implicit.
  • A method call such as obj.setX(10) binds this to obj, whereas extracting the function and calling f(90) binds this to the global object.
  • Desugaring makes this an explicit function argument and supplies its value explicitly at call sites.
  • Functions are desugared into objects with a distinguished code field, and application looks up that field.

Constructors and Prototypes

λJS explains JavaScript’s unusual constructor, prototype, instanceof, and control-flow behavior by desugaring these features into a smaller core calculus.

  • Constructors and Prototypes: Prototype inheritance makes pt.getX() equivalent to pt.__proto__.getX(), returning 50 in the example.
  • Constructors and Prototypes: JavaScript constructors establish prototype relationships through function prototype fields and object __proto__ links.The paper notes that standard JavaScript exposes prototype setup through constructor functions, while new implicitly sets this.__proto__ to the constructor’s prototype.
  • Constructors and Prototypes: instanceof is desugared to a physical-equality test between an object’s __proto__ and the constructor’s prototype.Thus, cat instanceof Cat is expressed as cat.__proto__ === Cat.prototype.
  • Constructors and Prototypes: After Cat.prototype is assigned Dog.prototype, cat instanceof Cat becomes false, while dog instanceof Cat succeeds.The assignment changes Cat.prototype but not cat.__proto__, producing the counterintuitive result described in the paper.
  • Statements and Control Operators: JavaScript control statements are mapped directly to λJS control operators or desugared into them, including while loops and finally-break interactions.
  • Statements and Control Operators: λJS represents return and break with one value-producing break expression, using labels to model transfers to function or loop boundaries.Functions begin with a ret label, return is desugared to break ret, and ordinary break produces undefined.

2.5 Static Scope in JavaScript

JavaScript identifier lookup uses object-based scope chains rather than substitution or environments, while λJS desugars scope manipulation into an explicitly lexical account.

  • Static Scope in JavaScript: JavaScript represents bindings as fields in scope objects linked through a parent-field scope chain.An identifier resolves to the first matching field in the current chain, and new variables are added to its head object.
  • Static Scope in JavaScript: Because with can insert arbitrary objects into the scope chain, JavaScript’s lexical-scoping status is unclear.The paper desugars these scope-manipulation statements into λJS, which is explicitly lexically scoped.

Local Variables

λJS desugars JavaScript’s local, global, and with-related scope behavior into lexical constructs while preserving observable interactions with the global object.

  • Local Variables: Function locals are lifted to the top of the function, so nested references resolve to the local binding even when its declaration appears inside a branch.The initial value of such local variables is undefined, yielding unintuitive behavior for var x = x.
  • Local Variables: A local declaration var x = e is desugared into an assignment x = e plus a top-level let-binding in the enclosing function.
  • Global Variables: Global variables are properties of window, which refers to itself and is directly accessible to programs.Consequently, assignments through x and window.x observe the same global property.
  • Global Variables: λJS preserves lexical scope for locals by abandoning global-variable bindings and desugaring global accesses explicitly through window.This leaves local variables amenable to substitution, α-renaming, and other standard reasoning techniques.
  • With Statements: A with statement conditionally redirects reads and writes to an inserted object, using property checks to choose between object, local, or global access.
  • With Statements: Desugaring nested with statements is non-compositional, although the paper handles nesting by the same general approach.Scope objects avoid the resulting code-size growth, which is linear in the number of nested withs.

2.6 Type Conversions and Primitive Operators

λJS makes JavaScript’s primitive/object distinction, implicit coercions, and operator behavior explicit through a small set of primitive operations and type-directed method calls.

  • Type Conversions: JavaScript distinguishes primitive numbers from number objects: typeof 10 is "number", whereas typeof new Number(7) is "object".
  • Type Conversions: Overriding Number.prototype.valueOf changes x + y to 10 while leaving y.toString() equal to "7".
  • Type Conversions: The + operator can concatenate strings, while * performs numeric coercion: 10 + "7" yields "107" and 10 * "7" yields 70.
  • Primitive Operators: Because x + y follows a 15-step standard algorithm, JavaScript operator semantics are substantially more complicated than their surface syntax suggests.
  • Primitive Operators: λJS models primitive addition, string concatenation, and number/string coercions with a conventional δ function, while making type tests and method calls explicit.The calculus does not enumerate every primitive; δ’s type constrains their behavior, including that primitives cannot manipulate the heap.

3 Soundness and Adequacy of λJS

The paper establishes λJS as a tractable core semantics whose progress properties are formalized and mechanized, then evaluates its adequacy through desugaring and implementation-based tests. The tests cover substantial JavaScript syntax and produce matching outputs across three implementations, while excluding eval and several implementation- or library-specific cases.

  • Soundness: The mechanized semantics exposed errors in interactions among control operators and supported safety testing for λJS.The authors mechanized λJS in PLT Redex and used the resulting semantics to test safety.
  • Soundness: λJS gives a small-step semantics with a progress property for closed, well-formed configurations.A configuration either is a value, evaluates to an error value, or steps to another closed, well-formed configuration.
  • Adequacy: Desugaring is total, and evaluation commutes with desugaring for all JavaScript programs.The paper states both that desugaring is defined for every program and that direct JavaScript evaluation equals λJS evaluation after desugaring.
  • Adequacy: The testing strategy compares direct execution with λJS execution after desugaring across SpiderMonkey, V8, and Rhino.A 100-LOC interpreter runs the desugared program, and its output is checked against all three JavaScript implementations.
  • Adequacy: The evaluation excludes Firefox-specific extensions, eval, and library-detail tests such as regular expressions.These exclusions bound the empirical coverage of the semantics and desugaring strategy.
  • Adequacy: The λJS interpreter produces exactly the same output as Rhino, V8, and SpiderMonkey on the entire tested suite.The tests cover many syntactic forms, including with and switch, and contain about 5,000 LOC after exclusions.

4 Example: Language-Based Sandboxing

The paper develops a type-based safe subset of JavaScript by first securing λJS against XMLHttpRequest access, then extending the reasoning to JavaScript through desugaring. The approach yields safety proofs, catches an unsafe wrapper implementation, and supports compositional reasoning for addition.

  • Security goal: The safe-subset goal is to prevent sandboxed code from communicating with a server, beginning with access to XMLHttpRequest.The construction is intentionally simplified to one property, while noting that other communication mechanisms would require additional restrictions.
  • Types for Securing λJS: The λJS type system initially disallows all field accesses by omitting a typing rule for e1[e2].Its single type, JS, denotes statically safe JavaScript expressions rather than conventional type correctness.
  • Types for Securing λJS: Theorem 1 guarantees that every λJS expression typable under the system evaluates only to safe expressions.The accompanying safety lemma excludes an active field access of the form v["XMLHttpRequest"].
  • Types for Securing λJS: The revised system introduces NotXHR for expressions that provably cannot evaluate to "XMLHttpRequest", allowing guarded lookup while preserving safety.The type system is presented as a means to establish the runtime-safety theorem rather than as the main result itself.
  • Safety for Addition: If both operands are safe, Proposition 1 establishes that their addition is safe because desugaring e1 + e2 is compositional.This compositionality lets results proved for λJS apply to most JavaScript constructs admitted by the safe sub-language.
  • Safe JavaScript sub-language: The safe JavaScript sub-language omits with, while the authors note that additional wrapping or restrictions could support a future safety analysis for it.The developed system also still requires restrictions for properties such as document.write and Element.innerHTML.
  • Safety for lookup: The JavaScript wrapper lookupJS is genuinely unsafe when field.toString() returns "XMLHttpRequest", and the type system catches this implementation bug.The fix is to ensure that field is a primitive string before applying the guarded lookup.

5 Related Work

The paper contrasts λJS’s compact core-plus-desugaring strategy with larger or narrower JavaScript semantics and subset type systems. It combines broad language coverage with conventional proof techniques and test-based adequacy evidence.

  • JavaScript Semantics: JavaScript’s 200-page specification and a 30-page formal semantics motivate a smaller, more tractable account.The earlier semantics follows the standard and inherits its complexities, while λJS and desugaring are described as much smaller and simpler.
  • JavaScript Semantics: λJS models JavaScript’s core, while desugaring translates the remaining language into it.The approach covers all JavaScript except eval and a substantial portion of the standard libraries.
  • JavaScript Semantics: Adequacy is evaluated by running third-party JavaScript tests in λJS and comparing the results with mainstream implementations.This differs from prior work that demonstrated adequacy by following the standard.
  • JavaScript Semantics: λJS uses conventional substitution rather than scope objects, enabling reasoning techniques such as subject reduction.The paper notes that building type systems is unclear for semantics based on scope objects.
  • Types for JavaScript: Other models trade coverage for simplicity: CoreScript omits functions and objects, while cited type systems target subsets that exclude major features or assignment.The cited examples respectively omit prototypes and first-class functions, or prototypes and first-class functions, or assignment.
  • Object Calculi: λJS supports prototype inheritance but omits methods as primitives, instead desugaring method invocation to self-application.It also does not support cloning or direct surface-syntax access to an object’s prototype.

Revision Log

The revision log records corrections to typing and reduction-rule presentation, including a missing rule that could leave a term stuck. It also credits readers who identified these issues.

  • Revision Log: The log records type-setting errors identified on October 3, 2015, July 8, 2010, and April 24, 2010.The entries credit Jean-Baptiste Jeannin, Shriram Krishnamurthi, Rodolfo Toledo, and Jan Vitek.
  • Revision Log: A missing E-Break-Break rule could leave the term (label x (break y (break x 1))) stuck.The rule was added to Figure 8.
  • Revision Log: Err-Break-Reduction was also missing and was added to the supplemental code.
Loading 1510.00925v1…