KLEE を試してみた。

シンボリック実行のツールとして公開されているKLEEを試してみました。

目次

dockerのインストール

KLEEの環境を構築するのはdockerのイメージを使うのが一番手軽に試せるようです。
dockerについてはこちらの記事を参考にインストールしてみました。
qiita.com

dockerイメージの実行

dockerのインストールが完了したらイメージを取得して実行します。

# イメージの取得

$ docker pull klee/klee

$ docker image ls

REPOSITORY          TAG                 IMAGE ID            CREATED             SIZE

klee/klee           latest              f0052ebadb00        7 months ago        1.31GB
# 実行

$ docker run --rm -ti --ulimit='stack=-1:-1' klee/klee
# dockerのコンテナを起動するとシェルが立ち上がります。

klee@684a74481856:~$ pwd                                                                                 

/home/klee

klee@684a74481856:~$ ls

klee_build  klee_src

チュートリアル

KLEEの最初のチュートリアルがこちらのサイトで解説されています。
klee.github.io

シンボリック実行を試すコードは以下のようなコードとして示されています。
引数で渡された数値の符号を判定する関数のようです。

/*
 * First KLEE tutorial: testing a small function
 */

#include <klee/klee.h>

int get_sign(int x) {
  if (x == 0)
     return 0;
  
  if (x < 0)
     return -1;
  else 
     return 1;
} 

int main() {
  int a;
  klee_make_symbolic(&a, sizeof(a), "a");
  return get_sign(a);
} 

チュートリアル自体は丁寧に解説が書かれていますのでここでは詳細は書きませんが、注意点として、上記のコンテナのシェル上では、 klee/klee.hは klee_src/include に展開されています。
従って get_sign.c を /home/klee 以下で配置した場合にビットコードにコンパイルするコマンドは

$ clang -I klee_src/include -emit-llvm -c -g get_sign.c

になります。

感想

dockerを普段使うことがないのでとまどいました(というかまだよくわかっていないのでもう少しdockerに対する勉強が必要そうです。
今回は以前に買って積本になっていたdocker教科書第2版が役に立ちました。

プログラマのためのDocker教科書 第2版 インフラの基礎知識&コードによる環境構築の自動化

KLEE本体がちゃちゃっとmakeして使えないのは不便な気もしますが、dockerで配布しているということはmacやwindowsでも使えるということですよね。KLEEをwindowsでも使えないか試してみたいと思います。

Dockerエキスパート養成読本［活用の基礎と実践ノウハウ満載！］ (Software Design plus)

xrdpをインストールしてLinuxマシンにリモートデスクトップで接続する。

xrdpをインストールしたときのメモ。OSはLinux Mint を使っていますがUbuntu系であれば恐らく同じだと思います。

$ sudo apt install xrdp vnc4server
$ sudo vi /etc/xrdp/xrdp.ini

# crypt_levelを crypt_level=high に設定
# サービスを再起動

sudo service xrdp restart

インストールとサービスが起動できればあとはリモートデスクトップで接続できます。

C言語の関数の戻り値を実行時に変更する

「試験をしているんだけど、実行中に関数の戻り値を変える方法はないかな？」

と相談を受けました。

C言語で単体テストをする場合、システムコールやライブラリ関数はダミーの関数を用意しておいて自作部分の実装をテストすることはよくありますが、実行中にこのダミー関数の振舞いを変えたいという趣旨です。*1

単純にダミー関数の戻り値をグローバル変数にしてしまえば問題はありません。
ただしテストコードが多いと呼び出し元のテストコードが少し複雑になりそうです。

少し考えてみましたが、

DLL,共有ライブラリならできるのでは？

というのが私の思いついた答えでした。

linuxだとdlopen,dlsym,dlcloseを使って、ダミー関数を共有ライブラリにしておけば実際に呼び出される関数を変更することができます。

ということでそれっぽいコードを書いてみました。

試してみたコード

呼び出し元のソースコード(main.c)

#include <stdio.h>
#include <dlfcn.h>
#include <unistd.h>

int add(int a, int b)
{
    int result;
    void *handle_a = dlopen("./liba.so", RTLD_LAZY);
    int(* add_handler)(int, int) = dlsym( handle_a, __FUNCTION__ );

    result = add_handler(a, b);

    dlclose(handle_a);
    return result;
}

int main(int argc, char **argv)
{
    int result = 0;

    while(1)
    {
        result = add(1,2);
        sleep(1);
        printf("%d\n", result);
    }

    return 0;
}

ダミー関数の実装(add.c)

int add(int a, int b)
{
	return a + b;
}

ビルドと実行

$ gcc -shared add.c -o libadd.so

$ gcc  main.c -ldl

$ ./a.out

$ 3

$ 3

$ 3

$ 3

....(1秒間隔で出力される)

共有ライブラリのaddが呼び出されてadd(1,2)の結果が正しく(1+2=3)出力されていることは分かります。

さてここからが本番です。
add.cの中身を

int add(int a, int b)
{
	return a * b;
}

のように書き換えてコンパイルしてみましょう。
この時、先ほど実行した a.out は停止せず動かしっぱなしにします。

別ターミナルで、

$ gcc -shared add.c -o libadd.so 

すると、実行している a.outの出力はどうなるでしょうか。

3

3

3

3

2

2

2

2

2に変わっています！
ということで実行中に関数の戻り値を変える事ができました。

わざわざ共有ライブラリを動的にロードするのはまどろっこしい気もしますが規模が大きいテストではこちらの手法の方が保守性が高い気もします。

補足

呼び出し側で sleep(1)を呼び出している箇所がありますが、最初sleep無しで試したところセグメンテーションフォルトで a.out は止まってしまいました。
add.cをコンパイルすることによってロードしているライブラリのファイルに対して競合してしまったんだ思います。
sleep(1)を入れて試した限りでは問題なく動作がしましたが、きちんと排他制御を行うのは正しい姿だと思います。

JITコンパイルについて

rubyでも 2.6 からJITコンパイルが取り入れられたそうですが、今回試した実行時にライブラリを差し替えるのはアプローチとしては同じようなイメージになるかと思います。今回のadd関数は1行で終わるシンプルな関数なので面白くありませんが、これが処理時間のかかる関数だったとして実行中に処理時間のかからない関数に差し替える事ができれば嬉しいですよね。実行中のデータなどで関数の処理にフィードバックをかけて最適な処理にしていくといったこともできます。
*2

感想

同じような事は以前にも試してみていたのですが、単体テストなんかで使えるテクニックだとは気づいていませんでした。

mcommit.hatenadiary.com

この手のテクニックはどの言語でも何かしら手段が提供されていると思います。
私の知っている範囲ではC言語ですと、BINARY HACKS、RubyですとメタプログラミングRubyでそういったテクニックが解説されています。

Binary Hacks ―ハッカー秘伝のテクニック100選

メタプログラミングRuby 第2版

メタプログラミング.Netという本もあるんですね。面白そうなので読んでみたいと思います。

メタプログラミング.NET (アスキー書籍)

動的に何かを変更するのってなんかかっこよくて面白いですね。

*1:正常系のケースを実行した後そのまま異常系を試験したいというような状況ですね

*2:人工知能系のプログラミングもこういった形で実装できそうですね。

社長失格を読んだ

最近社長失格という本を読みました。だいぶ前にも読んだことがある本だったのですが、久しぶりに読んだら面白かったので読書録を書いておきたいと思います。

読みたくなった理由

実は私が、この本を読むのは2回目になります。最初にこの本を読んだのは2013年頃だったと思います。当時、会社を辞めて個人事業主になったばかりで、起業や経営に関する本を読み漁っていました。この「社長失格」のほかに「不格好経営」、「今から君が社長をしなさい」など読んでました。

久しぶりに読みたくなった理由ですが、twitterで「平成ネット史」というハッシュタグのついたツイートがTLに沢山流れてきていて、
その中にハイパーネット社と夏野剛さんとに関するツイートを見つけて、この本のことを思い出し、懐かしさのせいか急に本書を読みたくなりました。
初めて読んだときはブックオフの中古で買ったような気がしますが、Kindle版が出版されており、すぐに読みたいという気持ちも強くてポチってしまいました。

面白かったところ

この本は板倉さんの体験談ですので基本的にノンフィクションの自伝ということになると思うのですが、物語として非常にわかりやすい筋書きになっていて、
前半はダイアルQ2やインターネットを使った画期的なアイデアで順風満帆に会社に板倉さんの会社が成長していく様子がかかれています。
そしてビルゲイツにあってビジネスを賞賛されるところをピークとして、後半はビジネスモデルの弱点に気付いた銀行団に見切りをつけられ融資の返済に追われ転落していくというストーリーです。後半で、銀行の人が貸したお金を取り立てに来た時の様子などは読んでいて怖くなってくるものがありました。

多少の脚色などはあるのかも知れませんが、恐らく記憶を頼りに当時の様子を臨場感あふれる文体で書かれていて引き込まれるものがありページをめくる手が止まりませんでした。

感想

日本人は社会的弱者に厳しいというイメージがありますが、著者の板倉さんのように何かで失敗した人に対しても接し方が厳しいのではないかと思いました。読んだ後で思いました。
「敗軍の兵はよく学ぶ」と言いますが失敗した人や組織に属していた人がその後に成功するというのはよくあるのではないでしょうか。本書で登場する夏野さんもハイパーネットを退職された後はドコモでi-modeの開発で活躍されたわけですし。

関係者で多少なり不快に思われる人はいるのかも知れませんが、過去を振り返って、失敗した原因などを分析し語るというのは失敗した人にしかできないことですし、ある意味ではその失敗というのは人々に語ることによってその人が世の中に提供できる資産であるように思います。ビジネスに限らずこの書籍のような失敗談を語るというスタイルのコンテンツは(失礼ですが)面白いし、得られるものも多いのではないのかと思いました。

社長失格

Ethernet2(DIX)のフレームについて

来年から仕事でお世話になるであろう方からネットワーク力についていろいろ質問されたけどネットワーク良く分かっていないので、勉強がてらCCNAの資格でも取ろうと思って真面目にネットワークについて勉強を始めることにしました。

ネットワーク強い人に「ネットワークってどれくらい分かります？」って煽られたので、L2～L4のプロトコルスタックを自作してやろうかと思ったけど、その人が期待しているのはciscoとかfortigateとか802.1QとかHAとその手の知識らしい。
ネットワーク詳しいってどういう状態を指すのか分かない。

— simotin (@simotin13) 2018年12月11日

そもそもTCPやUDPを扱うプログラミングは経験がありますし、FTPとかHTTPとかのサーバは実装したことがあって、あと他にもFA系のプロトコルは沢山実装したことがあるので少しはネットワークについては分かっているつもりだったのですがいざ勉強してみるとよくわかっていないことが多いことに気づかされました。

せっかく勉強しているので、調べたこととか備忘の為に書いてきたいと思います。

今回はレイヤー2。Ethernetフレームについてです。

Ethernetフレームの規格

Ethernetのフレームには、

• ethernetII(DIX) *1
• ethernet 802.3

の２つの規格が存在する。現在の主流はEthernet2の方。
ちょっと気になってRX63Nのハードウェアマニュアルを見てみたのですがイーサネットコントローラはIEEE802.3規格のフロー制御準拠とありました。PHYのチップは802.3準拠のチップが多いからでしょうか...

Ethernet2のフレームフォーマット。

フィールド	サイズ(byte)	内容
プリアンプル	8	7byteの間　0xAA(10101010)を送信　8byte目で　0xAB(10101011)を送信
送信先MACアドレス	6	フレームの送信先
送信元MACアドレス	6	フレームの送信元
タイプ	2	上位のプロトコルタイプ
データ	46-1500	送信データ
FCS	4	送信先MACアドレスからデータ部までのCRC
IFG	12	フレームの区切りを表す96bit分の無通信区間

受信データサイズについて

Ethernetは可変長のフレームであるにも関わらずデータ長をフィールドはありません。

じゃあフレームの区切りはどうやって識別するんだ？

と疑問が湧いたのですが、調べてみるとFCSの後に96bit分の無通信時間(IFG:Inter Frame Gap)が入ることでフレームの区切りを識別するようです。

ちなみにwiresharkでパケットを表示すると送信先MACアドレス～データまでは表示されますがプリアンプルとFCSは表示されません(もちろん無通信時間もですが)

どちらもレイヤ1で処理されているからだと思いますが、Ethernetのフレームに問題がある場合*2はトラブルシューティングができないですね。

タイプについて

2byteのタイプフィールドで、上位レイヤ(レイヤ3)で使用するタイプを指定します。
よく使われるIPv4は0x0800です。
PPPoEの仕様とかよく知らないですけどISPとの接続はPPPoEであることが多いと思うので実はお世話になっているプロトコルですね。

タイプの例

タイプ	プロトコル
0x0800	IPv4
0x0806	ARP
0x8100	IEEE802.1Q
0x86DD	IPv6
0x8863	PPPoE Discovery Stage
0x8864	PPPoE Session Stage

参考書籍

パラパラと読んでみましたが、Ethernetのレイヤ1、レイヤ2に関しては詳説 Ethernetでかなり詳しく書かれています。
IFGの話も付録に書かれていました。

詳説 イーサネット 第2版

次は802.1QとかL3スイッチについて勉強する予定。

*1:DIXはDEC,Intel,Xeroxの略

*2:例えばFCSが一致しない