Formal verification of mandatory access control for privacy cloud

According to the multiple security levels requirement of privacy cloud, we firstly propose a mandatory access control model for privacy cloud. Secondly, we illustrate the function of each module in the model. Thirdly, present the implementation model based on the data flow technology corresponding to each module. Fourthly, formally descript our models. Finally, verification results show that our mandatory access control model performs the security policy in the privacy cloud effectively.