| A formal model for integrity protection based on DTE technique |
| |
| 基金项目： | 北京市自然科学基金;国家自然科学基金;国家重点基础研究发展计划(973计划) |
| |
| 摘 要： | 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.
|
| 收稿时间： | 2006-02-07 |
| 修稿时间： | 2006-04-07 |
A formal model for integrity protection based on DTE technique |
| |
| JI Qingguang,QING Sihan,HE Yeping. A formal model for integrity protection based on DTE technique[J]. Science in China(Information Sciences), 2006, 49(5): 545-565. DOI: 10.1007/s11432-006-2014-6 |
| |
| Authors: | JI Qingguang QING Sihan HE Yeping |
| |
| Affiliation: | 1. Engineering Research Center for Information Security Technology, Institute of Software, Chinese Academy of Sciences, Beijing 100080, China
2. Infrastrucure Software Engineering Center, Institute of Software, Chinese Academy of Sciences, Beijing 100080, China |
| |
| Abstract: | 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. |
| |
| Keywords: | formal model integrity policy information flow domain type |
| 本文献已被 万方数据 SpringerLink 等数据库收录！ |
|
