Abstract
This paper introduces a formal program-rewriting approach that can automatically enforce security policies on non trusted programs. For a program P and a security policy \(\varPhi \), we generate another program \(P'\) that respects the security policy and behaves like P except that it stops any execution path whenever the enforced security policy is about to be violated. The presented approach uses the \(\mathcal {E}BPA_{0,1}^*\) algebra which is a variant of BPA (Basic Process Algebra) extended with variables, environments and conditions. The problem of computing the expected enforced program \(P'\) will turn to resolve a linear system which we already know how to extract the solution by a polynomial algorithm.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on FOCS, pp. 46–57 (1977)
Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30–50 (2000)
Alpern, B., Schneider, F.: Recognizing saftey, and liveness. Distrib. Comput. 2(3), 117–126 (1987)
Clarkson, M.R., Schneider, F.: Hyperproperties. In: J. Comput. Secur. 7thInternational Workshop on Issues in the Theory of Security (WITS 2007) 18(6). IOS Press, Amsterdam (2010)
Walker, D.: A type system for expressive security policies. In: POPL 2000: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 254–267. ACM (2000)
Khoury, R., Tawbi, N.: Corrective enforcement of security policies. In: Degano, P., Etalle, S., Guttman, J. (eds.) Formal Aspects in Security and Trust. LNCS, vol. 6561, pp. 176–190. Springer, Heidelberg (2010)
Clarke, E.M., Schlingloff, B.H.: Model checking. In: Handbook of Automated Reasoning, pp. 1635–1790 (2001)
Necula, G.: Proof-carring code. In: Proceedings of the POPL 1997, pp. 106–119. ACM Press (1997)
Deutsch, P., Grant, C.: A flexible measurement tool for software systems. In: 71 Proceedings of the IFIP Congress Information Processing, pp. 320–326. Yugoslavia (1971)
Langar, M., Mejri, M., Adi, K.: Formal enforcement of security policies on concurrent systems. J. Symb. Comput. 46(9), 997–1016 (2011)
Sui, G., Mejri, M., Ben Sta, H.: FASER (formal, automatic security enforcement by rewriting): an algebraic approach. In: Computational Intelligence for Security and Defence Applications (CISDA) (2012)
Mejri, M., Fujita, H.: Enforcing security policies using algebraic approach. SoMeT 182, 84–98 (2008)
Pardo, A.: Many-sorted algebras. grupo de métodos formales instituto de computación facultad de ingenierá
Bergstra, J.A., Klop, J.W.: The algebra of recursively defined processes and the algebra of regular processes. In: Paredaens, J. (ed.) Automata, Languages and Programming. LNCS, vol. 172, pp. 82–94. Springer, Heidelberg (1984)
https://drive.google.com/file/d/0B8V7WaS6PT37U29XLThkLXhVWlk/view?usp=sharing
FASER website. http://web\_security.fsg.ulaval.ca:8080/enf/enforce-cbpa-program.jsp
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Sui, G., Mejri, M. (2016). Security Enforcement by Rewriting: An Algebraic Approach. In: Garcia-Alfaro, J., Kranakis, E., Bonfante, G. (eds) Foundations and Practice of Security. FPS 2015. Lecture Notes in Computer Science(), vol 9482. Springer, Cham. https://doi.org/10.1007/978-3-319-30303-1_22
Download citation
DOI: https://doi.org/10.1007/978-3-319-30303-1_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-30302-4
Online ISBN: 978-3-319-30303-1
eBook Packages: Computer ScienceComputer Science (R0)