狠狠撸

2 /21
? InferはAIを使ってJava/C/C++/Objective-Cコー
ドのバグを検出するツールである。
? Inferに関する下記をまとめた資料です。
1. Inferの特徴
2. どんなバグが検出できるか
3. Inferの仕組み
4. 使ってみた感想
5. 環境構築【別紙】
C言語向け資料です。
公式URL
http://fbinfer.com/

3 /21
? もともとの開発元はFacebookが買収したMonoidics。
? 2015年にオープン化された。
? 現在は様々な企業で適用実績あり。
? Web系、モバイルアプリ系がメインユーザーっぽい。
? 人間の推論を擬似した数学的論理を使用してバグを見つ
ける。複数ファイルにまたがるバグも発見可能。
? 詳しい理論については後述。

5 /21
? Java
? Context leak
? Null dereference
? Resource leak
? C/C++/Objective-C
? Null dereference
? Memory leak
? Premature nil termination argument
? Resource leak
? C++
? Empty Vector Access
? Objective-C
? Ivar not null checked
? Parameter not null checked
? Retain cycle
2017/5時点。
まだロードマップの1%の時点にいるらしい。

6 /21
? サンプルコード
? 参考URL
? https://www.jpcert.or.jp/sc-rules/c-exp34-c.html
struct Person {
int age;
int height;
int weight;
};
int get_age(struct Person *who) {
return who->age;
}
int null_pointer_interproc() {
struct Person *joe = 0;
return get_age(joe);
}

7 /21
? mallocで確保したメモリが解放されていない場合に
報告される。
(void) memory_leak_bug {
struct Person *p = malloc(sizeof(struct Person));
}

8 /21
? リストで可変長引数を渡すときに終端していない場合
に報告される。
? strがnilの場合、期待通りのリストが作成されない。
NSArray *foo = [NSArray arrayWithObjects: @"aaa", str, @"bbb", nil];

9 /21
? File、Socket、Connection等のリソースの解放漏れ
を報告する。
(void) resource_leak_bug {
FILE *fp;
fp=fopen("c:test.txt", "r"); // file opened and not closed.
}

10 /2110
（参考URL）
http://fbinfer.com/docs/separation-logic-and-bi-abduction.html

11 /21
? 基本理論
? Hoare logic（ホーア論理）
? プログラムの正当性を推論するための形式論理の言語、体系。
? Abstract interpretation（抽象化解釈）
? プログラムのsemanticsを近似するための理論。
? 特徴的な理論
? Separation logic
? ホーア論理の拡張で、メモリ制御を表現/検証する論理体系。
? Bi-abduction
? Separation logicで推論/検証をするための一形態。
スケーラビリティに推論できるのが特徴。

12 /21
? 論理記号の導入
? A*B
? *は"and separately"という。
? ポインタA、Bが指すヒープが分離しているという意味。
?
? Heap#1はポインタxで指し、値はy。
? Heap#2はポインタyで指し、値はx。
? Heap#1、Heap#2は分離している。

13 /21
? プログラムの表現
? pre：前提条件、precondition
? prog：program part
? post：事後条件、post condition
? frame：フレーム、変化しない状態
? 例① closeするメソッド
? 例②r2がopenのまま

14 /21
? コードをpre/prog/postで表現することにより、変化
するメモリ(antiframe)と不変なメモリ（frame）を見つ
ける。
? このようにメモリ制御を表現/検証していく。
? 詳細はAbduction、Bi-Abductionの論文参照。
? Compositional Shape Analysis by Means of Bi-
Abduction, 2011, ACMの論文

16 /21
? よくバグが出るOpenSSLをチェックした結果。
? 主にNULL間接参照のバグが多く、修正内容はNULL
チェックの追加だった。
? 詳細：openssl-1.0.0a.html
バージョン検出したバグ
1.0.0a NULL_DEREFERENCE: 113
RESOURCE_LEAK: 1
1.0.0t NULL_DEREFERENCE: 102
RESOURCE_LEAK: 1
1.0.1 stable NULL_DEREFERENCE: 95
RESOURCE_LEAK: 1

17 /21
? バグ内容
arg->dataがNULLになる可能性がある。
apps/apps.c:394: error: NULL_DEREFERENCE
pointer `arg->data` last assigned on line 391 could be null and is dereferenced at line
394, column 3
391. arg->data=(char **)OPENSSL_malloc(sizeof(char *)*arg->count);
392. }
393. for (i=0; i<arg->count; i++)
394. > arg->data[i]=NULL; //arg->dataがNULLになる可能性がある。
395.
396. num=0;
? 修正内容
NULLチェック追加
if (arg->data == NULL)
return 0;

18 /21
? バグ内容
flagがNULLになる可能性がある。
ssl/d1_both.c:1164: error: NULL_DEREFERENCE
pointer `frag` last assigned on line 1162 could be null and is dereferenced at line 1164,
column 9
1162. frag = dtls1_hm_fragment_new(s->init_num, 0);
1163.
1164. > memcpy(frag->fragment, s->init_buf->data, s->init_num);
1165.
1166. if ( is_ccs)
? 修正内容
NULLチェック追加。
frag = dtls1_hm_fragment_new(s->init_num, 0);
if (!frag) return 0;
memcpy(frag->fragment, s->init_buf->data, s->init_num);

19 /21
? バグ内容
bufferがNULLになる可能性がある。
crypto/bio/b_print.c:718: error: NULL_DEREFERENCE
pointer `*buffer` last assigned on line 715 could be null and is dereferenced by call to
`memcpy()` at line 718, column 21
715. *buffer = OPENSSL_malloc(*maxlen);
716. if (*currlen > 0) {
717. assert(*sbuffer != NULL);
718. > memcpy(*buffer, *sbuffer, *currlen);
719. }
720. *sbuffer = NULL;
? 修正内容
*buffer = OPENSSL_malloc(*maxlen);
if (*buffer == NULL) return 0;

20 /21
? バグ内容
tmpがNULLになる可能性がある。
apps/ca.c:2782: error: NULL_DEREFERENCE
pointer `tmp` last assigned on line 2780 could be null and is dereferenced by call to
`strchr()` at line 2782, column 9
2780. tmp = BUF_strdup(str);
2781.
2782. > p = strchr(tmp, ',');
2783.
2784. rtime_str = tmp;
? 修正内容
if (!tmp) {
BIO_printf(bio_err, "memory allocation failuren");
goto err;
}

21 /21
? チェックはmakeするだけで簡単にできてよい。
? Clangのビルドに恐ろしく時間がかかった。6時間くらい。
低スペックPCの場合、Docker使うのが無難。
? チェック結果はチェック事例を増やして判断する必要が
あり、なんとも言えない状況。
? お試ししたいプロジェクト募集中！

狠狠撸

滨苍蹿别谤：人工知能を使った静的コードチェック

More Related Content

滨苍蹿别谤：人工知能を使った静的コードチェック