ネットワーク機器におけるステートレスな制御のための処理を扱えるネットワーク検証

ネットワーク機器における ステートレスな制御のための処理 を扱えるネットワーク検証 京都大学 森脇 遼太, 小谷 大祐, 岡部 寿男 1

背景：ネットワークの運用は難しい    ネットワークは複数の機器が協調して動作 各機器が設定・状態を持つ ネットワーク機器における様々な処理   データの転送やフィルタリング ネットワーク制御のための処理 安定した運用を行うためには 整合性を保つ必要があり難しい 2

関連研究：ネットワーク検証 ネットワークが管理者の意図通りに設定されているか形式手法で検証 「ネットワークはinvariantを満たすか」という問題を解く • invariant：管理者が指定するネットワークが満たすべき性質 • 「ホストAからホストBへの通信は遮断される」 • 「クライアントはDHCPサーバーとDHCPメッセージをやりとりできる」 様々な検証手法が提案されている： Anteater, NetSAT, Header Space Analysis, Graft, Batfish, VMN, SymNET 3

関連研究：Header Space Analysis [Kazemian et al. 2012]   パケットのヘッダーをビット列で表現 ネットワーク機器によるパケット転送処理を関数 𝑻𝑻(𝒉𝒉, 𝒑𝒑)として表現   受け取ったパケットを一部書き換えて出力する関数 ポートの接続情報をモデル化した関数 𝚪𝚪(𝒉𝒉, 𝒑𝒑) と組み合わせる 𝑻𝑻 𝒉𝒉, 𝒑𝒑 = 𝒉𝒉′ , 𝒑𝒑′ 𝒊𝒊𝒊𝒊 < ��𝟏𝟏 > � ′′ ′′ 𝒉𝒉 , 𝒑𝒑 𝒊𝒊𝒊𝒊 < ��𝟐𝟐 > 𝒉𝒉: ビット列で表したヘッダー 𝒑𝒑: パケットを入出力するポート 4

ネットワーク機器における処理を表す関数 • ネットワーク機器におけるパケット転送処理を表す関数を Transfer Function と呼ぶ • Transfer Function はネットワーク機器による各処理を表す関数を合成したもの • 各処理を表す関数を Processing Transfer Function と呼ぶことにする 宛先IPアドレスに基づいて適切なポートから出力する処理の Processing Transfer Function 𝑻𝑻𝒇𝒇𝒇𝒇𝒇𝒇 � # show ip cef Prefix Interface 0.0.0.0/0 Gi1 192.168.1.0/24 Gi2 𝑇𝑇𝑓𝑓𝑓𝑓𝑓𝑓 ℎ, 𝑝𝑝 = ℎ, Gi2 𝑖𝑖𝑖𝑖 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑(ℎ) ∈ 192.168.1.0/24 � ℎ, Gi1 𝑖𝑖𝑖𝑖 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑 ℎ ∈ 0.0.0.0/0 すべての処理を関数として表現することは必ずしも簡単ではない 5

関数の表現が難しい処理 • プロトコルの仕様や他の設定情報等も参照して決まるような処理は難しい • 例えば、DHCP relay では宛先IPアドレス以外の多くのフィールドも変化 DHCPが正しく動作することを保証するためには relayされたパケットがDHCPサーバーに届くことも保証する必要がある 6

提案：ネットワーク機器の処理を表す関数 HSAで考慮されていた処理 ステートレスな ネットワーク制御のための処理 DHCP relayなどの ・入力パケットやポート ・機器の設定 ・プロトコルの仕様 から決定されるパケット処理 モデル化が容易になる情報を取得可能 情報は設定ファイルの数行の記述のみ 仕様や他の設定情報を用いた補完が必要 本提案で関数として表現 より多くの処理が使われた複雑なネットワークもHSAで検証可能に 7

• • ステートレスな制御のための処理を表す関数 複数の機器の共通部分を、関数のひな型として作成 機器ごとに異なる部分はhostinfo()関数として表現 8

DHCP relay の処理を表す関数のひな型 クライアントからサーバー へリレーする処理 サーバーからクライアント へリレーする処理 9

動作説明 R1(Cisco IOS)のコンフィグ ip route 198.51.100.0/24 203.0.113.2 interface Gi1 ip address 203.0.113.1/24 interface Gi2 ip address 192.0.2.1/24 ip helper-address 198.51.100.2 R2のACLの設定 ACL Gi1 in permit udp 192.0.2.1/32:67 → 198.51.100.2/32:67 deny ip all ACL Gi2 in permit udp 198.51.100.2/32:67 → 192.0.2.1/32:67 deny ip all 10

T𝑑𝑑𝑑𝑑𝑑𝑑𝑑_𝑟𝑟𝑟𝑟𝑟𝑟𝑟𝑟𝑟𝑟 ℎ,𝑝𝑝 R1の設定ファイルや 実装に関する情報 • • • • {(𝒉𝒉_𝒄𝒄𝒄𝒄𝒔𝒔𝟏𝟏 , 𝒑𝒑), … , (𝒉𝒉_𝒄𝒄𝒄𝒄𝒔𝒔𝒏𝒏 , 𝒑𝒑)} 𝒊𝒊𝒊𝒊 𝒊𝒊𝒊𝒊_𝒅𝒅𝒅𝒅𝒅𝒅 𝒉𝒉 ∈ 255.255.255.255, 𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉 router, ipaddr,𝒊𝒊𝒊𝒊 = if_relay ∧ 𝒊𝒊𝒊𝒊_𝒑𝒑𝒑𝒑𝒑𝒑𝒑𝒑𝒑𝒑 𝒉𝒉 = 17 ∧ 𝒖𝒖𝒖𝒖𝒖𝒖_𝒅𝒅𝒅𝒅𝒅𝒅 𝒉𝒉 = 67 ∧ 𝒅𝒅𝒅𝒅𝒅𝒅𝒅𝒅_𝒐𝒐𝒐𝒐 𝒉𝒉 = 𝟏𝟏 ∧ 𝒅𝒅𝒅𝒅𝒅𝒅𝒅𝒅_𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉 𝒉𝒉 ≤ 𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉 router, hop_limit ∧ 𝒅𝒅𝒅𝒅𝒅𝒅𝒅𝒅_𝒈𝒈𝒈𝒈𝒈𝒈𝒈𝒈𝒈𝒈𝒈𝒈 𝒉𝒉 = 0 ∧ 𝒑𝒑 = if_relay 𝒉𝒉_𝒄𝒄𝒄𝒄𝒔𝒔𝒊𝒊 = 𝑹𝑹(𝒉𝒉, ip_src = 𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉 router, relay_srcaddr, 𝒊𝒊𝒊𝒊 = if_relay , ip_dst = 𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉 router, dhcp_server, if=if_relay, index = 𝒊𝒊 , udp_src = 67, dhcp_hops = 𝒅𝒅𝒅𝒅𝒅𝒅𝒅𝒅_𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉 𝒉𝒉 + 𝟏𝟏, dhcp_giaddr = 𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉 router, ipaddr, if=if_relay ) DHCPサーバーは198.51.100.2 送信元IPアドレスも192.0.2.1 RelayAgentのアドレスは 192.0.2.1 リレーは最大16hop クライアントからサーバーへリレーする処理 ひな型の𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉()に代入 {(𝑹𝑹(𝒉𝒉, ip_src = 192.0.2.1, 𝒊𝒊𝒊𝒊 𝒊𝒊𝒊𝒊_𝒅𝒅𝒅𝒅𝒅𝒅 𝒉𝒉 ∈ [255.255.255.255, 192.0.2.1] ip_dst = 198.51.100.2, ∧ 𝒊𝒊𝒊𝒊_𝒑𝒑𝒑𝒑𝒑𝒑𝒑𝒑𝒑𝒑 𝒉𝒉 = 17 ∧ 𝒖𝒖𝒖𝒖𝒖𝒖_𝒅𝒅𝒅𝒅𝒅𝒅 𝒉𝒉 = 67 udp_src = 67, ∧ 𝒅𝒅𝒅𝒅𝒅𝒅𝒅𝒅_𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉 𝒉𝒉 ≤ 15 ∧ 𝒅𝒅𝒅𝒅𝒅𝒅𝒅𝒅_𝒈𝒈𝒈𝒈𝒈𝒈𝒈𝒈𝒈𝒈𝒈𝒈 𝒉𝒉 = 0 dhcp_hops = 𝒅𝒅𝒅𝒅𝒅𝒅𝒅𝒅_𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉 𝒉𝒉 + 1, ∧ 𝒑𝒑 = Gi𝟐𝟐 dhcp_giaddr = 192.0.2.1), 𝒑𝒑)} 11

R1 の 𝑇𝑇𝑓𝑓𝑓𝑓𝑓𝑓 ℎ, 𝑝𝑝 ☎経路情報を基に構成 FIB取得コマンドやbatfishを用いて経路情報を取得 # show ip cef 設定ファイル Prefix Interface 198.51.100.0/24 Gi1 203.0.113.0/24 Gi1 192.0.2.0/24 Gi2 batfish 経路情報 経路情報を基に 𝑇𝑇𝑓𝑓𝑓𝑓𝑓𝑓 ℎ, 𝑝𝑝 を構成 𝑇𝑇𝑓𝑓𝑓𝑓𝑓𝑓 ℎ, 𝑝𝑝 = ℎ, Gi1 ℎ, Gi1 ℎ, Gi2 𝑖𝑖𝑖𝑖 𝑖𝑖𝑖𝑖 _𝑑𝑑𝑑𝑑𝑑𝑑 (ℎ) ∈ 198.51.100.0/24 𝑖𝑖𝑖𝑖 𝑖𝑖𝑖𝑖 _𝑑𝑑𝑑𝑑𝑑𝑑 (ℎ) ∈ 203.0.113.0/24 𝑖𝑖𝑖𝑖 𝑖𝑖𝑖𝑖 _𝑑𝑑𝑑𝑑𝑑𝑑 (ℎ) ∈ 192.0.2.0/24 𝑖𝑖𝑖𝑖 𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜 12

R1のTransfer Function 𝑇𝑇𝑅𝑅𝑅 (ℎ, 𝑝𝑝)の構成 𝑇𝑇𝑅𝑅𝑅 ℎ, 𝑝𝑝 は 𝑇𝑇𝑓𝑓𝑓𝑓𝑓𝑓 (ℎ, 𝑝𝑝)と𝑇𝑇𝑑𝑑𝑑𝑑𝑑𝑑𝑑_𝑟𝑟𝑟𝑟𝑟𝑟𝑟𝑟𝑟𝑟 (ℎ, 𝑝𝑝)を合成して構成 𝑇𝑇𝑅𝑅𝑅 ℎ, 𝑝𝑝 = 𝑇𝑇𝑓𝑓𝑓𝑓𝑓𝑓 (𝑇𝑇𝑑𝑑𝑑𝑑𝑑𝑑𝑑_𝑟𝑟𝑟𝑟𝑟𝑟𝑟𝑟𝑟𝑟 (ℎ, 𝑝𝑝) )= 𝑅𝑅 ℎ, 𝑖𝑖𝑖𝑖_𝑠𝑠𝑠𝑠𝑠𝑠 = 192.0.2.1, 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑 = 198.51.100.0, ⋯ , Gi1 𝑅𝑅 ℎ, 𝑖𝑖𝑖𝑖_𝑠𝑠𝑠𝑠𝑠𝑠 = 192.0.2.1, 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑 = 𝑑𝑑𝑑𝑑𝑑𝑑𝑑_𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦 ℎ , ⋯ , Gi2 ⋮ ℎ, 𝐺𝐺𝐺𝐺𝐺 { ℎ, 𝐺𝐺𝐺𝐺𝐺 } { ℎ, 𝐺𝐺𝐺𝐺𝐺 } {} 𝑖𝑖𝑖𝑖 𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵 ∧ 𝑝𝑝 = Gi2 𝑖𝑖𝑖𝑖 𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵 ∧ 𝑝𝑝 = Gi1 𝑖𝑖𝑖𝑖 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑(ℎ) ∈ 192.0.2.0/24 𝑖𝑖𝑖𝑖 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑 ℎ ∈ 203.0.113.0/24 𝑖𝑖𝑖𝑖 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑 ℎ ∈ 198.51.100.0/24 𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜 13

R2のTransfer Function 𝑇𝑇𝑅𝑅𝑅 (ℎ, 𝑝𝑝)の構成 ACL Gi1 in permit udp 192.0.2.1/32:67 → 198.51.100.2/32:67 deny ip all ACL Gi2 in permit udp 198.51.100.2/32:67 → 192.0.2.1/32:67 deny ip all ℎ, Gi2 ℎ, Gi1 𝑇𝑇𝑅𝑅𝑅 ℎ, 𝑝𝑝 = {} 𝑖𝑖𝑖𝑖 𝑖𝑖𝑖𝑖_𝑠𝑠𝑠𝑠𝑠𝑠 ℎ = 192.0.2.1 ∧ 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑(ℎ) = 198.51.100.2 ∧ 𝑖𝑖𝑖𝑖_𝑝𝑝𝑝𝑝𝑝𝑝𝑝𝑝𝑝𝑝 ℎ = 17 ∧ 𝑢𝑢𝑢𝑢𝑢𝑢_𝑠𝑠𝑠𝑠𝑠𝑠 ℎ = 67 ∧ 𝑢𝑢𝑢𝑢𝑢𝑢_𝑑𝑑𝑑𝑑𝑑𝑑 ℎ = 67 ∧ 𝑝𝑝 = Gi1 𝑖𝑖𝑖𝑖 𝑖𝑖𝑖𝑖_𝑠𝑠𝑠𝑠𝑠𝑠 ℎ = 198.51.100.2 ∧ 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑(ℎ) = 192.0.2.1 ∧ 𝑖𝑖𝑖𝑖_𝑝𝑝𝑝𝑝𝑝𝑝𝑝𝑝𝑝𝑝 ℎ = 17 ∧ 𝑢𝑢𝑢𝑢𝑢𝑢_𝑠𝑠𝑠𝑠𝑠𝑠 ℎ = 67 ∧ 𝑢𝑢𝑢𝑢𝑢𝑢_𝑑𝑑𝑑𝑑𝑑𝑑 ℎ = 67 ∧ 𝑝𝑝 = Gi2 𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜 14

DHCP relayの検証 1) クライアントのDHCPDISCOVERがR1でリレーされる 2) R1のGi1から送信されたパケットはR2のGi1に届く 𝑇𝑇𝑅𝑅𝑅 ℎ, 𝑝𝑝 = 𝑅𝑅 ℎ, 𝑖𝑖𝑖𝑖_𝑠𝑠𝑠𝑠𝑠𝑠 = 192.0.2.1, 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑 = 198.51.100.0, ⋯ , Gi1 � 𝑅𝑅 ℎ, 𝑖𝑖𝑖𝑖_𝑠𝑠𝑠𝑠𝑠𝑠 = 192.0.2.1, 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑 = 𝑑𝑑𝑑𝑑𝑑𝑑𝑑_𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦 ℎ , ⋯ , Gi2 ⋮ DHCP DISCOVER src: 0.0.0.0:68 dst: 255.255.255.255:67 proto: 17(udp) giaddr: 0.0.0.0 𝑇𝑇𝑅𝑅𝑅 (ℎ, 𝑝𝑝) DHCP DISCOVER src: 192.0.2.1:67 dst: 198.51.100.0:67 proto: 17(udp) giaddr: 192.0.2.1 𝑖𝑖𝑖𝑖 𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵 ∧ 𝑝𝑝 = Gi2 𝑖𝑖𝑖𝑖 𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵 ∧ 𝑝𝑝 = Gi1 ポートの接続情報 Γ ℎ, 𝑝𝑝 = ℎ, R2:Gi1 � 𝑖𝑖𝑖𝑖 𝑝𝑝 = R1:Gi1 ⋮ 15

DHCP relayの検証 𝑇𝑇𝑅𝑅𝑅 ℎ, 𝑝𝑝 = ℎ, Gi2 {} ℎ, Gi1 1) クライアントのDHCPDISCOVERがR1でリレーされる 2) R1のGi1から送信されたパケットはR2のGi1に届く 3) リレーされたパケットがR2で転送され DHCPサーバーに届く 𝑖𝑖𝑖𝑖 𝑖𝑖𝑖𝑖_𝑠𝑠𝑠𝑠𝑠𝑠 ℎ = 192.0.2.1 ∧ 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑(ℎ) = 198.51.100.2 ∧ 𝑖𝑖𝑖𝑖_𝑝𝑝𝑝𝑝𝑝𝑝𝑝𝑝𝑝𝑝 ℎ = 17 ∧ 𝑢𝑢𝑢𝑢𝑢𝑢_𝑠𝑠𝑠𝑠𝑠𝑠 ℎ = 67 ∧ 𝑢𝑢𝑢𝑢𝑢𝑢_𝑑𝑑𝑑𝑑𝑑𝑑 ℎ = 67 ∧ 𝑝𝑝 = Gi1 𝑖𝑖𝑖𝑖 𝑖𝑖𝑖𝑖_𝑠𝑠𝑠𝑠𝑠𝑠 ℎ = 198.51.100.2 ∧ 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑(ℎ) = 192.0.2.1 ∧ 𝑖𝑖𝑖𝑖_𝑝𝑝𝑝𝑝𝑝𝑝𝑝𝑝𝑝𝑝(ℎ) = 17 ∧ 𝑢𝑢𝑢𝑢𝑢𝑢_𝑠𝑠𝑠𝑠𝑠𝑠 ℎ = 67 ∧ 𝑢𝑢𝑢𝑢𝑢𝑢_𝑑𝑑𝑑𝑑𝑑𝑑 ℎ = 67 ∧ 𝑝𝑝 = Gi2 𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜𝑜 DHCP DISCOVER src: 192.0.2.1:67 dst: 198.51.100.0:67 proto: 17(udp) giaddr: 192.0.2.1 𝑇𝑇𝑅𝑅2 (ℎ, 𝑝𝑝) DHCP DISCOVER src: 192.0.2.1:67 dst: 198.51.100.0:67 proto: 17(udp) giaddr: 192.0.2.1 16

DHCP relay時の送信元IPアドレスについて 使うべき値がRFCでは規定されていない DHCP relayをするIFのアドレスを使う実装が多いがそうとは限らない ip helper-address 198.51.100.2 DHCP relayが設定されたインタフェースのアドレスを使う 𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉 router, relay_srcaddr, 𝒊𝒊𝒊𝒊 = Gi2 = 192.0.2.1 ip dhcp-relay server 198.51.100.2 設定しない限り、送信インタフェースのアドレスを使う 𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉𝒉 router, relay_srcaddr, 𝒊𝒊𝒊𝒊 = Gi2 = 203.0.113.1 17

NEC IXの場合 1) クライアントのDHCPDISCOVERがR1でリレーされる 2) R1のGi1から送信されたパケットはR2のGi1に届く 3) リレーされたパケットがR2のACLで遮断される 𝑇𝑇𝑅𝑅𝑅 ℎ, 𝑝𝑝 = 𝑅𝑅 ℎ, 𝑖𝑖𝑖𝑖_𝑠𝑠𝑠𝑠𝑠𝑠 = 203.0.113.1, 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑 = 198.51.100.0, ⋯ , Gi1 � 𝑅𝑅 ℎ, 𝑖𝑖𝑖𝑖_𝑠𝑠𝑠𝑠𝑠𝑠 = 192.0.2.1, 𝑖𝑖𝑖𝑖_𝑑𝑑𝑑𝑑𝑑𝑑 = 𝑑𝑑𝑑𝑑𝑑𝑑𝑑_𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦𝑦 ℎ , ⋯ , Gi2 ⋮ DHCP DISCOVER src: 0.0.0.0:68 dst: 255.255.255.255:67 proto: 17(udp) giaddr: 0.0.0.0 𝑻𝑻𝑹𝑹𝑹𝑹 (𝒉𝒉, 𝒑𝒑) DHCP DISCOVER src: 203.0.113.1:67 dst: 198.51.100.0:67 proto: 17(udp) giaddr: 192.0.2.1 𝑖𝑖𝑖𝑖 𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵 ∧ 𝑝𝑝 = Gi2 𝑖𝑖𝑖𝑖 𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵𝐵 ∧ 𝑝𝑝 = Gi1 R2のACLにより 𝑻𝑻𝑹𝑹𝟐𝟐 (𝒉𝒉, 𝒑𝒑) 破棄される 18

まとめ 本研究の貢献 • • ネットワーク機器におけるステートレスな制御のための処理を関数として表現し既存の ネットワーク検証手法であるHSAで考慮できるようにする手法を提案 提案手法をDHCP relayに実際に適用し、これらの処理も考慮して ネットワーク検証ができるようになることを示した 今後の課題 • • • 提案手法により複雑なネットワークでも検証できることを実際に示す 他のステートレスなネットワーク制御のための処理への提案手法の適用 自然言語で記述された仕様から関数の形への変換の支援 19