Towards Verified Cloud Computing Environments
As the usage of the cloud becomes pervasive in the people lives, it is needed to ensure the reliability, safety and security of cloud environments. In this paper, the authors study a usual software stack of a cloud environment from the perspective of formal verification. This software stack ranges from applications to the hypervisor. They argue that most of the layers could be practically formally verified, even if the work to verify all levels is huge. With the development of mobile and internet applications, cloud computing becomes more and more important. More and more of their data is in the cloud. It is thus necessary to have reliable, safe and secure cloud environments.