WEKO3
アイテム
Coqを用いたソフトウェアスイッチの設計と実装
https://ipsj.ixsq.nii.ac.jp/records/210108
https://ipsj.ixsq.nii.ac.jp/records/21010854afc2e7-0c78-4a85-9da5-97236cf9df4d
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-CSEC21092011.pdf (933.5 kB)
|
Copyright (c) 2021 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | SIG Technical Reports(1) | |||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 公開日 | 2021-03-08 | |||||||||||
| タイトル | ||||||||||||
| タイトル | Coqを用いたソフトウェアスイッチの設計と実装 | |||||||||||
| タイトル | ||||||||||||
| 言語 | en | |||||||||||
| タイトル | Design and Implementation of Software Switch using Coq | |||||||||||
| 言語 | ||||||||||||
| 言語 | jpn | |||||||||||
| キーワード | ||||||||||||
| 主題Scheme | Other | |||||||||||
| 主題 | システム設計・実装 | |||||||||||
| 資源タイプ | ||||||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_18gh | |||||||||||
| 資源タイプ | technical report | |||||||||||
| 著者所属 | ||||||||||||
| 大阪大学 | ||||||||||||
| 著者所属 | ||||||||||||
| 大阪大学 | ||||||||||||
| 著者所属 | ||||||||||||
| 大阪大学／北陸先端科学技術大学院大学 | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Osaka University | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Osaka University | ||||||||||||
| 著者所属(英) | ||||||||||||
| en | ||||||||||||
| Osaka University / Japan Advanced Institute of Science and Technology | ||||||||||||
| 著者名 |
斎藤, 文弥
× 斎藤, 文弥
× 高野, 祐輝
× 宮地, 充子
|
|||||||||||
| 論文抄録 | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | 多くの端末がネットワークに繋がるようになるにつれ，スイッチなどを含むネットワークファンクションの重要性が増している．スイッチはネットワークとユーザーの端末を繋ぐ機能があり，管理が容易なソフトウェアスイッチにおいても安全なソフトウェアスイッチの設計は重要である．しかし，ソフトウェアスイッチではしばしばバグやエラーなどにより通信障害が発生するため，動作の検証が必要である．Coq は定理証明支援系言語であり，定義された関数や式の正しさをプログラム上で証明可能である．本論文では，パケットハンドリング機構の一つである Raw Socket を用いて各端末の MAC アドレスを管理するソフトウェアスイッチの設計と実装を行った．特に，MAC アドレスの管理については Coq で動きを検証した．この結果，形式的に検証されたソフトウェアスイッチの基礎実装を実現した． | |||||||||||
| 論文抄録(英) | ||||||||||||
| 内容記述タイプ | Other | |||||||||||
| 内容記述 | As more and more devices are connected to the network, the importance of Network functions, including switches, is increasing. Switches have the function of connecting networks and users' devices, and it is important to design safe software switches even for software switches which are easy to manage. However, since network disturbance often occurs in software switches due to bugs and errors, we have to verify the operation of them. An interactive theorem prover language, called Coq, can prove some defined functions and formulas on the program. In this paper, a software switch controlling the MAC addresses of each device is designed and implemented using Raw Socket, which is one of the packet handling mechanisms. Especially, we verified the operation of the MAC addresses management in Coq. As a result, formally verified fundamental implementation of the software switch was realized. | |||||||||||
| 書誌レコードID | ||||||||||||
| 収録物識別子タイプ | NCID | |||||||||||
| 収録物識別子 | AA11235941 | |||||||||||
| 書誌情報 |
研究報告コンピュータセキュリティ（CSEC） 巻 2021-CSEC-92, 号 11, p. 1-8, 発行日 2021-03-08 |
|||||||||||
| ISSN | ||||||||||||
| 収録物識別子タイプ | ISSN | |||||||||||
| 収録物識別子 | 2188-8655 | |||||||||||
| Notice | ||||||||||||
| SIG Technical Reports are nonrefereed and hence may later appear in any journals, conferences, symposia, etc. | ||||||||||||
| 出版者 | ||||||||||||
| 言語 | ja | |||||||||||
| 出版者 | 情報処理学会 | |||||||||||
