Software-Defined Network 形式検証に関 動向
八鍬 豊† 夏子† 富沢 伸行† 内 敏夫†
近年 ン ネ ワ 運用管理 関 SDN(Software-Defined Network) 注目 さ ，運用 自動化 効率化 省電力化 い 期待 集 い ，自 度 高い制御
伴う 具合 混入 可能性 懸念さ い ．そ 々 ，SDN さ 検証 技術
注目 ，特 形式手法 利用 い 動向 調査 い ．本稿 そ い
紹 ，ワ 議論 い い 述 ．
About Formal Verification Techniques of Software-Defined
Network
Yutaka Yakuwa† Natsuko Noda† Nobuyuki Tomizawa† Toshio Tonouchi†
In recent years, SDN (Software-Defined Network) attracts attentions in respect to operation management, and it is expected to be useful for automation, streamlining and electricity saving of data centers. But there is an increasing concern that bugs will arise in networks that have high flexibility of control. Now We are interested in verification techniques of SDN, and we research on trend of them especially using formal methods. In this paper, we introduce them and describe a theme we want to discuss in the workshop.
1. めに
ラ ビ 普及 伴い， ン 安
定運用 後 IT 化社会 大 課題 い ． 例えば，現在多く ビ Amazon Web Service
連携 稼働 い ， そ ン 停
場合，そ ビ 一部 機能 く ．人
命 わ 医療系 ビ 等 機能 支 出
う 考え ，そ 社会 え 影響 計 知
い．そ ， ン 安定運用 目的
数多く 取 組 さ い ．
ン ，特 ネ ワ 運用管理
関 ，Software-Defined Network(以 SDN) 注目さ
い ．ネ ワ 制御 ラ 方法
一元管理 可能 新 パラ あ ，
ン 運用 自動化 効率化 省電力化等， 様々 期待 集 い [7]．
一方 ，ネ ワ 制御 柔軟性 増 分，そ 伴う 具合 生 懸念さ い ．例えば，パ
転送 う う 制御 ，ネ ワ
具合 基本的 ，開 者 ラ
定義 ネ ワ 制御 ，開 者 考慮漏
そ う 具合 混入 ，そ 他 ラ
組 合わ 予期 形 具合 顕在化
多く ． ，SDN ネ ワ 設定 非同期分散 度々変更さ ，そ 最中 制御 整合 生 可能性 あ ．
ほ 一例 あ ，新 パラ あ SDN 世
界 う 具合 起 得 ，そ 全容 明
い． ，将来 ン ネ ワ
SDN 構築さ 多く 思わ ，何
観点 そ ネ ワ さ 担保 検証技術
極 要 ．SDN 概念 実現 コ
代表的 OpenFlow[4] 提唱者 1 人 あ Prof. Mckeown ，Open Networking Summit 2012 基 調講演[5] SDN 検証 要性 訴え い ．
々 SDN 検証 技術 注目 ，特 形式手
法 利用 い 動向 調査 い ．従来
特定 コ ネ ワ 制御 い
形式検証 技術 提案さ い [2]，SDN
従来 コ 比 ネ ワ 制御 自 度
高く，利用 情報や定義 動作 種類 増
．SDN い ， やネ ワ 自体 ソ
実行基盤 一部 言え ．そ ，新
検証技術 必要 考え あ ．
本稿 ，形式手法 SDN 検証技術 動向
†NEC 情報 研究所
Knowledge Discovery Research Labs., NEC Corporation
調査 2 研究事例 紹 ． ，ワ
議論 い い 述 ．
2. SDN とそ 形式検証
SDN ，ネ ワ 制御 ラ 方法
一元管理 目指 パラ あ ．従来
個々 ネ ワ 機器 設定 ネ ワ
全体 制御 い ，SDN ネ ワ 全体 1
ラ ォ 見立 ，ソ 一元的 制
御 ．産業界 SDN 注目 高 い [7]． 形式手法 SDN 検証技術 動向調
査 2 研究事例 紹 ．
2.1. NICE
NICE[1] OpenFlow コン ラ NOX[3]向
あ ． 網羅度 形式
検証技術 利用 い ．基本的 機能 ，入力
コン ラ 用 ラ ネ ワ 構
パ (パ 転送 い等) え ，
パ 否 ， パ 満 さ い場合
反例 出力 ．コン ラ 用 ラ 変更
検証 ， 利便性 高い．
検証 ， 検査 ベ
い ，記号実行 組 合わ 用い ．ネ ワ
流 パ 具体的 値 扱 う 状
態爆 う ，記号実行 コン ラ
等価 パ ラ 導出 ，そ 代表値
用い 検査 行う ，状態数 削減
． ，OpenFlow 検証 特化 索戦略 用 い ． ，実験 Spin や JPF 比較 良好 検証効率 示 結果 得 い ．
，ネ ワ 構 や パ 関
，利用頻度 高い一般的 側 あ
用意 ， そ 選択 利用
可能 形 提供 い ．一方 ， カ
入力 可能 特殊 や
パ い 検証 ，検証 内容 応
柔軟 使い方 可能 あ 言え ．
2.2. ネットワーク設定更新 カニズ 整合性保証 Reitblatt ，OpenFlow ネ ワ 設定(パ
内容 応 処理 定義) 更新 関 整合性 定義 ，そ 整合性 保 ネ ワ 設定 更新 カ 提案 い [6]．
定義 い 整合性 per-packet 整合性 per-flow 整合性 2 種類 あ ．前者 任意 パ 同一
ネ ワ 設定 処理さ いう ，
後者 任意 全 パ 同一 ネ
ワ 設定 処理さ いう あ ．
ネ ワ 設定 更新 ， 整合性 い
満 い ば，ネ ワ 設定 更新前 更
新後 両方 立 任意 性質 ，ネ ワ 設
定 更新中 立 いう 定理証明支援
Coq 証明 い ．
文献 ，ネ ワ 関 基本的 性質 ，
更新前 更新後 設定 い NuSMV 検証
，全体 通 整合性 保 ネ ワ 設定
更新 可能 保証 例 示 い ． ，
NuSMV 限 ，ネ ワ 設定 静的 適用さ 環境 性質 検証 技術 あ ば， 記 整
合性 組 合わ ，ネ ワ 設定 動的
更新さ 環境 性質 否 検証可能 ．
，検証 難 さ 緩和 ．
3. おわ に
本稿 ，ネ ワ 分 い SDN いう
新 パラ 注目さ い ，そ 検証技術
後 要 う 述 ． ，特 形式
手法 用い 検証技術 注目 動向調査 2 研究事例 紹 ．
ワ ，SDN さ 担保 検証
技術 いう 要 向 ，形式手法 いう分
う 議論 い．
参考文献
[1] Canini, M. et al.: “A NICE Way to Test OpenFlow Applications”, Proc. of NSDI, 2012.
[2] Feamster, N. et al.: “Detecting BGP configuration faults with static analysis”, Proc. of NSDI, 2005.
[3] Gude, N. et al.: “NOX: Towards an Operating System for Networks”, ACM SIGCOMM Computer Communication Review, Vol. 38(2), pp. 105-110, 2008.
[4] McKeown, N. et al.: “OpenFlow: Enabling Innovation in Campus Networks”, ACM SIGCOMM Computer Communication Review, Vol. 38(2), pp. 69-74, 2008. [5] McKeown, N.: “Making SDNs Work”, Open Networking
Summit, 2012.
[6] Reitblatt, M. et al.: “Abstractions for network update”, to appear at ACM SIGCOMM, 2012.
[7] 河井保博ほ : “［特集］ Software Defined Network”, 日 経コ ン, No. 574, pp. 8-25, 2011.
