Efficient runtime-enforcement techniques for policy weaving

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.
2. A. Bauer, J.-C. Küster, and G. Vegliach. Runtime verification meets Android security. In NASA Formal Methods, pages 174–180. Springer, 2012.
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.
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.
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.
7. B. Chess and G. McGraw. Static analysis for security. IEEE Security and Privacy, 2(6):76–79, 2004.
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.
10. U. Erlingsson. The Inlined Reference Monitor Approach to Security Policy Enforcement. PhD thesis, Computer Sciences Department, Cornell University, January 2004.
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.
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.
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.
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.
16. W. Landi. Undecidability of static analysis. ACM Letters on Programming Languages and Systems, 1(4):323–337, 1992.
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.
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.
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.
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.
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.
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.
24. F. B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security, 3(1):30–50, 2000.
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.
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.
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.
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.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification