SymNetというネットワーク検証システムがあります。 このSymNetを手元で動かしたのでそのメモを残します。
SymNet 概要
シンボリック実行を用いてネットワークのdata planeを検証するシステムです。 似た手法としてHeader Space Analysisがありますが、SymNetはより強力です。
ネットワーク機器における処理はSEFLというシンボリック実行に適した言語で記述します。 ネットワーク機器における各処理についてSEFLを記述し、それらを Click Modular Router のコンフィグファイルの形式で組み合わせることでネットワーク機器をモデル化します。 この各機器のモデルと、モデル同士の接続関係を記述したファイルを組み合わせてネットワーク全体を表現します。
あとはシンボリック実行によって、指定したポートに入力されたパケットがどのパスを通るか、そのパスを通るときのパケットはどういう条件を満たすべきなのか、を追跡して ネットワーク全体が意図通りに設計できているかどうかを検証します。
SymNetのコードは以下のリポジトリで公開されています。
構築
Dockerで構築するのが楽でした。 sbtのダウンロードURLが古くなっているため、まずはリポジトリにあるDockerfileを以下のように修正します。
RUN cd / && \ - wget https://dl.bintray.com/sbt/native-packages/sbt/0.13.9/sbt-0.13.9.tgz && \ - tar xf sbt-0.13.9.tgz && \ + wget https://github.com/sbt/sbt/releases/download/v0.13.18/sbt-0.13.18.tgz && \ + tar xf sbt-0.13.18.tgz && \ rm *.tgz && \ ln -s /sbt/bin/sbt /usr/local/bin/sbt
また、不足していたライブラリを追加します。
- RUN apk --no-cache add ca-certificates wget openssl bash && \ + RUN apk --no-cache add ca-certificates wget openssl bash libgomp gcompat && \
dockerコマンドのオプションを毎回書くのも面倒なので以下のようなdocker-compose.ymlを用意しました
services:
symnet:
build: .
image: johscheuer/symnet
container_name: symnet
volumes:
- .:/Symnet
サンプルコードを実行する場合は以下のようなコマンドを実行します。
--rm オプションを付けているので、コマンド終了時にコンテナが自動でお掃除されます。
docker compose run --rm symnet sbt sample
毎回これを書くのも面倒なので以下のようなMakefileを書きました。
run-%: @echo "run ${@:run-%=%}" @docker compose run --rm symnet sbt ${@:run-%=%}
これで
make run-sample
とかで実行できるようになります。 （参考：Makefile で第2引数を使う方法 #Makefile - Qiita）
