WEKO3
アイテム
Rust言語を用いたNATの実装と検証
https://ipsj.ixsq.nii.ac.jp/records/216999
https://ipsj.ixsq.nii.ac.jp/records/216999fcb0c668-f43f-42ca-98c5-c08f197d81c3
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-DPS22190015.pdf (1.6 MB)
|
Copyright (c) 2022 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2022-03-03 | |||||||||||
| タイトル | ||||||||||||
| タイトル | Rust言語を用いたNATの実装と検証 | |||||||||||
| タイトル | ||||||||||||
| 言語 | en | |||||||||||
| タイトル | Implementation and Verification of A NAT in Rust | |||||||||||
| 言語 | ||||||||||||
| 言語 | jpn | |||||||||||
| キーワード | ||||||||||||
| 主題Scheme | Other | |||||||||||
| 主題 | システム設計・実装 | |||||||||||
| 資源タイプ | ||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||||||
| 資源タイプ | technical report | |||||||||||
| 著者所属 | ||||||||||||
| 大阪大学大学院工学研究科 | ||||||||||||
| 著者所属 | ||||||||||||
| 大阪大学大学院工学研究科 | ||||||||||||
| 著者所属 | ||||||||||||
| 大阪大学大学院工学研究科／北陸先端科学技術大学院大学 | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Graduate School of Engineering, Osaka University | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Graduate School of Engineering, Osaka University | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Graduate School of Engineering, Osaka University / Japan Advanced Institute of Science and Technology(JAIST) | ||||||||||||
| 著者名 |
細谷, 昂平
× 細谷, 昂平
× 高野, 祐輝
× 宮地, 充子
|
|||||||||||
| 論文抄録 | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | SDN や NFV といった技術の発展によってソフトウェアでのパケット処理の需要が高まっている．10-100GbE の普及により端末間のデータ通信は高速に行える環境が整備されつつあるが，ソフトウェアでの処理はハードウェアに比べて低速であるため通信のボトルネックとなっている．この問題を解決する一例として DPDK を代表とするカーネルバイパス技術が挙げられる．また，ネットワークサービスにおける深刻な障害の要因としてソフトウェアのバグが占める割合が高いという現状があるため，ネットワークファンクションを構築する上でソフトウェアのメモリ安全性や仕様の検証を行うことが望まれる．本論文では，上述の DPDK を用いてユーザー空間での高速なパケット処理を実現し，Rust 言語を用いてマップを構成することで仕様に誤りなく動作する NAT を実装する．Rust 言語で構成されるマップは Rust 言語の検証器である Prusti を用いて検証され，追加，削除，参照といった操作をメモリ安全かつ仕様に誤りなく行うことができ，本手法を用いることで他のネットワークファンクションにおいてもデータ構造の検証が可能となると考えられる． | |||||||||||
| 論文抄録(英) | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | The development of technologies such as SDN and NFV has increased the demand for software packet processing. With the spread of 10-100GbE, a high-speed environment for data communication between terminals is being developed, but software processing is slower than hardware, and thus becomes a bottleneck for communication. Kernel bypass technology, such as DPDK, is an example of a solution to this problem. In addition, software bugs account for a large percentage of serious failures in network services, so it is desirable to verify the memory safety and specifications of software when constructing network functions. In this paper, we implement a NAT that can operate without errors in the specifications by realizing fast packet processing in user space using the DPDK described above and constructing maps using the Rust language. The map constructed in the Rust language is verified using Prusti, a verifier for the Rust language, and operations such as addition, deletion, and reference can be performed memory-safely and without specification errors. | |||||||||||
| 書誌レコードID | ||||||||||||
| 収録物識別子タイプ | NCID | |||||||||||
| 収録物識別子 | AN10116224 | |||||||||||
| 書誌情報 |
研究報告マルチメディア通信と分散処理（DPS） 巻 2022-DPS-190, 号 15, p. 1-8, 発行日 2022-03-03 |
|||||||||||
| ISSN | ||||||||||||
| 収録物識別子タイプ | ISSN | |||||||||||
| 収録物識別子 | 2188-8906 | |||||||||||
| Notice | ||||||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||||||
| 出版者 | ||||||||||||
| 言語 | ja | |||||||||||
| 出版者 | 情報処理学会 | |||||||||||
