Analyzing and improving Linux kernel memory protection: a model checking approach

Code injection continues to pose a serious threat to computer systems. Among existing solutions, W X is a notable approach to prevent the execution of injected code. In this paper, we focus on the Linux kernel memory protection and systematically check for possible W X violations in the Linux kernel design and implementation. In particular, we eloped a Murphi-based abstract model and used it to discover several serious shortcomings in the current Linux kernel that violate the W X property. We have confirmed with the Linux community the presence of these problems and accordingly developed five Linux kernel patches. (Four of them are in the process of being integrated into the mainline Linux kernel.) Our evaluation with these patches indicate that they involve only minimal changes to the existing code base and incur negligible performance overhead.

• Type: Journal
• Year: 2010
• Where: ACSAC
• Authors: Siarhei Liakh, Michael C. Grace, Xuxian Jiang
• Keywords: ACSAC 2010, Linux Kernel, Linux Kernel Design, Linux Kernel Memory, Security Privacy