Abstract
We define a small-step operational semantics for the ECMAScript standard language corresponding to JavaScript, as a basis for analyzing security properties of web applications and mashups. The semantics is based on the language standard and a number of experiments with different implementations and browsers. Some basic properties of the semantics are proved, including a soundness theorem and a characterization of the reachable portion of the heap.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
AdSafe: Making JavaScript safe for advertising, http://www.adsafe.org/
Google-Caja, A.: source-to-source translator for securing JavaScript-based Web, http://code.google.com/p/google-caja/
Jscript (Windows Script Technologies), http://msdn2.microsoft.com/en-us/library/hbxc2t98.aspx
Rhino: Javascript for Java, http://www.mozilla.org/rhino/
Abadi, M., Cardelli, L.: A Theory of Objects. Springer, Heidelberg (1996)
Adida, B.: BeamAuth: two-factor Web authentication with a bookmark. In: ACM Computer and Communications Security, pp. 48–57 (2007)
Anderson, C., Giannini, P., Drossopoulou, S.: Towards type inference for JavaScript. In: Black, A.P. (ed.) ECOOP 2005. LNCS, vol. 3586, pp. 428–452. Springer, Heidelberg (2005)
Eich, B.: Javascript at ten years, http://www.mozilla.org/js/language/ICFP-Keynote.ppt
Fisher, K., Honsell, F., Mitchell, J.C.: A lambda calculus of objects and method specialization. Nordic J. Computing (formerly BIT) 1, 3–37 (1994)
Flanagan, D.: JavaScript: The Definitive Guide. O’Reilly, Sebastopol (2006), http://proquest.safaribooksonline.com/0596101996
Herman, D.: Classic JavaScript, http://www.ccs.neu.edu/home/dherman/javascript/
Herman, D., Flanagan, C.: Status report: specifying JavaScript with ML. In: ML 2007: Proc. Workshop on ML, pp. 47–52 (2007)
ECMA International. ECMAScript 4, http://www.ecmascript.org
ECMA International. ECMAScript language specification. stardard ECMA-262, 3rd Edition (1999), http://www.ecma-international.org/publications/ECMA-ST/Ecma-262.pdf
Maffeis, S., Mitchell, J., Taly, A.: Complete ECMA 262-3 operational semantics and long version of present paper. Semantics: http://jssec.net/semantics/ Paper: http://jssec.net/semantics/
Mitchell, J.C.: Toward a typed foundation for method specialization and inheritance. In: POPL 1990, pp. 109–124 (1990)
Mozilla. Spidermonkey (javascript-c) engine, http://www.mozilla.org/js/spidermonkey/
Reis, C., Dunagan, J., Wang, H., Dubrovsky, O., Esmeir, S.: Browsershield: Vulnerability-driven filtering of dynamic HTML. ACM Transactions on the Web 1(3) (2007)
Siek, J., Taha, W.: Gradual typing for objects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 2–27. Springer, Heidelberg (2007)
The FaceBook Team. FBJS, http://wiki.developers.facebook.com/index.php/FBJS
Thiemann, P.: Towards a type system for analyzing JavaScript programs. In: Sagiv, M. (ed.) ESOP 2005, vol. 3444, pp. 408–422. Springer, Heidelberg (2005)
Thiemann, P.: A type safe DOM api. In: Bierman, G., Koch, C. (eds.) DBPL 2005. LNCS, vol. 3774, pp. 169–183. Springer, Heidelberg (2005)
Ungar, D., Smith, R.B.: Self: The power of simplicity. In: Proc. OOPSLA, vol. 22, pp. 227–242 (1987)
Yu, D., Chander, A., Islam, N., Serikov, I.: JavaScript instrumentation for browser security. In: ACM POPL, pp. 237–249 (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Maffeis, S., Mitchell, J.C., Taly, A. (2008). An Operational Semantics for JavaScript. In: Ramalingam, G. (eds) Programming Languages and Systems. APLAS 2008. Lecture Notes in Computer Science, vol 5356. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89330-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-89330-1_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89329-5
Online ISBN: 978-3-540-89330-1
eBook Packages: Computer ScienceComputer Science (R0)