M. Ali, S. U. Khan, and A. V. Vasilakos. Security in cloud computing: Opportunities and challenges. Inf. Sci., 305:357–383, 2015.

O. Ali, J. Soar, and J. Yong. Challenges and issues that influence cloud computing adoption in local government councils. In 21st IEEE International Conference on Computer Supported Cooperative Work in Design, CSCWD 2017, Wellington,
New Zealand, April 26-28, 2017.

Amazon Web Serives EC2. AWS EC2. Available at: https://aws.amazon.com/ec2/.

Amazon Web Services. Overview of security processes. Available at: https://d1.awsstatic.com/whitepapers/Security/AWS_Security_Whitepaper.pdf.

ARC. Audit Ready Cloud. Available at:http://arc.encs.concordia.ca/.

ArchLinux. PhpVirtualBox. Available at:https://wiki.archlinux.org/
index.php/PhpVirtualBox.

M. Armbrust, A. Fox, R. Griffith, A. D. Joseph, R. H. Katz, A. Konwinski, G. Lee, D. A. Patterson, A. Rabkin, I. Stoica, and M. Zaharia. A view of cloud computing. Commun. ACM, 53(4):50–58, 2010.

BayesFusion. GeNIe and SMILE. Available at: https://www.bayesfusion.com.

S. Bleikertz, C. Vogel, and T. Groß. Cloud radar: near real-time detection of security failures in dynamic virtualized infrastructures. In Annual Computer Security Applications Conference (ACSAC’ 14), 2015.

S. Bleikertz, C. Vogel, T. Groß, and S. M ̈odersheim. Proactive Security Analysis of Changes in Virtualized Infrastructures. In Annual Computer Security Applications Conference (ACSAC’15), 2015.

Y. Cai, F. R. Yu, and S. Bu. Cloud radio access networks (C-RAN) in mobile cloud computing systems. In 2014 Proceedings IEEE INFOCOM Workshops, Toronto, ON, Canada, April 27 - May 2, 2014.

CISCO. VNI Mobile Forecast Highlights Tool. Available at:
https://www.cisco.com/c/m/en_us/solutions/service-provider/
forecast-highlights-mobile.html.


Cloud auditing data federation. PyCADF: A Python-based CADF library, 2015. Available at: http://docs.openstack.org/developer/keystonemiddleware/audit.html.

Cloud Native Computing Foundation. Kubernetes. Available at: https://kubernetes.io/.

Cloud Security Alliance. Cloud control matrix CCM v3.0.1, 2014. Available at:https://cloudsecurityalliance.org/research/ccm/.

Cloud Security Alliance. Security guidance for critical areas of focus in cloud computing v 4.0. Available at:https://cloudsecurityalliance.org/working-groups/security-guidance.

R. Dua, A. R. Raja, and D. Kakadia. Virtualization vs Containerization to Support PaaS. In 2014 IEEE International Conference on Cloud Engineering, Boston, MA, USA, March 11-14, 2014.

ETSI. European Telecommunications Standards Institute. Available at: https://www.etsi.org/.

ETSI. Network Functions Virtualisation. Available at: https://portal.etsi.org/NFV/NFV_White_Paper.pdf.

ETSI. Network Functions Virtualisation (NFV) Release 2; Protocols and Data Models; NFV descriptors based on TOSCA specification. Available at: https://www.etsi.org/deliver/etsi_gs/NFV-SOL/001_099/001/02.05.01_60/gs_NFV-SOL001v020501p.pdf.

ETSI. Network FunctionsVirtualisation (NFV) Release 2;Protocols and Data Models; RESTful protocols specification for the Ve-Vnfm Reference Point. Available at: https://www.etsi.org/deliver/etsi_gs/NFV-SOL/001_099/002/02.03.01_60/gs_NFV-SOL002v020301p.pdf.

S. K. Fayaz, T. Sharma, A. Fogel, R. Mahajan, T. D. Millstein, V. Sekar, and G. Varghese. Efficient Network Reachability Analysis Using a Succinct Control Plane Representation. In 12th USENIX Symposium on Operating Systems Design and Implementation,OSDI 2016, Savannah, GA, USA, November 2-4, 2016.

A. Fogel, S. Fung, L. Pedrosa, M. Walraed-Sullivan, R. Govindan, R. Mahajan, and T. D. Millstein. A General Approach to Network Configuration Analysis. In 12th USENIX Symposium on Networked Systems Design and Implementation, NSDI 15, Oakland, CA, USA, May 4-6, 2015.

A. Gember-Jacobson, R. Viswanathan, A. Akella, and R. Mahajan. Fast Control Plane Analysis Using an Abstract Representation. In Proceedings of the ACM SIGCOMM 2016 Conference, Florianopolis, Brazil, August 22-26, 2016.

Google. Google Cloud Platoform. Available at: https://cloud.google.com/.

ISO Std IEC. ISO 27002:2005. Information Technology-Security Techniques, 2005. Available at: http://www.iso27001security.com/html/27002.html.

ISO Std IEC. ISO 27017. Information technology- Security techniques, 2013. Available at: http://www.iso27001security.com/html/27017.html.

J. Corbet. Trees I:Radix trees. Available at: https://lwn.net/Articles/175432.

JGraphT. A Java library of graph theory data structures and algorithms. Available at: https://jgrapht.org/.

Y. Jiang, E. Z. Zhang, K. Tian, F. Mao, M. Gethers, X. Shen, and Y. Gao. Exploiting statistical correlations for proactive prediction of program behaviors. In Proceedings of the CGO 2010, The 8th International Symposium on Code Generation and Optimization, Toronto, Ontario, Canada, April 24-28, 2010, pages 248–256, 2010.

P. Kazemian, M. Chan, H. Zeng, G. Varghese, N. McKeown, and S. Whyte. Real Time Network Policy Checking Using Header Space Analysis. In Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2013, Lombard, IL, USA, April 2-5, 2013.

P. Kazemian, G. Varghese, and N. McKeown. Header Space Analysis: Static Checking for Networks. In Proceedings of the 9th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2012, San Jose, CA, USA, April 25-27, 2012.

A. Khurshid, X. Zou, W. Zhou, M. Caesar, and P. B. Godfrey. VeriFlow: Verifying Network-Wide Invariants in Real Time. In Proceedings of the 10th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2013, Lombard, IL, USA, April 2-5, 2013.

S. Li, L. D. Xu, and S. Zhao. The internet of things: a survey. Information Systems Frontiers, 2015.

J. Ligatti and S. Reddy. A theory of runtime enforcement, with results. In Computer Security - ESORICS 2010, 15th European Symposium on Research in Computer Security, Athens, Greece, September 20-22, 2010. Proceedings, pages
87–100, 2010.

N. P. Lopes, N. Bjørner, P. Godefroid, K. Jayaraman, and G. Varghese. Checking beliefs in dynamic networks. In Network and Distributed System Security Symposium (NDSS’15), 2015.
[37] Y. Luo, W. Luo, T. Puyang, Q. Shen, A. Ruan, and Z. Wu. Openstack security modules: A least-invasive access control framework for the cloud. In 9th IEEE International Conference on Cloud Computing, CLOUD 2016, San Francisco, CA, USA, June 27 - July 2, 2016, 2016.

T. Madi, S. Majumdar, Y. Wang, Y. Jarraya, M. Pourzandi, and L. Wang. Auditing Security Compliance of the Virtualized Infrastructure in the Cloud: Application to OpenStack. In Conference on Data and Application Security and
Privacy (CODASPY’ 16), 2015.

H. Mai, A. Khurshid, R. Agarwal, M. Caesar, B. Godfrey, and S. T. King. Debugging the data plane with anteater. In Proceedings of the ACM SIGCOMM 2011 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications, Toronto, ON, Canada, August 15-19, 2011, pages 290–301, 2011.

S. Majumdar, Y. Jarraya, T. Madi, A. Alimohammadifar, M. Pourzandi, L. Wang, and M. Debbabi. Proactive Verification of Security Compliance for Clouds Through Pre-computation: Application to OpenStack. In European Symposium on Research in Computer Security (ESORICS ’16), 2015.

S. Majumdar, Y. Jarraya, M. Oqaily, A. Alimohammadifar, M. Pourzandi, L. Wang, and M. Debbabi. LeaPS: Learning-Based Proactive Security Auditing for Clouds. In European Symposium on Research in Computer Security (ESORICS ’17), 2015.

Microsoft. Microsoft Azure, 2010. Available at: https://azure.microsoft.com/en-us/.

OASIS. Open standards, Open source. Available at: https://www.oasis-open.org/.

OASIS. TOSCA Simple Profile for Network Functions Virtualization (NFV). Available at: http://docs.oasis-open.org/tosca/tosca-nfv/v1.0/tosca-nfv-v1.0.html.

OASIS. TOSCA Simple Profile for NetworkFunctions Virtualiza-
tion (NFV) Version 1.0; Committee Specification Draft 04. Available at: http://docs.oasis-open.org/tosca/tosca-nfv/v1.0/csd04/tosca-nfv-v1.0-csd04.pdf.

OpenStack. Barbican. Available at: https://wiki.openstack.org/wiki/Barbican.

OpenStack. Heat : OpenStack Orchestration. Available at: https://wiki.openstack.org/wiki/Heat.

OpenStack. Heat : OpenStack Orchestration. Available at: https://docs.openstack.org/heat/latest/template_guide/hot_guide.html.

OpenStack. Horizon. Available at: https://wiki.openstack.org/wiki/Horizon.

OpenStack. Mistral Overview. Available at: https://docs.openstack.org/mistral/latest/overview.html.

OpenStack. Nova network security group changes are not applied to running instances, 2015. Available at: https://security.openstack.org/ossa/OSSA-2015-021.html.

Openstack. OpenStack : Cloud Operating System. Available at: https://www.openstack.org/.

OpenStack. OpenStack Congress. Available at: https://wiki.openstack.org/wiki/Congress.

Openstack. OpenStack Identity Keystone. Available at: https://wiki.openstack.org/wiki/Keystone.

Openstack. Openstack User Survey, 2017. Available at: https://www.openstack.org/assets/survey/April2017SurveyReport.pdf.

OpenStack. OSSA-2014-008: Routers can be cross plugged by other tenants. Available at: https://security.openstack.org/ossa/OSSA-2014-008.html.

OpenStack. Service Function Chaining Extension for OpenStack Networking. Available at: https://docs.openstack.org/networking-sfc/latest/.

OpenStack. TOSCA-Parser. Available at: https://wiki.openstack.org/wiki/TOSCA-Parser.

Oracle. Java. Available at: https://www.oracle.com/java/.

Oracle. Java: Processes and Threads. Available at: https://docs.oracle.com/javase/tutorial/essential/concurrency/procthread.html.

Oracle. Tacker - OpenStack NFV Orchestration. Available at: https://wiki.openstack.org/wiki/Tacker.

Oracle. VirtualBox. Available at: https://www.virtualbox.org/.

V. D. Piccolo, A. Amamou, K. Haddadou, and G. Pujolle. A Survey of Network Isolation Solutions for Multi-Tenant Data Centers. IEEE Communications Surveys and Tutorials, 2016.
[64] G. D. Plotkin, N. Bjørner, N. P. Lopes, A. Rybalchenko, and G. Varghese. Scaling network verification using symmetry and surgery. In Principles of Programming Languages (POPL’ 16), 2015.

T. Probst, E. Alata, M. Kaˆaniche, and V. Nicomette. An approach for the automated analysis of network access controls in cloud computing infrastructures. In Network and System Security - 8th International Conference, NSS 2014, Xi’an, China, October 15-17, 2014, Proceedings, pages 1–14, 2014.

Sugar. Sugar: a SAT-based Constraint Solver. Available at: http://bach.istc.kobe-u.ac.jp/sugar/.

vmware. vmware cloud. Available at:https://cloud.vmware.com/.

R. J. W. Definitions and Examples. In Introduction to Graph Theory, Second Edition, 1979.

Y. Wang, T. Madi, S. Majumdar, Y. Jarraya, A. Alimohammadifar,
M. Pourzandi, L. Wang, and M. Debbabi. TenantGuard: Scalable Runtime Verification of Cloud-Wide VM-Level Network Isolation. In Network and Distributed System Security Symposium (NDSS’17), 2017.

Wikipedia. Object Copying. Available at: https://en.wikipedia.org/wiki/Object_copying#Deep_copy.

Wikipedia. OSS/BSS. Available at: https://en.wikipedia.org/wiki/OSS/BSS.

H. Yang and S. S. Lam. Real-time verification of network properties using atomic predicates. In 2013 21st IEEE International Conference on Network Protocols, ICNP 2013, G ̈ottingen, Germany, October 7-10, 2013, pages 1–11, 2013.

H. Zeng, S. Zhang, F. Ye, V. Jeyakumar, M. Ju, J. Liu, N. McKeown, and A. Vahdat. Libra: Divide and Conquer to Verify Forwarding Tables in Huge Networks. In Proceedings of the 11th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2014, Seattle, WA, USA, April 2-4, 2014.

Q. Zhang, L. Cheng, and R. Boutaba. Cloud computing: state-of-the-art and research challenges. J. Internet Services and Applications, 2010.