research-article

Dynamic detection of object capability violations through model checking

Authors:

Cormac FlanaganAuthors Info & Claims

ACM SIGPLAN Notices, Volume 50, Issue 2

Pages 103 - 112

https://doi.org/10.1145/2775052.2661099

Published: 14 October 2014 Publication History

Abstract

In this paper we present a new tool called DOCaT (Dynamic Object Capability Tracer), a model checker for JavaScript that detects capability leaks in an object capability system. DOCaT includes an editor that highlights the sections of code that can be potentially transferred to untrusted third-party code along with a trace showing how the code could be leaked in an actual execution. This code highlighting provides a simple way of visualizing the references untrusted code potentially has access to and helps programmers to discover if their code is leaking more capabilities then required. DOCaT is implemented using a combination of source code rewriting (using Sweet.js, a JavaScript macro system), dynamic behavioral intercession (Proxies, introduced in ES6, the most recent version of JavaScript), and model checking. Together these methods are able to locate common ways for untrusted code to elevate its authority.

References

[1]

Adsafe. http://www.adsafe.org/, accessed June 2014.

[2]

T. H. Austin, T. Disney, and C. Flanagan. Virtual values for language extension. SIGPLAN Not., 46(10):921--938, Oct. 2011.

Digital Library

[3]

A. Barth, U. Berkeley, J. Weinberger, and D. Song. Cross-origin javascript capability leaks: Detection, exploitation, and defense. In Proc. of the 18th USENIX Security Symposium (USENIX Security 2009), 2009.

Digital Library

[4]

A. Bruni, T. Disney, and C. Flanagan. A peer architecture for lightweight symbolic execution. 2013.

[5]

T. V. Cutsem and M. S. Miller. Trustworthy proxies: Virtualizing objects with invariants. In ECOOP 2013, 2013.

Digital Library

[6]

T. V. Cutsem and S. Miller. Proxies: Design principles for robust object-oriented intercession APIs. In Dynamic Languages Symposium, 2010.

Digital Library

[7]

C. Dimoulas, S. D. Moore, A. Askarov, and S. N. Chong. Declarative policies for capability control. Institute of Electrical and Electronics Engineers, 2014.

Digital Library

[8]

S. Drossopoulou and J. Noble. The need for capability policies. In Proceedings of the 15th Workshop on Formal Techniques for Java-like Programs, FTfJP '13, pages 6:1--6:7, New York, NY, USA, 2013. ACM.

Digital Library

[9]

FacebookAPI. https://developers.facebook.com/docs /reference/php/facebook-api/, accessed June 2014.

[10]

M. Flatt and PLT. Reference: Racket. Technical Report PLT-TR2010-1, PLT Inc., June 7, 2010. http://racketlang.org/tr1/.

[11]

Global object poisoning. http://code.google.com/p/google- caja/wiki/GlobalObjectPoisoning, accessed June 2014.

[12]

A. Goldberg and D. Robson. Smalltalk-80: the language and its implementation. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1983.

Digital Library

[13]

Caja. http://code.google.com/p/google-caja/, accessed June 2014.

[14]

V. Kashyap and B. Hardekopf. Security signature inference for javascript-based browser addons. In Proceedings of Annual IEEE/ACM International Symposium on Code Generation and Optimization, CGO '14, pages 219:219--219:229, New York, NY, USA, 2014. ACM.

Digital Library

[15]

S. Maffeis, J. Mitchell, and A. Taly. Object capabilities and isolation of untrusted web applications. Dep. of Computing, Imperial College London, Technical Report DTR10-04, 2010.

[16]

M. S. Miller. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. PhD thesis, Johns Hopkins University, 2006.

Digital Library

[17]

M. S. Miller and T. V. Cutsem. Catch-all proxies. http:// wiki.ecmascript.org/doku.php?id=harmony:proxies.

[18]

M. S. Miller, T. V. Cutsem, and B. Tulloh. Distributed electronic rights in javascript. ESOP'13 22nd European Symposium on Programming, 2013.

Digital Library

[19]

M. S. Miller, E. D. Tribble, and J. Shapiro. Concurrency among strangers: Programming in E as plan coordination. In In Trustworthy Global Computing, International Symposium, TGC 2005, pages 195--229. Springer, 2005.

Digital Library

[20]

M. S. Miller, B. Tulloh, and J. S. Shapiro. The structure of authority: Why security is not a separable concern. In Proceedings of the Second International Conference on Multiparadigm Programming in Mozart/Oz, MOZ'04, pages 2--20, Berlin, Heidelberg, 2005. Springer-Verlag.

Digital Library

[21]

Sweet.js. http://http://sweetjs.org/, accessed June 2014.

[22]

Global scope reachable via this. http://code.google.com/p /google-caja/wiki/GlobalScopeViaThis, accessed June 2014.

[23]

S. Tobin-Hochstadt and D. Van Horn. Higher-order symbolic execution via contracts. SIGPLAN Not., 47(10):537--554, Oct. 2012.

Digital Library

[24]

G. van Rossum and F. Drake. Python Reference Manual. PythonLabs, Virginia, USA, 2001.

Digital Library

Cited By

Drossopoulou SNoble JMackay JEisenbach S(2020)Holistic Specifications for Robust ProgramsFundamental Approaches to Software Engineering10.1007/978-3-030-45234-6_21(420-440)Online publication date: 17-Apr-2020
https://doi.org/10.1007/978-3-030-45234-6_21
Sun KRyu S(2017)Analysis of JavaScript ProgramsACM Computing Surveys10.1145/310674150:4(1-34)Online publication date: 25-Aug-2017
https://dl.acm.org/doi/10.1145/3106741

Index Terms

Dynamic detection of object capability violations through model checking
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
        Software testing and debugging

Recommendations

Dynamic detection of object capability violations through model checking
DLS '14: Proceedings of the 10th ACM Symposium on Dynamic languages

In this paper we present a new tool called DOCaT (Dynamic Object Capability Tracer), a model checker for JavaScript that detects capability leaks in an object capability system. DOCaT includes an editor that highlights the sections of code that can be ...
Isolating JavaScript in dynamic code environments
APLWACA '10: Proceedings of the 2010 Workshop on Analysis and Programming Languages for Web Applications and Cloud Applications

We analyze the source code of four well-known large web applications, namely WordPress, phpBB, phpMyAdmin and Drupal. We want to quantify the level of language intermixing in modern web applications and, if possible, we want to categorize all coding ...
Conditional model checking: a technique to pass information between verifiers
FSE '12: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering

Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 50, Issue 2

DLS '14

February 2015

146 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2775052

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

DLS '14: Proceedings of the 10th ACM Symposium on Dynamic languages
October 2014
160 pages
ISBN:9781450332118
DOI:10.1145/2661088
General Chair:
Andrew Black
Portland State University, USA
,
Program Chair:
Laurence Tratt
King's College London, UK

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 October 2014

Published in SIGPLAN Volume 50, Issue 2

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
147
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Drossopoulou SNoble JMackay JEisenbach S(2020)Holistic Specifications for Robust ProgramsFundamental Approaches to Software Engineering10.1007/978-3-030-45234-6_21(420-440)Online publication date: 17-Apr-2020
https://doi.org/10.1007/978-3-030-45234-6_21
Sun KRyu S(2017)Analysis of JavaScript ProgramsACM Computing Surveys10.1145/310674150:4(1-34)Online publication date: 25-Aug-2017
https://dl.acm.org/doi/10.1145/3106741

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents