Abstract
We present a framework that automatically produces suggestions to resolve type errors in security-typed programs, enabling legacy code to be retrofit with comprehensive security policy mediation. Resolving such type errors requires selecting a placement of mediation statements that implement runtime security decisions, such as declassifiers and authorization checks. Manually placing mediation statements in legacy code can be difficult, as there may be several, interacting type errors. In this paper, we solve this problem by constructing a graph that has the property that a vertex cut is equivalent to the points at which mediation statements can be inserted to allow the program to satisfy the type system. We build a framework that produces suggestions that are minimum cuts of this graph, and the framework can be customized to find suggestions that satisfy programmer requirements. Our framework implementation for Java programs computes suggestions for 20,000 line programs in less than 100 seconds, reduces the number of locations a programmer must consider by 90%, and selects suggestions similar to those proposed by expert programmers 80% of the time.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bar-Yehuda, R., Even, S.: A linear-time approximation algorithm for the weighted vertex cover problem. Journal of Algorithms 2(2), 198–203 (1981)
Clarkson, M.R., Chong, S., Myers, A.C.: Civitas: Toward a secure voting system. In: Proceedings of the 2008 IEEE Symposium on Security and Privacy, May 2008, pp. 354–368 (2008)
Criswell, J., Lenharth, A., Dhurjati, D., Adve, V.: Secure virtual architecture: a safe execution environment for commodity operating systems. SIGOPS Oper. Syst. Rev. 41(6), 351–366 (2007)
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems 13(4), 451–490 (1991)
Deng, Z., Smith, G.: Type inference and informative error reporting for secure information flow. In: ACM-SE 44: Proceedings of the 44th annual Southeast regional conference, pp. 543–548. ACM, New York (2006)
Fahndrich, M., Foster, J.S., Su, Z., Aiken, A.: Partial online cycle elimination in inclusion constraint graphs. In: Proceedings of PLDI 1998, pp. 85–96 (1998)
Flanagan, C., Flatt, M., Krishnamurthi, S., Weirich, S., Felleisen, M.: Catching bugs in the web of program invariants. SIGPLAN Not. 31(5), 23–32 (1996)
Fraser, T., Petroni Jr., N.L., Arbaugh, W.A.: Applying flow-sensitive CQUAL to verify minix authorization check placement. In: Proceedings of PLAS 2006, pp. 3–6. ACM, New York (2006)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings of the 1982 IEEE Symposium on Security and Privacy, April 1982, pp. 11–20 (1982)
Halperin, E.: Improved approximation algorithms for the vertex cover problem in graphs and hypergraphs. In: SODA 2000: Proceedings of the 11th Annual ACM-SIAM Symposium on Discrete Algorithms, pp. 329–337. Society for Industrial and Applied Mathematics (2000)
Heintze, N., Tardieu, O.: Ultra-fast aliasing analysis using CLA: A million lines of C code in a second. In: Proceedings of PLDI 2001, June 2001, pp. 254–263 (2001)
Hicks, B., Ahmadizadeh, K., McDaniel, P.: From languages to systems: Understanding practical application development in security-typed languages. In: ACSAC 2006: Proceedings of the 22nd Annual Computer Security Applications Conference, pp. 153–164. IEEE Computer Society, Los Alamitos (2006)
Hicks, B., Rueda, S., Jaeger, T., McDaniel, P.: From trusted to secure: Building and executing applications that enforce system security. In: Proceedings of the USENIX Annual Technical Conference, June 2007, pp. 1–14 (2007)
Khachiyan, L., Boros, E., Elbassioni, K., Gurvich, V., Makino, K.: Enumerating disjunctions and conjunctions of paths and cuts in reliability theory. Discrete Appl. Math. 155(2), 137–149 (2007)
King, D., Jaeger, T., Jha, S., Seshia, S.A.: Effective blame for information-flow violations. In: SIGSOFT 2008/FSE-16: Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 250–260. ACM, New York (2008)
King, D., Jha, S., Muthukumaran, D., Jaeger, T., Jha, S., Seshia, S.: Automating Security Mediation Placement. Tech. Rep. NAS-TR-0123-2010, Network and Security Research Center, Department of Computer Science and Engineering, Pennsylvania State University, University Park, PA, USA (January 2010)
McCamant, S., Ernst, M.D.: Quantitative information flow as network flow capacity. In: Proceedings of PLDI 2008, pp. 193–205. ACM, New York (2008)
Muchnick, S.S.: Advanced Compiler Design and Implementation. Morgan Kaufmann, San Francisco (1997)
Myers, A., Liskov, B.: Complete, safe information flow with decentralized labels. In: Proceedings of the IEEE Symposium on Security & Privacy, May 1998, pp. 186–197 (1998)
Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Proceedings of POPL 1999, January 1999, pp. 228–241 (1999)
Necula, G.C., Condit, J., Harren, M., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy software. ACM Transactions on Programming Languages and Systems 27(3), 477–526 (2005)
Pottier, F., Simonet, V.: Information flow inference for ML. In: Proceedings of POPL 2002, pp. 319–330. ACM Press, New York (2002)
Rehof, J., Mogensen, T.A.: Tractable constraints in finite semilattices. Science of Computer Programming 35(2-3), 191–221 (1999)
Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: CSFW 2005: Proceedings of the 18th IEEE Workshop on Computer Security Foundations, pp. 255–269. IEEE Computer Society, Los Alamitos (2005)
Shapiro, M., Horwitz, S.: Fast and accurate flow-insensitive points-to analysis. In: Proceedings of POPL 1997, pp. 1–14. ACM, New York (1997)
Tip, F., Dinesh, T.B.: A slicing-based approach for locating type errors. ACM Trans. Softw. Eng. Methodol. 10(1), 5–55 (2001)
Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security 4(3), 167–187 (1996)
Walsh, E.: Integrating X.Org with Security-Enhanced Linux. In: Proceedings of the Third Annual Security Enhanced Linux Symposium, March 2007, pp. 33–40 (2007)
Wheeler, D.A.: Software/dbus, http://www.freedesktop.org/wiki/Software/dbus
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)
Wright, C., Cowan, C., Morris, J., Smalley, S., Kroah-Hartman, G.: Linux security modules: General security support for the linux kernel. In: Proceedings of the 11th USENIX Security Symposium, August 2002, pp. 17–31 (2002)
Zhang, X., Edwards, A., Jaeger, T.: Using CQUAL for static analysis of authorization hook placement. In: Proceedings of the 11th USENIX Security Symposium, August 2002, pp. 33–48 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
King, D., Jha, S., Muthukumaran, D., Jaeger, T., Jha, S., Seshia, S.A. (2010). Automating Security Mediation Placement. In: Gordon, A.D. (eds) Programming Languages and Systems. ESOP 2010. Lecture Notes in Computer Science, vol 6012. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11957-6_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-11957-6_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11956-9
Online ISBN: 978-3-642-11957-6
eBook Packages: Computer ScienceComputer Science (R0)