Font Size: a A A

Researching Of Implementation Of High Level Secure Trusted Operationg System

Posted on:2009-12-18Degree:DoctorType:Dissertation
Country:ChinaCandidate:J HuFull Text:PDF
GTID:1118360245975368Subject:Signal and Information Processing
Abstract/Summary:PDF Full Text Request
This paper focuses on the implement of the high level secure operatingsystem in the productive information system. Follow the requirements of thefourth level in the GB 17859(Structured protection level),this paper discussesabout the mandatory access control model and the formal describe of the trustedcomputing,provide several creative contents, including a new lattice-based ac-cess control(LBAC) model which protects both confidentiality and integrity,adynamic planar access control(DPAC) model, quantitative Analysis Method toBLP Model, a formal describe method to the trusted computing, and trustedencapsulated method. Based on the Linux operating system, we give a transpar-ent security mechanism, and a structured transform method which separate theLinux kernel to three layers.LBAC model is the most frequently used mandatory access control model.This paper introduces a new lattice-based mandatory access control(LBAC) model,This model take the information in subject/object in the system as a composi-tion of information with di?erent secure labels,add a trusted subject which canexecute information purging operation to support the inverse information ?owin the LBAC model.Based on this model, we integrate the two classical models—BLP model and Biba model,propose a dynamic multi-level planar mandatoryaccess control model(DPAC),and prove its security. DPAC model follows thesecure target of the BLP model in confidentiality protection,follows the securetarget of the Biba model in integrity protection, and provides secure informationexchange channels between different secure levels.BLP model is based on an multi-level information flow policy to implementaccess control. However, the information flow policy of BLP model does notsupport downward information flow from high security level to low security level.This paper proposed an analysis method based on the conditional entropy whichgives quantitative analysis to the security of BLP model. With this analysismethod, we can define the confidentiality of an information system with secure thresholds defined by confidential information and its conditional entropy. Weproved that under certain condition, a downward information ?ow won't let thesystem be not secure.The essence of trusted computing is the behavior expectation,But there isstill no formal trusted computing model based on the behavior expectation. Inthis paper, we give a formal definition of behavior expectation, a discuss theassumption of trust about behavior expectations,propose a formal definition oftrust, give the trust transmission a formal description, and prove two theoremsabout the validity of the set of trusted components.To keep the application be trusted, we propose a new concept: trustedsubset. With selected initial state and carefully limited input,a possibly-buggyapplication can always run in a trusted subset. A trusted encapsulation methodis provided to make an application run in the trusted state even if it is buggy.A productive information system have relatively fixed working procedure.Withthis feature, we let the secure policies mechanism be independent with the ap-plication, provide a transparent implementation method of the reference moni-tor.this paper also provided a channel transform operation method and a channelredirected operation method.We implement security assurance from three layers: structured program-ming, structured data organizing and structured connecting. and discuss abouthow to transform the Linux operating system to achieve the requirement of thestructured protection requirements. our method is based on the trusted comput-ing technology and the layered reformation of the Linux kernel.
Keywords/Search Tags:Structured protection level, secure operating system, mandatoryaccess control model, information ?ow, trusted computing, formal method
PDF Full Text Request
Related items