Cloud computing has become a prominent technology with the potential for tremendously positive effects on the future of computer networks and services. However, as the resources are shared in cloud environments, cloud security is a major concern. As such, for cloud computing to reach its full potential, better security solutions are required (particularly solutions to security issues that are unique and fundamental to the cloud environment). In this dissertation, we present a formal method-based approach to making clouds environments more secure and manageable. The scope of our work addresses one of the three major types of cloud environments, Infrastructure as a Service (IaaS) cloud environments, and is grounded in a common set of formal methods (i.e., binary decision diagrams, constraint satisfaction problems, and computational tree logic). First, we present a formal method-based, semi-automated framework for access control list (ACL) generation to improve IaaS security manageability. Second, we present a formal method-based cloud resource allocation framework that factors in customer security requirements, specifically reachability and ACLs, at the time of virtual machine provisioning. Third, we present a formal method-based framework for virtual machine migration planning, in which a safe migration order is determined to ensure the preservation of security requirement during migration. Fourth, we present a formal method-based framework for virtual machine post migration reconfiguration and verification. Fifth, we provide a formal method-based framework that detects and resolves policy misconfigurations in Software Defined Networks (SDNs), an important, emerging approach to managing cloud computing infrastructures. These frameworks use a common formal method-based approach and were evaluated in simulated environments for their effect on IaaS security. The results demonstrate the efficiency and usability of these frameworks to improve IaaS security and suggest promising further areas of research.
