Improving reliability in management of cloud computing infrastructure by formal methods

Recent studies identify misconfiguration as the most frequent cause for failures in information systems including cloud computing infrastructure. Therefore, reducing operator error is key to improving the reliability and availability of cloud services. In order to reduce the risk of improper configurations, we propose the following two techniques; (1) automated synthesis of configuration change procedure to avoid improper changes and (2) identification of vulnerabilities (e.g. single point of failures) in system configuration to increase service resilience in the presence of undesirable events such as components failures and improper operations. We devised frameworks that realize these techniques using formal methods and evaluate their effectiveness through case studies. Based on the results of this evaluation, we discuss the benefits and limitations in applying formal methods for cloud system managements.