| Item type |
SIG Technical Reports(1) |
| 公開日 |
2024-02-12 |
| タイトル |
|
|
タイトル |
Towards Automatic Verification of Concurrency Memory Bug Freeness of Linux Kernel Modules by Transpilation to PlusCal |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Towards Automatic Verification of Concurrency Memory Bug Freeness of Linux Kernel Modules by Transpilation to PlusCal |
| 言語 |
|
|
言語 |
eng |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
一貫性制御 |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_18gh |
|
資源タイプ |
technical report |
| 著者所属 |
|
|
|
University of Tokyo／TIER IV, Inc. |
| 著者所属 |
|
|
|
TIER IV, Inc. |
| 著者所属 |
|
|
|
University of Tokyo |
| 著者所属(英) |
|
|
|
en |
|
|
University of Tokyo / TIER IV, Inc. |
| 著者所属(英) |
|
|
|
en |
|
|
TIER IV, Inc. |
| 著者所属(英) |
|
|
|
en |
|
|
University of Tokyo |
| 著者名 |
Joe, Hattori
Yuuki, Takano
Naoki, Kobayashi
|
| 著者名(英) |
Joe, Hattori
Yuuki, Takano
Naoki, Kobayashi
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
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. |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
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. |
| 書誌レコードID |
|
|
収録物識別子タイプ |
NCID |
|
収録物識別子 |
AN10444176 |
| 書誌情報 |
研究報告システムソフトウェアとオペレーティング・システム（OS）
巻 2024-OS-162,
号 7,
p. 1-6,
発行日 2024-02-12
|
| ISSN |
|
|
収録物識別子タイプ |
ISSN |
|
収録物識別子 |
2188-8795 |
| Notice |
|
|
|
SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. |
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-OS24162007.pdf (878.7 kB)
