| 電子情報通信学会 研究会発表申込システム 講演論文 詳細 |
技報閲覧サービス [ログイン] 技報アーカイブ |
| トップに戻る | 前のページに戻る | [Japanese] / [English] |
| 講演抄録／キーワード | ||
| 講演名 | 2026-09-15 16:30 Yosegine: NaaSを含むネットワークのパケット処理仕様に基づくDesign-Plane Verification ○森脇遼太・岡部寿男・小谷大祐（京大）  IA2026-33 |
|
| 抄録 | （和） | Network Verificationは，ネットワークの設計や設定，状態が意図した性質を満たすかどうかを形式手法で検証し，管理者を支援する技術である． 従来の手法は，ネットワーク上の機器の設定・状態情報を用いてモデル化し，control-planeまたはdata-planeの検証を行ってきた． しかし，NaaSなどの内部情報を取得できない区間を含むネットワークでは，全区間の情報を前提とする従来手法だけで全体を検証することは難しい． 本研究では機器の具体的な設定情報ではなく，各区間のネットワークの仕様を入力として全体の設計上の整合性を確認するdesign-plane verificationと，それを実現するシステムYosegineを提案する． Yosegineは，入手できる情報の粒度などに応じて分割された各区間のパケット処理仕様（入力ポート，ヘッダ条件，ヘッダ変換，出力ポート等のルール）を入力とする． この仕様をモデル化してシンボリック実行を行うことで，外部サービスの内部情報を取得できない場合も，複数区間を組み合わせた際の設計上の不整合を検出する． 実際にNaaSが使われたJANOG57のイベントネットワークを例として，設計をパケット処理仕様として表現し，Yosegineによるdesign-plane verificationが可能であることを確認した． |
| （英） | Network verification uses formal methods to determine whether a network's design, configuration, and state satisfy intended properties. Conventional approaches model networks using device configuration and state information to verify the control plane or data plane. However, end-to-end verification is difficult when a network includes segments whose internal information is unavailable, as in Network-as-a-Service (NaaS). This paper proposes design-plane verification, which examines the consistency of an overall network design based on segment-level specifications rather than detailed device configurations. We also present Yosegine, a system that takes packet-processing specifications for each segment, including input ports, header conditions, header transformations, and output ports. Yosegine models these specifications and performs symbolic execution to detect design inconsistencies that arise when multiple segments are combined, even when the internal details of external services are unavailable. We applied Yosegine to the JANOG57 event network, which used NaaS, and demonstrated that its design can be represented and verified using packet-processing specifications. |
|
| キーワード | （和） | ネットワーク検証 / Design-Plane Verification / / / / / / |
| （英） | Network Verification / Design-Plane Verification / / / / / / | |
| 文献情報 | 信学技報, vol. 126, no. 180, IA2026-33, pp. 40-47, 2026年9月. | |
| 資料番号 | IA2026-33 | |
| 発行日 | 2026-09-08 (IA) | |
| ISSN | Online edition: ISSN 2432-6380 | |
| 著作権に ついて |
技術研究報告に掲載された論文の著作権は電子情報通信学会に帰属します．(許諾番号：10GA0019/12GB0052/13GB0056/17GB0034/18GB0034) | |
| PDFダウンロード | IA2026-33 |
|
| 研究会情報 | |
| 研究会 | IA |
| 開催期間 | 2026-09-15 - 2026-09-16 |
| 開催地（和） | 北海道大学 情報基盤センター南館 |
| 開催地（英） | Hokkaido Univ. |
| テーマ（和） | インターネット運用・管理, ネットワークアーキテクチャ, 通信プロトコル, IoT, 一般 |
| テーマ（英） | Internet Operation and Management, Network Architecture, Communication Protocols, IoT, etc. |
| 講演論文情報の詳細 | |
| 申込み研究会 | IA |
| 会議コード | 2026-09-IA |
| 本文の言語 | 日本語 |
| タイトル（和） | Yosegine: NaaSを含むネットワークのパケット処理仕様に基づくDesign-Plane Verification |
| サブタイトル（和） | |
| タイトル（英） | Yosegine: Design-Plane Verification for NaaS-Integrated Networks Based on Packet Processing Specifications |
| サブタイトル（英） | |
| キーワード(1)（和/英） | ネットワーク検証 / Network Verification |
| キーワード(2)（和/英） | Design-Plane Verification / Design-Plane Verification |
| キーワード(3)（和/英） | / |
| キーワード(4)（和/英） | / |
| キーワード(5)（和/英） | / |
| キーワード(6)（和/英） | / |
| キーワード(7)（和/英） | / |
| キーワード(8)（和/英） | / |
| 第1著者 氏名（和/英/ヨミ） | 森脇 遼太 / Ryota Moriwaki / モリワキ リョウタ |
| 第1著者 所属（和/英） | 京都大学 (略称： 京大) Kyoto University (略称： Kyoto Univ.) |
| 第2著者 氏名（和/英/ヨミ） | 岡部 寿男 / Yasuo Okabe / オカベ ヤスオ |
| 第2著者 所属（和/英） | 京都大学 (略称： 京大) Kyoto University (略称： Kyoto Univ.) |
| 第3著者 氏名（和/英/ヨミ） | 小谷 大祐 / Daisuke Kotani / コタニ ダイスケ |
| 第3著者 所属（和/英） | 京都大学 (略称： 京大) Kyoto University (略称： Kyoto Univ.) |
| 講演者 | 第1著者 |
| 発表日時 | 2026-09-15 16:30:00 |
| 発表時間 | 25分 |
| 申込先研究会 | IA |
| 資料番号 | IA2026-33 |
| 巻番号（vol） | vol.126 |
| 号番号（no） | no.180 |
| ページ範囲 | pp.40-47 |
| ページ数 | 8 |
| 発行日 | 2026-09-08 (IA) |
[研究会発表申込システムのトップページに戻る]