@techreport{oai:ipsj.ixsq.nii.ac.jp:00232376,
 author = {Joe, Hattori and Yuuki, Takano and Naoki, Kobayashi and Joe, Hattori and Yuuki, Takano and Naoki, Kobayashi},
 issue = {7},
 month = {Feb},
 note = {Linux kernel, predominantly written in C language, has been suffering countless memory bugs, such as use after free, double free, and memory leaks. Linux kernel modules, in particular, are prone to these memory errors as they allow users to write and load the code into kernel at any time. While this flexible design makes Linux highly adaptable for a wide range of applications, the inherent security risks are becoming increasingly severe as more and more new hardware emerges. Given the security concern and the notorious difficultly in detecting such bugs, especially in concurrent execution environments of Linux kernel modules, the demand for automated detection of these bugs are critically high. This paper proposes a tool to automatically detect memory bugs, including those occur exclusively in concurrent executions. This tool traspiles kernel module source to PlusCal, a formal specification language suited for software verification in concurrent scenarios. By transpiling the kernel module source code into concise yet effective PlusCal code, we can detect a wide range of concurrency memory bugs., Linux kernel, predominantly written in C language, has been suffering countless memory bugs, such as use after free, double free, and memory leaks. Linux kernel modules, in particular, are prone to these memory errors as they allow users to write and load the code into kernel at any time. While this flexible design makes Linux highly adaptable for a wide range of applications, the inherent security risks are becoming increasingly severe as more and more new hardware emerges. Given the security concern and the notorious difficultly in detecting such bugs, especially in concurrent execution environments of Linux kernel modules, the demand for automated detection of these bugs are critically high. This paper proposes a tool to automatically detect memory bugs, including those occur exclusively in concurrent executions. This tool traspiles kernel module source to PlusCal, a formal specification language suited for software verification in concurrent scenarios. By transpiling the kernel module source code into concise yet effective PlusCal code, we can detect a wide range of concurrency memory bugs.},
 title = {Towards Automatic Verification of Concurrency Memory Bug Freeness of Linux Kernel Modules by Transpilation to PlusCal},
 year = {2024}
}