This paper interprets the essence of XEN and hardware virtualization technology, which make the virtual machine technology become the focus of people＇s attention again because of its impressive performance. The secur...This paper interprets the essence of XEN and hardware virtualization technology, which make the virtual machine technology become the focus of people＇s attention again because of its impressive performance. The security challenges of XEN are mainly researched from the pointes of view： security bottleneck, security isolation and share, life-cycle, digital copyright protection, trusted virtual machine and managements, etc. These security problems significantly affect the security of the virtual machine system based on XEN. At the last, these security measures are put forward, which will be a useful instruction on enhancing XEN security in the future.展开更多
With development of electronic com-merce,non-repudiation protocol as the basal component of non-repudiation service has done more and more important functions.Comparing with lots of work on two-party non-repudiation,t...With development of electronic com-merce,non-repudiation protocol as the basal component of non-repudiation service has done more and more important functions.Comparing with lots of work on two-party non-repudiation,there are less work on multi-party non-repudiation protocol.Multi-party protocol is more complex and facing more challenge of collusion attack.In this paper we give a kind of multi-party non-repudiation protocol based on off-line TTP with consistent evidence.Consistent evidence is a property that can not only simplify the process of disputation resolving,but also make the service more friendly to users,which means that whether or not TTP involves,evidences participants obtained are consistent.In the meanwhile we analyze the collusion attack that multi-party protocol facing,our protocol can prevent collusion attack.展开更多
Based on the study of existing fair exchange protocols,this paper sets up an accurate formal model by stepwise refinement.In the process of refinement an unreliable channel is employed to simulate an attack behavior.T...Based on the study of existing fair exchange protocols,this paper sets up an accurate formal model by stepwise refinement.In the process of refinement an unreliable channel is employed to simulate an attack behavior.The model provides a novel formal definition of exchanged items,and presents the formal goals for fairness,accountability,etc.,reflecting the inherent requirements for fair exchange protocols across-the-board.In order to check,prove,and design fair exchange protocols effectively and efficiently,the model puts forward a novel property of abuse-freeness which applies to all fair exchange protocols,gives a formal definition for trust strand of the third party,and presents general criteria of designing a secure and effective fair exchange protocol.Taking a typical fair exchange protocol as an example,this paper presents the analysis steps of fair exchange protocols appealing to our model.An unknown attack is uncovered.The analysis reveals the process of a complete attack,discovering deeper reasons for causing an attack.Finally,we modify the flawed protocol and the revised protocol ensures the desirable properties.展开更多
In order to provide integrity protection for the secure operating system to satisfy the structured protection class＇ requirements, a DTE technique based integrity protection formalization model is proposed after the ...In order to provide integrity protection for the secure operating system to satisfy the structured protection class＇ requirements, a DTE technique based integrity protection formalization model is proposed after the implications and structures of the integrity policy have been analyzed in detail. This model consists of some basic rules for configuring DTE and a state transition model, which are used to instruct how the domains and types are set, and how security invariants obtained from initial configuration are maintained in the process of system transition respectively. In this model, ten invariants are introduced, especially, some new invariants dealing with information flow are proposed, and their relations with corresponding invariants described in literatures are also discussed. The thirteen transition rules with well-formed atomicity are presented in a well-operational manner. The basic security theorems correspond to these invariants and transition rules are proved. The rationalities for proposing the invariants are further annotated via analyzing the differences between this model and ones described in literatures. At last but not least, future works are prospected, especially, it is pointed out that it is possible to use this model to analyze SE-Linux security.展开更多
Numerous Internet security incidents have shown that support from secure operating systems is paramount to fighting threats posed by modern computing environments.Based on the requirements of the relevant national and...Numerous Internet security incidents have shown that support from secure operating systems is paramount to fighting threats posed by modern computing environments.Based on the requirements of the relevant national and international standards and criteria,in combination with our experience in the design and development of the ANSHENG v4.0 secure operating system with high security level(hereafter simply referred to as ANSHENG OS),this paper addresses the following key issues in the design of secure operating systems with high security levels:security architecture,security policy models,and covert channel analysis.The design principles of security architecture and three basic security models:confidentiality,integrity,and privilege control models are discussed,respectively.Three novel security models and new security architecture are proposed.The prominent features of these proposals,as well as their applications to the ANSHENG OS,are elaborated.Cover channel analysis(CCA)is a well-known hard problem in the design of secure operating systems with high security levels since to date it lacks a sound theoretical basis and systematic analysis approach.In order to resolve the fundamental difficulties of CCA,we have set up a sound theoretical basis for completeness of covert channel identification and have proposed a unified framework for covert channel identification and an efficient backward tracking search method.The successful application of our new proposals to the ANSHENG OS has shown that it can help ease and speedup the entire CCA process.展开更多
Based on the origin of message items and channel combination between transacting parties,and events and relations among events,this paper presents a concise,precise,and hierarchical model for general fair exchange pro...Based on the origin of message items and channel combination between transacting parties,and events and relations among events,this paper presents a concise,precise,and hierarchical model for general fair exchange protocols,formally specifies various security requirements which are able to reflect inherent requirements for fair exchange protocols more rigorously,and partition these security requirements with fine granularity.This work helps analyze,debug,and design multi-party fair exchange protocols more effectively and elaborately.展开更多
基金Supported by the National Natural Science Foundation of China (90104005, 60373087, 60473023) and Network and Information Security Key Laboratory Program of Ministry of Education of China
文摘This paper interprets the essence of XEN and hardware virtualization technology, which make the virtual machine technology become the focus of people＇s attention again because of its impressive performance. The security challenges of XEN are mainly researched from the pointes of view： security bottleneck, security isolation and share, life-cycle, digital copyright protection, trusted virtual machine and managements, etc. These security problems significantly affect the security of the virtual machine system based on XEN. At the last, these security measures are put forward, which will be a useful instruction on enhancing XEN security in the future.
基金National High Technology Research and Development Program(863 program)(2007AA01217903)Important Direction for the Project Chinese Academy of Sciences(KGCX2-YW-125)
文摘With development of electronic com-merce,non-repudiation protocol as the basal component of non-repudiation service has done more and more important functions.Comparing with lots of work on two-party non-repudiation,there are less work on multi-party non-repudiation protocol.Multi-party protocol is more complex and facing more challenge of collusion attack.In this paper we give a kind of multi-party non-repudiation protocol based on off-line TTP with consistent evidence.Consistent evidence is a property that can not only simplify the process of disputation resolving,but also make the service more friendly to users,which means that whether or not TTP involves,evidences participants obtained are consistent.In the meanwhile we analyze the collusion attack that multi-party protocol facing,our protocol can prevent collusion attack.
基金the Natural Science Foundation ofBeijing(Grant No.4052016)the National Natural Science Foundation of China(Grant No.60083007)the National Grand Fundamental Research 973 Program ofChina(Grant No.G1999035802).
文摘Based on the study of existing fair exchange protocols,this paper sets up an accurate formal model by stepwise refinement.In the process of refinement an unreliable channel is employed to simulate an attack behavior.The model provides a novel formal definition of exchanged items,and presents the formal goals for fairness,accountability,etc.,reflecting the inherent requirements for fair exchange protocols across-the-board.In order to check,prove,and design fair exchange protocols effectively and efficiently,the model puts forward a novel property of abuse-freeness which applies to all fair exchange protocols,gives a formal definition for trust strand of the third party,and presents general criteria of designing a secure and effective fair exchange protocol.Taking a typical fair exchange protocol as an example,this paper presents the analysis steps of fair exchange protocols appealing to our model.An unknown attack is uncovered.The analysis reveals the process of a complete attack,discovering deeper reasons for causing an attack.Finally,we modify the flawed protocol and the revised protocol ensures the desirable properties.
基金supported by the Beijing Natural Science Foundation(Grant No.4052016)the National Natural Science Foundation of China(Grant No.60573042)the National Grand Fundamental Research 973 Program of China(Grant No.G1999035802).
文摘In order to provide integrity protection for the secure operating system to satisfy the structured protection class＇ requirements, a DTE technique based integrity protection formalization model is proposed after the implications and structures of the integrity policy have been analyzed in detail. This model consists of some basic rules for configuring DTE and a state transition model, which are used to instruct how the domains and types are set, and how security invariants obtained from initial configuration are maintained in the process of system transition respectively. In this model, ten invariants are introduced, especially, some new invariants dealing with information flow are proposed, and their relations with corresponding invariants described in literatures are also discussed. The thirteen transition rules with well-formed atomicity are presented in a well-operational manner. The basic security theorems correspond to these invariants and transition rules are proved. The rationalities for proposing the invariants are further annotated via analyzing the differences between this model and ones described in literatures. At last but not least, future works are prospected, especially, it is pointed out that it is possible to use this model to analyze SE-Linux security.
基金the Natural Science Foundation of Beijing(Grant No.4052016)the National Natural Science Foundation of China(Grant No.60573042)the National Grand Fundamental Research 973 Program of China(Grant No.G1999035802)
文摘Numerous Internet security incidents have shown that support from secure operating systems is paramount to fighting threats posed by modern computing environments.Based on the requirements of the relevant national and international standards and criteria,in combination with our experience in the design and development of the ANSHENG v4.0 secure operating system with high security level(hereafter simply referred to as ANSHENG OS),this paper addresses the following key issues in the design of secure operating systems with high security levels:security architecture,security policy models,and covert channel analysis.The design principles of security architecture and three basic security models:confidentiality,integrity,and privilege control models are discussed,respectively.Three novel security models and new security architecture are proposed.The prominent features of these proposals,as well as their applications to the ANSHENG OS,are elaborated.Cover channel analysis(CCA)is a well-known hard problem in the design of secure operating systems with high security levels since to date it lacks a sound theoretical basis and systematic analysis approach.In order to resolve the fundamental difficulties of CCA,we have set up a sound theoretical basis for completeness of covert channel identification and have proposed a unified framework for covert channel identification and an efficient backward tracking search method.The successful application of our new proposals to the ANSHENG OS has shown that it can help ease and speedup the entire CCA process.
基金This work was supported by the Natural Science Foundation of Beijing(Grant No.4052016)the National Natural Science Foundation of China(Grant No.60573042)the National Grand Fundamental Research 973 Program of China(Grant No.G 1999035802).
文摘Based on the origin of message items and channel combination between transacting parties,and events and relations among events,this paper presents a concise,precise,and hierarchical model for general fair exchange protocols,formally specifies various security requirements which are able to reflect inherent requirements for fair exchange protocols more rigorously,and partition these security requirements with fine granularity.This work helps analyze,debug,and design multi-party fair exchange protocols more effectively and elaborately.
