Research On Formal Design And Analysis For Security System

With the widespread application and rapid development of computer and network technology, information security has increasingly become people's focus point. Following the national requirements of the classified criteria for information security, this paper studies about the theory of developing high level security system, which consists of security policy model design, information flow analysis and etc. In this paper, our research work focus on the following four interrelated aspects.(1) Present a dynamically modified union model combining confidentiality and integrity. To meet the security need of information confidentiality and integrity, we present a dynamic union model based on MLS policy (called DMUM). The two dimensions of secure model are composed of confidentiality and integrity respectively, of which history label is introduced and each subject's access range is adjusted dynamically, thus it leads to a compatible integration of BLP model and Biba model. With the unmanaged dynamic adjustment of secure label, untrusted subjects need not totally dependent on the managed adjustment by trusted subjects, which reduce some unexpected security risks. The formal definition of trusted subject is introduced, and also the paper presents the concept of multilevel trusted subject who has the read and write right among specifying access range. This notion of multilevel trusted subject will give a better support of least privilege principle within the MLS policy framework. Finally, examples are illuminated to show the effectivity and usability of this model.(2) Propose an analysis method of intransitive timed information flow based on process algebra. To reveal timing covert information flow of intransitive secure policy, we analyze the real-time intransitive information flow security properties based on process algebra. To simulate trusted parts of real systems, the concept of trust domain is introduced into Timed Secure Process Algebra (tSPA). Based on tSPA, the intransitive noninterference information flow security model is extended from deterministic systems to timed systems such as real-time systems. We present Intransitive Timed Bisimulation Strong Nondeterministic Noninterference (I_tBSNNI) and Intransitive Timed Bisimulation-based Nondeducibility on Composition (I_tBNDC) based on timed weak bisimulation equivalence. In order to discover the potential secure problem that I_tBNDC cannot discover in dynamic context, the I_tSBSNNI property is proposed, which requires that every reachable state of the system must satisfy I_tBSNNI. Furthermore, we analyze intransitive information flow security properties of a real system in a time setting.(3) Provide a new definition of multilevel security based on the construction of covert channels. Aiming at the main problem that the link between the formal definition of multilevel security and security goal is not always clear, we propose a new definition of multilevel security based on the construction of covert channels. Covert channels are the security problem that the security system must avoid as far as possible; therefore, it will be more helpful to understand the nature of system security from the perspective of implementing a covert channel to define multilevel security. Due to the fact that separability property based on the construction of covert channels is not practical, we introduce the concept of trusted domain to the theoretical framework initiated by the characteristics of transitive and intransitive security policy. Following that two intuitive propositions with the corresponding proof are proposed.On the basis of research results mentioned above, we introduce the design and implemention of a high secure operating system (called Tuling SecOS) base on the trusted computing platform. Firstly we give an overview on the design principles and functional modules of prototype system; then intruduce several key technologies such as mandatory access mechanisms, malicious code protection mechanism, trusted recovery, as well as identification and disposition of covert channels in detail; and at last, the functinal and experimental results show the practicability and feasibility of the prototype system.