In the kernel, the MAC module is the basis of security policy implementation. Hence its correctness is of utmost importance. The current research on the correctness of the MAC focuses primarily on the verification of the placements of authorization hook functions. This article analyzed the issue of verifying correctness of the MAC framework and on this basis, raised the concept of authorization verification. With regard to limitations in current verification methods, we introduce selective symbolic execution for analyzing the correctives of MAC framework. This method can realize the placement problem of hook functions and ensure the accuracy and completeness of such placements. This method is able to offer complete path coverage just like the normal static analysis method yet has higher precision and performance. This method has helped determine a path that may cause a bypass error.
展开▼
