Research On Information Flow Security Of Cloud Computing Based On Noninterference Models

Cloud computing provides services to users through Internet. This open mode not only facilitates the access by users, but also brings potential security risks. In cloud computing, the risk of data leakage exists between users and virtual machines. Whether direct or indirect data leakage, it can be regarded as illegal information flow. Methods, such as access control models can control the information flow, but not the covert information flow. Therefore, it needs to use the noninterference models to detect the existence of illegal information flow in cloud computing architecture. Typical noninterference models are not suitable to verificate information flow in cloud computing architecture.Cloud computing architecture design is a process from simple to complex. Simple cloud computing architecture is to facilitate the formal verification of its security attributes. Complex cloud computing architecture is to facilitate implementation. The complex cloud computing architecture is refined by the simple cloud computing architecture. In the cloud computing architecture, security is one of the bottlenecks restricting the development of cloud computing. When design the cloud computing architecture, it is necessary to consider the security attributes and maintain the security attributes of the architecture in the refinement process of the cloud computing architecture. Whether security attributes of cloud computing architecture are maintained is not considered by the traditional refinement method.To solve these problems, we study the features of noninterference models and the relationship between them. Based on this, we propose the method to keep the security attributes in architecture refinement and information flow security models for cloud computing. The main contents and innovations of this paper are as follows:(1) Research on transitive noninterference model and intransitive noninterference model. Propose properties of these models and make theoretical derivation of properties. Transitive noninterference model is P-secure model. Intransitive noninterference models include IP-secure model, TA-secure model and so on. They both have similar attributes. P-secure model, IP-secure model and TA-secure model have the smallest action sequences property, while the smallest action sequences of P-secure model and IP-secure model is unique, the smalles action sequences are not unique for TA-secure model. They also have different properties. P-secure model and IP-secure model is idempotent, that is sequence of actions after the first treatment is same with the results of the function after function repeatedly treated. TA-secure model does not have this property. By an extraction algorithm of this paper, which is to extract an action subsequence from the processing result of the action sequence by the model function, TA-secure model also has the attribute which is similar to idempotent. In this paper, the properties of these noninterference models are analyzed comprehensively and verified theoretically.(2) Research on the relationship between the two intransitive noninterference models, IP-secure and TA-secure. Propose condition that can transfer the IP-secure model to TA-secure model. Prove that the condition is sound and complete for the relationship. IP-secure model and TA-scure model are two important noninterference models of intransitive policies. TA-secue model hides more information than IP-secure model. Generally, if the system is TA-secure, then the system is IP-secure. On the contrary, the system is IP-secure, but wether the system is TA-secure or not is uncerten. This paper analyzes the inherent relationship between the two models. When the system is IP-secure, we propose restriction conditions to limit the system, and then the system is TA-secure. Theoretically verify the soundness and completeness of the condition.(3) Research on noninterference property in architecture refinement. Propose a method to refine an architecture which can keep the noninterference property. Noninterference property is a kind of security property. Traditional, architecture refinement methods don’t consider how to keep security attributes. In this paper, we propose an architecture refinement method, including a refining function and a number of restriction rules. The refining function refines the security domain of the architecture. A number of restriction rules limit the flow of information between the security domains. When the original architecture meets the noninterference property, use the method to refine the architecture, then refined architecture also meets noninterference property. Theoretically prove soundness of the method.(4) Research on the application of noninterference in cloud application computing. Propose noninterference model for cloud architecture. Cloud architecture is a multi-user architecture which concurrent access and sequential access is coexistence. Users may concurrently access cloud services, also may access cloud computing services sequentially. The traditional model of noninterference can not process information flow caused by concurrent access in cloud infrastructure. In this paper, we propose a noninterference model for secure cloud architecture for concurrent access. When concurrent access actions execute in the cloud architecture, security domains and security domains do not affect each other, that there is no information flow between security domains. Based on this, further propose noninterference for cloud architecture which concurrent access and sequential access coexist. When the sequential actions execute, the information flow between security domains can flow in accordance with established rules. When concurrent access actions execute, there should not have the information flow between security domains.In summary, the targets of this paper are to solve the information flow security of cloud computing and keep noninterference properties in architecture refinement. Then analyze the fetures of noninterference model and the relationship between them. Give the transition condition from one model to another. Based on this, we study the problem of keeping security attributes in architecture refinement. Function and refinement rules are proposed to solve the problem. Finally, we propose information flow security models for cloud computing and solve the covert information flow issues of cloud computing architecture.