We present a formal policy language (C2L) for stating permissible cloud conﬁgurations. Syntactically, C2L is based upon a spatio-temporal modal logic and provides a concise and clear statement of policy constraints for colocation, hosting, migration, security, andavailability.We illustrate the language witha numberof policyspeciﬁcationexamples and also present an algorithm forverifying whethera cloud conﬁguration along with its history satisﬁesaC2Lpolicy speciﬁcation.We provide complexity analysisof the algorithm, and conclude thatC2Lisa useful and viable formalism for specifying and verifying cloud conﬁguration policies
Jayaraj Poroor and Bharat Jayaraman, “C2L:A Formal Policy Language for Secure Cloud Conﬁgurations”, Procedia Computer Science, vol. 10, pp. 499 - 506, 2012.