Verifying mediations of Linux Security Modules with BLAST

The Linux Security Modules (LSM) framework provides a flexible access control mechanism for the Linux kernel. While plenty of efforts were dedicated to put LSM into the kernel, there has been little work on verifying the correct placement of authorization hooks. This paper proposes an approach to verify the mediations of LSM using BLAST, a software model checker for C programs. We choose several subsystems in the Linux kernel source code to verify the mediations of controlling functions using our approach. We also discuss the effectiveness and limitations of our approach and the solutions for future improvement.