Security Enforcement by Rewriting: An Algebraic Approach

  • Guangye SuiEmail author
  • Mohamed Mejri
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9482)


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.


Program rewriting Process algebra Security policy Security enforcement 


  1. 1.
    Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on FOCS, pp. 46–57 (1977)Google Scholar
  2. 2.
    Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30–50 (2000)CrossRefGoogle Scholar
  3. 3.
    Alpern, B., Schneider, F.: Recognizing saftey, and liveness. Distrib. Comput. 2(3), 117–126 (1987)CrossRefzbMATHGoogle Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    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)CrossRefGoogle Scholar
  7. 7.
    Clarke, E.M., Schlingloff, B.H.: Model checking. In: Handbook of Automated Reasoning, pp. 1635–1790 (2001)Google Scholar
  8. 8.
    Necula, G.: Proof-carring code. In: Proceedings of the POPL 1997, pp. 106–119. ACM Press (1997)Google Scholar
  9. 9.
    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)Google Scholar
  10. 10.
    Langar, M., Mejri, M., Adi, K.: Formal enforcement of security policies on concurrent systems. J. Symb. Comput. 46(9), 997–1016 (2011)CrossRefMathSciNetzbMATHGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Mejri, M., Fujita, H.: Enforcing security policies using algebraic approach. SoMeT 182, 84–98 (2008)Google Scholar
  13. 13.
    Pardo, A.: Many-sorted algebras. grupo de métodos formales instituto de computación facultad de ingenieráGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
  16. 16.
    FASER website. http://web\ Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Departement of Computer ScienceLaval UniversityQuebecCanada

Personalised recommendations