Raphaël Khoury
Abstract
Runtime monitoring is an increasingly popular method to ensure the safe execution of untrusted codes. Monitors observe and transform the execution of these codes, responding when needed to correct or prevent a violation of a user-defined security policy. Prior research has shown that the set of properties monitors can enforce correlates with the latitude they are given to transform and alter the target execution. But for enforcement to be meaningful this capacity must be constrained, otherwise the monitor can enforce any property, but not necessarily in a manner that is useful or desirable. However, such constraints have not been significantly addressed in prior work. In this article, we develop a new paradigm of security policy enforcement in which the behavior of the enforcement mechanism is restricted to ensure that valid aspects present in the execution are preserved notwithstanding any transformation it may perform. These restrictions capture the desired behavior of valid executions of the program, and are stated by way of a preorder over sequences. The resulting model is closer than previous ones to what would be expected of a real-life monitor, from which we demand a minimal footprint on both valid and invalid executions. We illustrate this framework with examples of real-life security properties. Since several different enforcement alternatives of the same property are made possible by the flexibility of this type of enforcement, our study also provides metrics that allow the user to compare monitors objectively and choose the best enforcement paradigm for a given situation.
Supplemental Material
Available for Download
The proof is given in an electronic appendix, available online in the ACM Digital Library.
- Alpern, B. and Schneider, F. 1985. Defining liveness. Inform. Process Lett. 21, 4, 181--185.Google Scholar
Cross Ref
- Bauer, L., Ligatti, J., and Walker, D. 2002. More enforceable security policies. In Proceedings of the Workshop on Foundations of Computer Security (FCS).Google Scholar
- Beauquier, D., Cohen, J., and Lanotte, R. 2009. Security policies enforcement using finite edit automata. Electron. Notes Theoret. Comput. Sci. 229, 3, 19--35. Google ScholarDigital Library
- Bielova, N. and Massacci, F. 2011a. Do you really mean what you actually enforced? Intern. J. Inform. Secur. 10, 4, 1--16. Google ScholarDigital Library
- Bielova, N. and Massacci, F. 2011b. Iterative enforcement by suppression: Towards practical enforcement theories. J. Comput. Secur. To appear.Google Scholar
- Bielova, N. and Massacci, F. 2011c. Predictability of enforcement. In Proceedings of the International Symposium on Engineering Secure Software and Systems. 73--86. Google ScholarDigital Library
- Bielova, N., Massacci, F., and Micheletti, A. 2009. Towards practical enforcement theories. In Proceedings of the 14th Nordic Conference on Secure IT Systems (NordSec). 239--254. Google ScholarDigital Library
- Boebert, W. E. and Kain, R. Y. 1985. A practical alternative to hierarchical integrity policies. In Proceedings of the 8th National Computer Security Conference.Google Scholar
- Brewer, D. F. C. and Nash, M. J. 1989. The Chinese Wall security policy. In Proceedings of the IEEE Symposium on Security and Privacy. 206--214.Google Scholar
- Chabot, H., Khoury, R., and Tawbi, N. 2009. Generating in-line monitors for Rabin automata. In Proceedings of the 14th Nordic Conference on Secure IT Systems (NordSec). 287--301. Google ScholarDigital Library
- Chang, E., Manna, Z., and Pnueli, A. 1991. The safety-progress classification. In Logic and Algebra of Specifications, F. Bauer, W. Brauer, and H. Schwichtenberg Eds., Springer-Verlag, 143--202.Google Scholar
- d’Amorim, M. and Roşu, G. 2005. Efficient monitoring of omega-languages. In Proceedings of the 17th International Conference on Computer Aided Verification (CAV). 364--378. Google ScholarDigital Library
- Erlingsson, U. and Schneider, F. 2000. IRM enforcement of java stack inspection. In Proceedings of the IEEE Symposium on Security and Privacy. 246--255. Google ScholarDigital Library
- Falcone, Y., Fernandez, J.-C., and Mounier, L. 2008. Synthesizing enforcement monitors wrt. the safety-progress classification of properties. In Proceedings of the 4th International Conference Information Systems Security (ICISS). 41--55. Google ScholarDigital Library
- Fong, P. 2004. Access control by tracking shallow execution history. In Proceedings of the IEEE Symposium on Security and Privacy.Google ScholarCross Ref
- Hamlen, K. W., Morrisett, G., and Schneider, F. 2006. Computability classes for enforcement mechanisms. ACM Trans. Prog. Lang. Syst. 28, 1, 175--205. Google ScholarDigital Library
- Hamlen, M. S. K. W. 2011. Flexible in-lined reference monitor certification: Challenges and future directions. In Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification (PLPV). 55--60. Google ScholarDigital Library
- Jun, P., Xingyuan, C., Bei, W., Xiangdong, D., and Yongliang, W. 2008. Policy monitoring and a finite state automata model. In Proceedings of the International Conference on Computer Science and Software Engineering (CSSE). 646--649. Google ScholarDigital Library
- Khoury, R. and Tawbi, N. 2010a. Corrective enforcement of security policies. In Proceedings of the 7th International Workshop on Formal Aspects of Security & Trust (FAST). Google ScholarDigital Library
- Khoury, R. and Tawbi, N. 2010b. Using equivalence relations for corrective enforcement of security policies. In Proceedings of the 5th International Conference Mathematical Methods, Models, and Architectures for Computer Networks Security. Google ScholarDigital Library
- Kim, M., Kannan, S., Lee, I., Sokolsky, O., and Viswanathan, M. 2002. Computational analysis of run-time monitoring---fundamentals of java-mac. Electr. Notes Theor. Comput. Sci. 70, 4.Google ScholarCross Ref
- Kupferman, O., Lustig, Y., and Vardi, M. 2006. On locally checkable properties. In Proccedings of the 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning. Google ScholarDigital Library
- Ligatti, J., Bauer, L., and Walker, D. 2004. Edit automata: Enforcement mechanisms for run-time security policies. Intern. J. Inform. Secur. 4, 1--2, 2--16.Google Scholar
- Ligatti, J., Bauer, L., and Walker, D. 2005. Enforcing non-safety security policies with program monitors. In Proceedings of the 10th European Symposium on Research in Computer Security (ESORICS). Google ScholarDigital Library
- Ligatti, J., Bauer, L., and Walker, D. 2009. Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur. 12, 3, 1--41. Google ScholarDigital Library
- Ligatti, J. and Reddy, S. 2010. A theory of runtime enforcement, with results. In Proceedings of the European Symposium on Research in Computer Security (ESORICS). Google ScholarDigital Library
- Mealy, G. H. 1955. A method for synthesizing sequential circuits. Bell System Tech. J. 34, 5, 1045--1079.Google ScholarCross Ref
- Ould-Slimane, H., Mejri, M., and Adi, K. 2009. Using edit automata for rewriting-based security enforcement. In Proceedings of 23rd Annual Conference on Data and Applications Security (IFIP). 175--190. Google ScholarDigital Library
- Schneider, F. 2000. Enforceable security policies. Inf. Syst. Secur. 3, 1, 30--50. Google ScholarDigital Library
- Sobel, A. E. K. and Alves-Foss, J. 1999. A trace-based model of the chinese wall security policy. In Proceedings of the 22nd National Information Systems Security Conference.Google Scholar
- Syropoulos, A. 2001. Mathematics of multisets. In Proceedings of the Workshop on Multiset Processing. 347--358. Google ScholarDigital Library
- Talhi, C., Tawbi, N., and Debbabi, M. 2008. Execution monitoring enforcement under memory-limitations constraints. Inf. Comput. 206, 1, 158--184. Google ScholarDigital Library
- Viswanathan, M. 2000. Foundations for the run-time analysis of software systems. Ph.D. thesis, University of Pennsylvania. Google ScholarDigital Library
- Young, W., Telega, P., and Boebert, W. 1986. A verified labeler for the secure ada target. In Proceedings of the 9th National Computer Security Conference.Google Scholar
- Zhu, G., Tyagi, A., and Roop, P. 2006. Stream automata as run-time monitors for open system security policies. Tech. rep. 06-101, Department of Electrical and Computer Engineering, Iowa State University, Ames, Iowa.Google Scholar
Index Terms
- Corrective Enforcement: A New Paradigm of Security Policy Enforcement by Monitors
Recommendations
Corrective enforcement of security policies
FAST'10: Proceedings of the 7th International conference on Formal aspects of security and trustMonitoring is a powerful security policy enforcement paradigm that allows the execution of a potentially malicious software by observing and transforming it, thus ensuring its compliance with a user-defined security policy. Yet some restrictions must be ...
Using equivalence relations for corrective enforcement of security policies
MMM-ACNS'10: Proceedings of the 5th international conference on Mathematical methods, models and architectures for computer network securityIn this paper, we present a new framework of runtime security policy enforcement. Building on previous studies, we examine the enforcement power of monitors able to transform their target's execution, rather than simply accepting it if it is valid, or ...
Extending the enforcement power of truncation monitors using static analysis
Runtime monitors are a widely used approach to enforcing security policies. Truncation monitors are based on the idea of truncating an execution before a violation occurs. Thus, the range of security policies they can enforce is limited to safety ...
Comments