Chinese Journal of Computers   Full Text
Title	Static Analysis Based Correctness Verification for Mandatory Access Control Framework
Authors	WU Xin-Song1)，2) ZHOU Zhou-Yi1)，2) HE Ye-Ping1) LIANG Hong-Liang1) YUAN Chun-Yang3)
Address	1)(Institute of Software, Chinese Academy of Sciences, Beijing 100190) 2)(Graduate University of Chinese Academy of Sciences, Beijing 100049) 3)(National Computer Network Emergency Response Technical Team/Coordination Center of China, Beijing 100029)
Year	2009
Issue	No.4(730—739)
Abstract &   Background	Abstract Current researches on correctness verification for the mandatory access control framework of operating systems mainly focus on authorization hooks placement verification. Based on TrustedBSD MAC framework, this paper analyses the correctness verification problem for mandatory access control framework, and proposes complete initialization and complete destruction for security labels, as well as complete authorization for access. In order to enforce these verifications, this paper also presents a path-sensitive and user-defined-rule based static analysis approach. This approach verifies the accuracy and completeness of hooks placement of the mandatory access control framework through extending the compiler integrated static analysis tool-mygcc. It achieves high path cover, low false positive rate and time overhead. Keywords correctness verification; static analysis; mandatory access control framework; hooks placement; mygcc Background This work attributes to the project “FreeBSD-based Trusted Operating System Research and Development”, which is supported by the National Science Foundation of China under grant No. 90818012, the National High Technology Research and Development Program of China (863 Plan) under grant No. 2007AA010601, and Key Project of Chinese Academy of Sciences under grant No. KGCX2-YW-125. Mandatory access control frameworks are important mechanisms of operating systems to support multi-security policies. Security label management hooks and authorization hooks, which are manually inserted into the operating system kernel source code, are essential parts of the mandatory access control framework. Therefore, the correctness of these hooks placement is crucial for the framework. There have been many researches on the correctness verification of the hooks placement of the LSM (Linux Security Module). However, current researches mainly focus on the verification of the authorization hooks placement. In this work, based on the TrustedBSD MAC framework, the authors analyze the correctness verification problems of the security label management hooks placement and the authorization hooks placement. To address these correctness verifications, this paper also presents a path-sensitive and user-defined-rule based static analysis approach. This approach verifies the accuracy and completeness of hooks placement through extending the compiler integrated static analysis tool-mygcc. It achieves complete coverage of execution paths and has low false positive rate. The verified TrustedBSD MAC framework has been implemented in the NFSARK trusted operating system.