research-article

Efficient runtime-enforcement techniques for policy weaving

Authors:

Richard Joiner,

Vinod GanapathyAuthors Info & Claims

FSE 2014: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering

Pages 224 - 234

https://doi.org/10.1145/2635868.2635907

Published: 11 November 2014 Publication History

Abstract

Policy weaving is a program-transformation technique that rewrites a program so that it is guaranteed to be safe with respect to a stateful security policy. It utilizes (i) static analysis to identify points in the program at which policy violations might occur, and (ii) runtime checks inserted at such points to monitor policy state and prevent violations from occurring. The promise of policy weaving stems from the possibility of blending the best aspects of static and dynamic analysis components. Therefore, a successful instantiation of policy weaving requires a careful balance and coordination between the two. In this paper, we examine the strategy of using a combination of transactional introspection and statement indirection to implement runtime enforcement in a policy-weaving system. Transactional introspection allows the state resulting from the execution of a statement to be examined and, if the policy would be violated, suppressed. Statement indirection serves as a light-weight runtime analysis that can recognize and instrument dynamically generated code that is not available to the static analysis. These techniques can be implemented via static rewriting so that all possible program executions are protected against policy violations. We describe our implementation of transactional introspection and statement indirection for policy weaving, and report experimental results that show the viability of the approach in the context of real-world JavaScript programs executing in a browser.

References

[1]

C. Allan, P. Avgustinov, A. S. Christensen, L. Hendren, S. Kuzins, O. Lhoták, O. De Moor, D. Sereni, G. Sittampalam, and J. Tibble. Adding trace matching with free variables to AspectJ. In Proceedings of the 20th Annual ACM SIGPLAN Conference on Object Oriented Programming Systems Languages and Applications, pages 345–364. ACM, 2005.

Digital Library

[2]

A. Bauer, J.-C. Küster, and G. Vegliach. Runtime verification meets Android security. In NASA Formal Methods, pages 174–180. Springer, 2012.

Digital Library

[3]

N. Bielova. Survey on JavaScript security policies and their enforcement mechanisms in a web browser. The Journal of Logic and Algebraic Programming, 82(8):243–262, 2013.

[4]

A. Birgnisson, M. Dhawan, U. Erlingsson, V. Ganapathy, and L. Iftode. Enforcing authorization policies using transactional memory introspection. In Proceedings of the 15th ACM Conference on Computer and Communications Security, pages 223–234. ACM, 2008.

Digital Library

[5]

E. Bodden and L. Hendren. The Clara framework for hybrid typestate analysis. International Journal on Software Tools for Technology Transfer, 14(3):307–326, 2012.

Digital Library

[6]

C. Cas¸caval, C. Blundell, M. Michael, H. W. Cain, P. Wu, S. Chiras, and S. Chatterjee. Software transactional memory: Why is it only a research toy? ACM Queue, 6(5), September 2008.

Digital Library

[7]

B. Chess and G. McGraw. Static analysis for security. IEEE Security and Privacy, 2(6):76–79, 2004.

Digital Library

[8]

D. Crockford. ADsafe: Making JavaScript safe for advertising. http: //www.adsafe.org.

[9]

M. Dhawan, C. Shan, and V. Ganapathy. Enhancing JavaScript with transactions. In European Conference on Object Oriented Programming, pages 383–408. Springer, 2012.

Digital Library

[10]

U. Erlingsson. The Inlined Reference Monitor Approach to Security Policy Enforcement. PhD thesis, Computer Sciences Department, Cornell University, January 2004.

Digital Library

[11]

U. Erlingsson and F. B. Schneider. SASI enforcement of security policies: a retrospective. In Proceedings of the 1999 Workshop on New Security Paradigms, pages 87–95. ACM, 2000.

Digital Library

[12]

Y. Falcone, S. Currea, and M. Jaber. Runtime verification and enforcement for Android applications with RV-Droid. In Runtime Verification, pages 88–95. Springer, 2013.

[13]

M. Fredrikson, R. Joiner, S. Jha, T. Reps, P. Porras, H. Sa¨ıdi, and V. Yegneswaran. Efficient runtime policy enforcement using counterexample-guided abstraction refinement. In Computer Aided Verification, pages 548–563. Springer, 2012.

Digital Library

[14]

S. Hussein, P. Meredith, and G. Ros¸u. Security-policy monitoring and enforcement with JavaMOP. In Proceedings of the 7th Workshop on Programming Languages and Analysis for Security, page 3. ACM, 2012.

Digital Library

[15]

S. Jana, D. E. Porter, and V. Shmatikov. TxBox: Building secure, efficient sandboxes with system transactions. In Symposium on Security and Privacy, pages 329–344. IEEE, 2011.

Digital Library

[16]

W. Landi. Undecidability of static analysis. ACM Letters on Programming Languages and Systems, 1(4):323–337, 1992.

Digital Library

[17]

M. E. Locasto, A. Stavrou, G. F. Cretu, and A. D. Keromytis. From STEM to SEAD: Speculative execution for automated defense. In USENIX Annual Technical Conference, pages 219–232, 2007.

Digital Library

[18]

S. Maffeis, J. C. Mitchell, and A. Taly. Isolating JavaScript with filters, rewriting, and wrappers. In European Symposium on Research in Computer Security, pages 505–522. Springer, 2009.

Digital Library

[19]

P. O. Meredith, D. Jin, D. Griffith, F. Chen, and G. Ros¸u. An overview of the MOP runtime verification framework. International Journal on Software Tools for Technology Transfer, 14(3):249–289, 2012.

Digital Library

[20]

L. A. Meyerovich and B. Livshits. ConScript: Specifying and enforcing fine-grained security policies for JavaScript in the browser. In 2010 IEEE Symposium on Security and Privacy, pages 481–496. IEEE, 2010.

Digital Library

[21]

M. S. Miller, M. Samuel, B. Laurie, I. Awad, and M. Stay. Safe active content in sanitized JavaScript. Technical report, Google, Inc, 2008.

[22]

G. Richards, S. Lebresne, B. Burg, and J. Vitek. An analysis of the dynamic behavior of JavaScript programs. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 1–12. ACM, 2010.

Digital Library

[23]

G. Richards, C. Hammer, F. Z. Nardelli, S. Jagannathan, and J. Vitek. Flexible access control for JavaScript. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages and Applications, pages 305–322, 2013.

Digital Library

[24]

F. B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security, 3(1):30–50, 2000.

Digital Library

[25]

M. Song and E. Tilevich. TAE-JS: Automated enhancement of Java-Script programs by leveraging the Java annotations framework. In Proceedings of the 2013 International Conference on Principles and Practices of Programming on the Java Platform: Virtual Machines, Languages, and Tools, pages 13–24. ACM, 2013.

Digital Library

[26]

R. Toledo, P. Leger, and É. Tanter. AspectScript: Expressive aspects for the web. In Proceedings of the 9th International Conference on Aspect-Oriented Software Development, pages 13–24. ACM, 2010.

Digital Library

[27]

H. Washizaki, A. Kubo, T. Mizumachi, K. Eguchi, Y. Fukazawa, N. Yoshioka, H. Kanuka, T. Kodaka, N. Sugimoto, Y. Nagai, et al. AOJS: Aspect-oriented JavaScript programming framework for Web development. In Proceedings of the 8th Workshop on Aspects, Components, and Patterns for Infrastructure Software, pages 31–36. ACM, 2009.

Digital Library

[28]

D. Yu, A. Chander, N. Islam, and I. Serikov. JavaScript instrumentation for browser security. In Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, volume 42, pages 237–249. ACM, 2007.

Digital Library

Cited By

Alpuente MBallis DSapiña J(2020)Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME SystemMathematics in Computer Science10.1007/s11786-020-00455-3Online publication date: 7-Feb-2020
https://doi.org/10.1007/s11786-020-00455-3
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
Van Acker SSabelfeld A(2016)JavaScript SandboxingTutorial Lectures on Foundations of Security Analysis and Design VIII - Volume 980810.1007/978-3-319-43005-8_2(32-86)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1007/978-3-319-43005-8_2

Index Terms

Efficient runtime-enforcement techniques for policy weaving

Recommendations

Efficient runtime policy enforcement using counterexample-guided abstraction refinement
CAV'12: Proceedings of the 24th international conference on Computer Aided Verification

Stateful security policies--which specify restrictions on behavior in terms of temporal safety properties--are a powerful tool for administrators to control the behavior of untrusted programs. However, the runtime overhead required to enforce them on ...
Predictive runtime enforcement

Runtime enforcement (RE) is a technique to ensure that the (untrustworthy) output of a black-box system satisfies some desired properties. In RE, the output of the running system, modeled as a sequence of events, is fed into an enforcer. The enforcer ...
Policy enforcement via program monitoring

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

FSE 2014: Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering

November 2014

856 pages

ISBN:9781450330565

DOI:10.1145/2635868

General Chair:
Shing-Chi Cheung
Hong Kong University of Science and Technology, China
,
Program Chairs:
Alessandro Orso
Georgia Institute of Technology, USA
,
Margaret-Anne Storey
University of Victoria, Canada

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 ACM 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]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 November 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SIGSOFT/FSE'14

Sponsor:

SIGSOFT

SIGSOFT/FSE'14: 22nd ACM SIGSOFT Symposium on the Foundations of Software Engineering

November 16 - 21, 2014

Hong Kong, China

Acceptance Rates

Overall Acceptance Rate 17 of 128 submissions, 13%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
203
Total Downloads

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

Reflects downloads up to 22 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Alpuente MBallis DSapiña J(2020)Efficient Safety Enforcement for Maude Programs via Program Specialization in the ÁTAME SystemMathematics in Computer Science10.1007/s11786-020-00455-3Online publication date: 7-Feb-2020
https://doi.org/10.1007/s11786-020-00455-3
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
Van Acker SSabelfeld A(2016)JavaScript SandboxingTutorial Lectures on Foundations of Security Analysis and Design VIII - Volume 980810.1007/978-3-319-43005-8_2(32-86)Online publication date: 1-Jun-2016
https://dl.acm.org/doi/10.1007/978-3-319-43005-8_2

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.

Figures

Tables

Media

View Table of Conten