Cloud Computing has known in the past few years a fast development, leading to a spike in the number of companies competing on providing the best Cloud services. This makes it harder for potential Cloud customers to chose the adequate provider. Despite its wide adoption, many are still hesitant due to the security issues Cloud Computing poses. In this paper, we propose a brokerage solution that formalizes security properties under the form of inter-VM relations, and gives the possibility of setting these security requirements to its customers from the first steps. This solution uses formal methods and the finite model finder KodKod to verify the consistency of the customer's requirements, and to find a placement for his deployment model.