Formal Verification of Security Preservation for Migrating Virtual Machines in the Cloud

  • Yosr Jarraya
  • Arash Eghtesadi
  • Mourad Debbabi
  • Ying Zhang
  • Makan Pourzandi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7596)


Firewalls are a prerequisite for securing any communication network. In cloud computing environments, virtual machines are dynamically and frequently migrated across data centers. This frequent modification in the topology requires frequent reconfiguration of security appliances, particularly firewalls. In this paper, we address the issue of security policy preservation in a distributed firewall configuration within a highly dynamic context. Thus, we propose a systematic procedure to verify security compliance of firewall policies after VM migration. First, the distributed firewall configurations in the involved data centers are defined according to the network topology expressed using Cloud Calculus. Then, these configurations are expressed as propositional constraints and used to build a verification model based on the constraint satisfaction problem framework, which allows reasoning on security policy preservation. Finally, we present a case study inspired from Amazon EC2 to show the applicability and usefulness of our approach.


Virtual Machine Data Center Security Policy Security Requirement Constraint Satisfaction Problem 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Malcolm, D.: The Five Pillars of Cloud Computing (2009),; SOA & WOA magazine, Cloud Expo article (last visited, April 2012)
  2. 2.
    Jarraya, Y., Eghtesadi, A., Debbabi, M., Zhang, Y., Pourzandi, M.: Cloud calculus: Security verification in elastic cloud computing platform. In: The Proceeding of the 2012 International Conference on Collaboration Technologies and Systems (CTS), pp. 447–454. IEEE (2012)Google Scholar
  3. 3.
    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded Model Checking. Advances in Computers, vol. 58, pp. 117–148. Elsevier (2003)Google Scholar
  4. 4.
    Jeffrey, A., Samak, T.: Model Checking Firewall Policy Configurations. In: IEEE International Symposium on Policies for Distributed Systems and Networks, POLICY 2009, pp. 60–67 (July 2009)Google Scholar
  5. 5.
    Tamura, N., Banbara, M.: Sugar: A CSP to SAT Translator Based on Order Encoding. In: The Proceedings of the Second International CSP Solver Competition, pp. 65–69 (2008)Google Scholar
  6. 6.
    Yuan, L., Chen, H., Mai, J., Chuah, C.-N., Su, Z., Mohapatra, P.: Fireman: a toolkit for firewall modeling and analysis. In: IEEE Symposium on Security and Privacy, pp. 199–213 (May 2006)Google Scholar
  7. 7.
    Ben Youssef, N., Bouhoula, A.: Automatic Conformance Verification of Distributed Firewalls to Security Requirements. In: 2010 IEEE Second International Conference on Social Computing (SocialCom), pp. 834–841 (August 2010)Google Scholar
  8. 8.
    Gawanmeh, A., Tahar, S.: Modeling and Verification of Firewall Configurations Using Domain Restriction Method. In: 6th International Conference on Internet Technology and Secured Transactions (December 2011)Google Scholar
  9. 9.
    Al-Shaer, E., Marrero, W., El-Atawy, A., ElBadawi, K.: Network Configuration in a Box: Towards End-to-End Verification of Network Reachability and Security. In: 17th IEEE International Conference on Network Protocols, ICNP 2009, pp. 123–132 (October 2009)Google Scholar
  10. 10.
    Acharya, H., Gouda, M.: Firewall Verification and Redundancy Checking are Equivalent. In: 2011 Proceedings IEEE INFOCOM, pp. 2123–2128 (April 2011)Google Scholar
  11. 11.
    Kotenko, I., Polubelova, O.: Verification of Security Policy Filtering Rules by Model Checking. In: The Proceedings of the IEEE 6th International Conference on Intelligent Data Acquisition and Advanced Computing Systems (IDAACS), vol. 2, pp. 706–710 (September 2011)Google Scholar
  12. 12.
    Gouda, M., Liu, A., Jafry, M.: Verification of Distributed Firewalls. In: Global Telecommunications Conference, IEEE GLOBECOM 2008, pp. 1–5. IEEE (December 2008)Google Scholar
  13. 13.
    Yin, Y., Xu, J., Takahashi, N.: Verifying Consistency between Security Policy and Firewall Policy by Using a Constraint Satisfaction Problem Server. In: Zhang, Y. (ed.) Future Wireless Networks and Information Systems. LNEE, vol. 144, pp. 135–146. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  14. 14.
    Cardelli, L., Gordon, A.D.: Mobile Ambients. Theoretical Computer Science 240(1), 177–213 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  15. 15.
    Bugliesi, M., Crafa, S., Merro, M., Sassone, V.: Communication and Mobility Control in Boxed Ambients. Inf. Comput. 202(1), 39–86 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  16. 16.
    Syntax of sugar csp description (2010), (last modified: Tuesday June 29, 13:09:26, 2010 JST)
  17. 17.
    Lu, L., Safavi-Naini, R., Horton, J., Susilo, W.: Comparing and debugging firewall rule tables. IET Information Security 1(4), 143–151 (2007)CrossRefGoogle Scholar
  18. 18., Amazon web services: Overview of security processes (May 2011),
  19. 19.
    van Harmelen, F., Lifschitz, V., Porter, B.: Handbook of Knowledge Representation. Elsevier Science (2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Yosr Jarraya
    • 1
  • Arash Eghtesadi
    • 1
  • Mourad Debbabi
    • 1
  • Ying Zhang
    • 2
  • Makan Pourzandi
    • 3
  1. 1.Computer Security LaboratoryCIISE, Concordia UniversityMontrealCanada
  2. 2.Sillicon Valley LabEricsson ResearchSan JoseUSA
  3. 3.Ericsson Research CanadaMontrealCanada

Personalised recommendations