Research On Trusted Process Mechanism And Related Problems

With an experiment of implementing a practical secure operating system SECIMOS, research on the trusted process mechanism and some relative problems in secure operating system is discussed in this dissertation. As results, four principal archivements have been obtained. First, based on the thorough research on the fundamental properties of trusted processes, a new generic definition of trusted process is proposed from the aspect of trustworthiness. The definition overcomes the one-sidedness of some old definitions; provide a firm theoretical foundation for implementing a comparative complete trusted process mechanism. Under the guidance of this definition, a prototype of trusted process mechanism is implemented in SECIMOS; the trustworthiness of trusted process is assured in many ways. As a result, a comparative perfect solution is offered. Second, In order to provide effective support to the principle of least privilege, considering the limitation of traditional privilege mechanisms, a new privilege control model called State-Based Privilege Control (SBPC) is proposed and a prototype system for SBPC called Controlled Privilege Framework (CPF) is implemented in SECIMOS. SBPC concentrates on program logic, introduces the notation of privilege state for privilege control; constructs the explicit relationship between privileges and their parameters; and improves the privilege computing mechanism of privileged process. With the implementation of CPF, fine-grain and automatic privilege control can be transparently exercised to traditional applications, threats of malicious intrusion to a system can be reduced greatly, and support to the principle of least privilege can therefore be achieved effectively. Third, the ideas of lightweight formal methods are extended and applied to modeling the formal security policy model (FSPM) of secure operating system. A lightweight Z-based specification and verification method for FSPM called LFSV (Lightweight Formal Specification and Verification) is proposed. In this method, the formal specification and verification are performed with succinct and unitary formal techniques. As a result, the complexity of FSPM and difficulties of modeling are reduced greatly. LFSV has been employed in modeling FSPM of SECIMOS. Using it, a pricise and easy-understand formal policy model is providedfor the access control mechanisms enforced by SECIMOS; and some inconsistent implementation that violate the requirements of model are found, especially, a serious error of orginal Linux privilege mechanism in the newest release is detected by consistence proving. Consequently, the correct enforcement of security control is ensured, and the security of basic platform (Linux) is improved. The experiment results show that this method is an effective and easy-master FSPM specifying and verifying method. Fourth, an existing classic and generally accepted method of enforcing BLP model in Role-based Access Control (RBAC) model presented by Sandhu et al. is researched and analyzed. Some errors of it are revealed and proved; and some shortages are pointed out, especially it can't accommodate the notation of trusted subject necessary for BLP model. An improved method called ISandhu method is presented. Based on this method, the mistakes of the original method are revised; the support to the notation of trusted subject is provided and the scope of enforcement objects is extended to meet the practical requirements. As results, the exact enforcement of mandatory access control in RBAC is guaranteed and the theoretical foundation for adopting MAC in a large amount of commercial systems with small cost is offered. In summary, the principal achievements of this dissertation are helpful to the research and development of a consummate trusted process mechanism, and to the construction of high-trust secure operating system.