@techreport{oai:ipsj.ixsq.nii.ac.jp:00216999,
 author = {細谷, 昂平 and 高野, 祐輝 and 宮地, 充子},
 issue = {15},
 month = {Mar},
 note = {SDN や NFV といった技術の発展によってソフトウェアでのパケット処理の需要が高まっている．10-100GbE の普及により端末間のデータ通信は高速に行える環境が整備されつつあるが，ソフトウェアでの処理はハードウェアに比べて低速であるため通信のボトルネックとなっている．この問題を解決する一例として DPDK を代表とするカーネルバイパス技術が挙げられる．また，ネットワークサービスにおける深刻な障害の要因としてソフトウェアのバグが占める割合が高いという現状があるため，ネットワークファンクションを構築する上でソフトウェアのメモリ安全性や仕様の検証を行うことが望まれる．本論文では，上述の DPDK を用いてユーザー空間での高速なパケット処理を実現し，Rust 言語を用いてマップを構成することで仕様に誤りなく動作する NAT を実装する．Rust 言語で構成されるマップは Rust 言語の検証器である Prusti を用いて検証され，追加，削除，参照といった操作をメモリ安全かつ仕様に誤りなく行うことができ，本手法を用いることで他のネットワークファンクションにおいてもデータ構造の検証が可能となると考えられる．, 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.},
 title = {Rust言語を用いたNATの実装と検証},
 year = {2022}
}