| Item type |
Trans(1) |
| 公開日 |
2024-01-31 |
| タイトル |
|
|
タイトル |
Rabbit: A Modeling Language for Verifying Data-flow Security |
| タイトル |
|
|
言語 |
en |
|
タイトル |
Rabbit: A Modeling Language for Verifying Data-flow Security |
| 言語 |
|
|
言語 |
eng |
| キーワード |
|
|
主題Scheme |
Other |
|
主題 |
[発表概要, Unrefereed Presentatin Abstract] |
| 資源タイプ |
|
|
資源タイプ識別子 |
http://purl.org/coar/resource_type/c_6501 |
|
資源タイプ |
journal article |
| 著者所属 |
|
|
|
School of Informatics, Kyoto University |
| 著者所属 |
|
|
|
National Institute of Informatics |
| 著者所属 |
|
|
|
School of Informatics, Kyoto University |
| 著者所属 |
|
|
|
National Institute of Informatics |
| 著者所属(英) |
|
|
|
en |
|
|
School of Informatics, Kyoto University |
| 著者所属(英) |
|
|
|
en |
|
|
National Institute of Informatics |
| 著者所属(英) |
|
|
|
en |
|
|
School of Informatics, Kyoto University |
| 著者所属(英) |
|
|
|
en |
|
|
National Institute of Informatics |
| 著者名 |
Terunobu, Inaba
Taro, Sekiyama
Atsushi, Igarashi
Yutaka, Ishikawa
|
| 著者名(英) |
Terunobu, Inaba
Taro, Sekiyama
Atsushi, Igarashi
Yutaka, Ishikawa
|
| 論文抄録 |
|
|
内容記述タイプ |
Other |
|
内容記述 |
In systems with high-security requirements such as IoT systems, it is desired to confirm that security requirements are met via formal verification. However, verification often has notations that are largely different from those of general-purpose programming languages. In this presentation, we propose a modeling language called Rabbit, which has both simplicity and an ability of security verification on data flow. In Rabbit, systems are modeled as a parallel process, together with security assumptions, i.e., which variables and communication channels are eavesdropped or tampered. Given a model and security requirements, such as secrecy and integrity, Rabbit verifies whether the model meets the requirements. The verification part is performed by Tamarin Prover, a powerful verification tool for security protocols. The system model in Rabbit is translated into a Tamarin model, and then symbolic model checking is conducted. We implemented a translator from Rabbit to Tamarin Prover. To mitigate computational complexity in the model checking part, we experiment with different translation strategies. We confirmed that Rabbit is sufficiently expressive and the verification via Tamarin Prover finishes in reasonable time in several case studies. |
| 論文抄録(英) |
|
|
内容記述タイプ |
Other |
|
内容記述 |
In systems with high-security requirements such as IoT systems, it is desired to confirm that security requirements are met via formal verification. However, verification often has notations that are largely different from those of general-purpose programming languages. In this presentation, we propose a modeling language called Rabbit, which has both simplicity and an ability of security verification on data flow. In Rabbit, systems are modeled as a parallel process, together with security assumptions, i.e., which variables and communication channels are eavesdropped or tampered. Given a model and security requirements, such as secrecy and integrity, Rabbit verifies whether the model meets the requirements. The verification part is performed by Tamarin Prover, a powerful verification tool for security protocols. The system model in Rabbit is translated into a Tamarin model, and then symbolic model checking is conducted. We implemented a translator from Rabbit to Tamarin Prover. To mitigate computational complexity in the model checking part, we experiment with different translation strategies. We confirmed that Rabbit is sufficiently expressive and the verification via Tamarin Prover finishes in reasonable time in several case studies. |
| 書誌レコードID |
|
|
収録物識別子タイプ |
NCID |
|
収録物識別子 |
AA11464814 |
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO）
巻 17,
号 1,
p. 12-12,
発行日 2024-01-31
|
| ISSN |
|
|
収録物識別子タイプ |
ISSN |
|
収録物識別子 |
1882-7802 |
| 出版者 |
|
|
言語 |
ja |
|
出版者 |
情報処理学会 |
IPSJ-TPRO1701003.pdf (30.1 kB)
