形式手法を使って、 発見しにくいバグを一網打尽にしよう

builderscon tokyo 2019で話したときに使った資料です。
YouTube: https://www.youtube.com/watch?v=D7GccAn6R94

[2020/04/17追記]
この資料をさらにブラッシュアップした資料を公開しました。
この資料よりも次の資料をご覧いただくことをおすすめします。
https://www.slideshare.net/dena_tech/dena-techcon-2020-230372486

Transcript

1. 形式手法を使って、
 発見しにくいバグを一網打尽にしよう
 1 Aug 30, builderscon tokyo 2019 鈴木 穂高 | Hodaka Suzuki システム本部品質統括部SWETグループ DeNA Co., Ltd.
2. 自己紹介 • 鈴木 穂高（すずき ほだか） • 経歴 − 2014年DeNA新卒入社 − 2014年8月〜 大規模アプリゲーム開発 − 2018年10月〜 SWET − Androidテストチーム − テストの普及のための活動 − Game Testing Revolution（GTR）チーム − 仕様品質を向上させるための技術的なアプローチ研究 2
3. 自己紹介 • 鈴木 穂高（すずき ほだか） • 経歴 − 2014年DeNA新卒入社 − 2014年8月〜 大規模アプリゲーム開発 − 2018年10月〜 SWET − Androidテストチーム − テストの普及のための活動 − Game Testing Revolution（GTR）チーム − 仕様品質を向上させるための技術的なアプローチ研究 3
4. お話すること • 動機 • 形式手法とは • 私が考える適用可能性 4 Main CFP: https://builderscon.io/builderscon/tokyo/2019/session/e14fce7f-7ccc-42e5-b240-062e8719fa83
5. 動機 5
6. 動機 6 ゲーム開発をしているときに多かった 仕様の不備（考慮漏れ、記載漏れ、矛盾など）に 開発フェーズの早い段階で気づきたい。
7. 7 一般的な開発フロー 企画 実装 QA リリース 仕様作成 仕様不備の発見が後になればなるほど、 修正を伴う手戻り工数は大きくなる傾向がある。 小 大 手戻り工数
8. 8 開発チームも、レビュー、チェックリスト運用などで 対応していたが、技術的なアプローチで何かできないか 探していたところ、形式手法に出会った。
9. 形式手法とは 9
10. 形式手法 仕様を明確に記述したり、記述された設計の性質を機 械的に検証する手法の総称。 形式手法にもいくつか種類があるが、 いずれも数学に基づく科学的な裏付けを持つ。 登場は古く、1970年代頃から。 10
11. 形式手法にも種類が色々ある 11 種類 説明 代表的な記述言語 形式仕様記述 矛盾がなく論理的に正しい仕様を作 成する VDM++/Event-B/ Z/Alloy etc. モデル検査 プログラムの状態をモデル化すること で、プログラムが期待される性質を満 たすことを検証する Promela/TLA+ etc. 他もありますが、今回は割愛。
12. 簡単に言うと、こんなことができる 日本語の仕様書や、プログラムを 専用の記述言語で書き表し、ツールにかませると システマチックに不備を発見できる 12 形式手法
13. モデル検査の例 1. 検査したいもの（仕様書、ソースコードなど） から専用言語でモデルを作成する 2. 検査対象が満たすべき性質から検査式を作成する 3. モデル検査ツールにかける 13
14. byte n = 0; active proctype P() { n = 1; printf(“process P, n = %d\n”, n) } active proctype Q() { n = 2; printf(“process Q, n = %d\n”, n) } 14 「Spinモデル検査入門」より引用 ・・・① ・・・② ・・・③ ・・・④ モデル検査の例（Spin/Promela） 「異なるプロセスP, Qが、globalなnへの代入とprintを 実行する」をモデル化
15. byte n = 0; active proctype P() { n = 1; assert(n == 1); printf(“process P, n = %d\n”, n) } active proctype Q() { n = 2; printf(“process Q, n = %d\n”, n) } 15 モデル検査の例 assertを入れ、Spinの状態空間で成り立つことを 確認する
16. モデル検査の例 システムが取りうる状態・パスを自動で網羅的に 探索する 16 1 2 3 4 5 6 ① n = 1 ① n = 1 ① n = 1 ③ n = 2 ③ n = 2 ③ n = 2 ② printf(P) ③ n = 2 ③ n = 2 ④ printf(Q) ① n = 1 ① n = 1 ③ n = 2 ② printf(P) ④ printf(Q) ① n = 1 ④ printf(Q) ② printf(P) ④ printf(Q) ④ printf(Q) ② printf(P) ② printf(P) ② printf(P) ④ printf(Q)
17. $ spin -a -o2 sample.pml $ gcc -o pan pan.c $ ./pan -e pan:1: assertion violated (n==1) (at depth 4) pan: wrote sample.pml1.trail pan: wrote sample.pml2.trail ... 17 モデル検査の例 ツールをかませる
18. $ spin -a -o2 sample.pml $ gcc -o pan pan.c $ ./pan -e pan:1: assertion violated (n==1) (at depth 4) pan: wrote sample.pml1.trail pan: wrote sample.pml2.trail ... 18 モデル検査の例 assertionが満たされないパスが2つあることが わかる
19. $ spin -pglsr -t1 sample.pml using statement merging 1: proc 0 (P:1) sample.pml:4 (state 1) [n = 1] 2: proc 1 (Q:1) sample.pml:10 (state 1) [n = 2] process Q, n = 2 3: proc 1 (Q:1) sample.pml:11 (state 2) [printf('process Q, n = %d\\n',n)] 4: proc 1 terminates spin: sample.pml:5, Error: assertion violated spin: text of failed assertion: assert((n==1)) 5: proc 0 (P:1) sample.pml:5 (state 2) [assert((n==1))] spin: trail ends after 5 steps #processes: 1 n = 2 5: proc 0 (P:1) sample.pml:6 (state 3) 2 processes created 19 モデル検査の例 反例が出たときの計算の再構成に必要なデータ （trailファイル）をベースに再度シミュレーション
20. $ spin -pglsr -t1 sample.pml using statement merging 1: proc 0 (P:1) sample.pml:4 (state 1) [n = 1] 2: proc 1 (Q:1) sample.pml:10 (state 1) [n = 2] process Q, n = 2 3: proc 1 (Q:1) sample.pml:11 (state 2) [printf('process Q, n = %d\\n',n)] 4: proc 1 terminates spin: sample.pml:5, Error: assertion violated spin: text of failed assertion: assert((n==1)) 5: proc 0 (P:1) sample.pml:5 (state 2) [assert((n==1))] spin: trail ends after 5 steps #processes: 1 n = 2 5: proc 0 (P:1) sample.pml:6 (state 3) 2 processes created 20 1つ目の反例
21. $ spin -pglsr -t2 sample.pml using statement merging 1: proc 0 (P:1) sample.pml:4 (state 1) [n = 1] 2: proc 1 (Q:1) sample.pml:10 (state 1) [n = 2] spin: sample.pml:5, Error: assertion violated spin: text of failed assertion: assert((n==1)) 3: proc 0 (P:1) sample.pml:5 (state 2) [assert((n==1))] spin: trail ends after 3 steps #processes: 2 n = 2 3: proc 1 (Q:1) sample.pml:11 (state 2) 3: proc 0 (P:1) sample.pml:6 (state 3) 2 processes created 21 2つ目の反例
22. モデル検査の例 2つの反例が見つかった 22 1 2 3 4 5 6 ① n = 1 ① n = 1 ① n = 1 ③ n = 2 ③ n = 2 ③ n = 2 ② printf(P) ③ n = 2 ③ n = 2 ④ printf(Q) ① n = 1 ① n = 1 ③ n = 2 ② printf(P) ④ printf(Q) ① n = 1 ④ printf(Q) ② printf(P) ④ printf(Q) ④ printf(Q) ② printf(P) ② printf(P) ② printf(P) ④ printf(Q) assert(n==1)
23. さきほどのは至極簡単なモデル検査の例だが、 形式手法を適用して品質向上につながったという事例 は、欧米を中心に多く報告されている。 有名どころだと、AWSでも利用されている。 日本でもFelica等で利用されている。 23
24. 私のこれまでの道筋 • 形式手法についてキャッチアップ − 形式手法について調べてみた • プロダクトに適用できそうかPoCを作成して確認 − SWETグループが考える形式手法の現在とこれからの可能 性 24
25. よし、プロジェクト導入だ！ 25
26. とはならない！ 26
27. • うちの会社で使ったときの効果は？ • 学習コストは？ • 運用コストは？ • 人どれだけ雇う必要があるの？ • などなど 27 会社で導入するためには...
28. 私のこれまでの道筋 • 形式手法についてキャッチアップ − 形式手法について調べてみた • プロダクトに適用できそうかPoCを作成して確認 − SWETグループが考える形式手法の現在とこれからの可能 性 • 実際のプロダクトに適用して、会社として投資 できそうかを確かめる 28 Now
29. 私が考える適用可能性 29
30. 実際のプロダクトに適用する • 対象のプロダクト − Oyakata − DeNAで現在内製開発している、ゲームに特化した マスターデータの編集・管理ツール − https://genom.dena.com/event/20190327_study/ 30
31. やったこと • 形式仕様記述とモデル検査を適用 − 適用中に記録すること − どれくらいの不備が見つかったのか − 不備のインパクトはどれほどか − その他、かかった時間、感想など 31
32. 32 フェーズとしては、αテストの最中 SWET Oyakata dev Team • エンジニアOnlyで構成 • プロダクト要求仕様書（ PRD）も エンジニアが記述 ゲーム Team フィードバック プロダクト提供 PRDに対して形式仕様記述 コードに対してモデル検査 Oyakata含めた開発体制
33. 改めて目的 33 • 投資判断材料を集める − 「Oyakataチームに貢献」よりも、まずは技術を もっと知る
34. 形式仕様記述 34
35. 形式仕様記述 • 既存でいくつかあるプロダクト要求仕様書 （PRD）を書き起こす − Alloy 4.2 − http://alloytools.org − 「関係」を使って空間や時間の構造を表現する 35
36. 例 • 各ユーザーはロールを持つ • ロールには、「一般」と「Admin」がある ※説明のため実際の仕様書に記載されていた内容を改変しています 36
37. 例 • 各ユーザーはロールを持つ • ロールには、「一般」と「Admin」がある 37 User Role
38. 例 38 • 各ユーザーはロールを持つ • ロールには、「一般」と「Admin」がある 集合で表現 User Role 一般 Admin 1ユーザーの 集まり
39. 例 39 関係を記述する • 各ユーザーはロールを持つ • ロールには、「一般」と「Admin」がある User Role
40. 例 40 • 各ユーザーはロールを持つ • ロールには、「一般」と「Admin」がある User Role
41. 例 41 • 各ユーザーはロールを持つ • ロールには、「一般」と「Admin」がある User Role
42. 例 42 • 各ユーザーはロールを持つ • ロールには、「一般」と「Admin」がある User Role
43. 例 43 色々な関係が考えられる • 各ユーザーはロールを持つ • ロールには、「一般」と「Admin」がある User Role
44. 例 44 • 各ユーザーはロールを持つ • ロールには、「一般」と「Admin」がある • 1人のメンバーは1つのロールが割り当てられる • 1つの役職を複数メンバーが担当することができる • AdminのみOyakata上から0人にすることは できない
45. 形式仕様記述 abstract sig Role {} one sig General, AD extends Role {} sig User {} sig Oyakata { role: User -> one Role, } 45
46. 形式仕様記述 abstract sig Role {} one sig General, AD extends Role {} sig UserId {} sig Oyakata { role: User -> one Role, } 46 sig : 要素（アトム）の集合を表す
47. 形式仕様記述 abstract sig Role {} one sig General, AD extends Role {} sig User {} sig Oser { role: UserId -> one Role, } 47 Role General Admin Admin要素1 General 要素1
48. 形式仕様記述 abstract sig Role {} one sig General, AD extends Role {} sig User {} sig User { role: UserId -> one Role, frozen: UserId -> one FreezeStatus } 48 User User 要素1 User 要素2 User 要素N ・・・
49. 形式仕様記述 abstract sig Role {} one sig General, AD extends Role {} sig UserId {} sig Oyakata { role: User -> one Role, } 49 User Role Admin General
50. 形式仕様記述 abstract sig Role {} one sig General, AD extends Role {} sig UserId {} sig Oyakata { role: User -> one Role, } 50 User Role Admin Oyakata role General 関係を表す
51. 形式仕様記述 続き fact AtLeastAdmin { // 「Adminの役職をOyakata上から // 0人にすることはできない」を不変条件としてセット all o: Oyakata | AD in User.(o.role) } 51
52. 形式仕様記述（実際の仕様） • Adminは次のことができる − ユーザーの凍結 − 凍結したユーザーではログインできなくなる − 情報表示の不整合が起こるので、ユーザー削除はできな い 52
53. 形式仕様記述 abstract sig FreezeStatus {} one sig Frozen, NotFrozen extends FreezeStatus {} abstract sig Role {} one sig General, AD extends Role {} sig User {} sig Oyakata { role: User -> one Role, frozen: User -> one FreezeStatus } 53
54. 形式仕様記述 abstract sig FreezeStatus {} one sig Frozen, NotFrozen extends FreezeStatus {} abstract sig Role {} one sig General, AD extends Role {} sig UserId {} sig User { role: UserId -> one Role, frozen: UserId -> one FreezeStatus } 54 FreezeStatus Frozen NotFrozen Frozen要素1 NotFrozen要素1
55. 形式仕様記述 abstract sig FreezeStatus {} one sig Frozen, NotFrozen extends FreezeStatus {} abstract sig Role {} one sig General, AD extends Role {} sig UserId {} sig Oyakata { role: User -> one Role, frozen: User -> one FreezeStatus } 55 User FreezeStatus NotFrozen Frozen
56. 形式仕様記述 abstract sig FreezeStatus {} one sig Frozen, NotFrozen extends FreezeStatus {} abstract sig Role {} one sig General, AD extends Role {} sig UserId {} sig Oyakata { role: User -> one Role, frozen: User -> one FreezeStatus } 56 User FreezeStatus NotFrozen Oyakata frozen Frozen
57. 形式仕様記述 続き pred freeze(o, o': Oyakata, u: User) { o'.role = o.role (u -> NotFrozen) in o.frozen o'.frozen = o.frozen ++ (u -> Frozen) } 57 形式仕様記述
58. 形式仕様記述 続き pred freeze(u, u': User, uid: UserId) { u'.role = u.role (uid -> NotFrozen) in u.frozen u'.frozen = u.frozen ++ (uid -> Frozen) } 58 形式仕様記述 User FreezeStatus Oyakata o o’ NotFrozen Frozen frozen
59. 形式仕様記述 続き pred freeze(u, u': User, uid: UserId) { u'.role = u.role (uid -> NotFrozen) in u.frozen u'.frozen = u.frozen ++ (uid -> Frozen) } 59 形式仕様記述 User FreezeStatus Oyakata o o’ NotFrozen Frozen frozen
60. 形式仕様記述 続き pred freeze(u, u': User, uid: UserId) { u'.role = u.role (uid -> NotFrozen) in u.frozen u'.frozen = u.frozen ++ (uid -> Frozen) } 60 形式仕様記述 User FreezeStatus Oyakata o o’ NotFrozen Frozen frozen
61. 形式仕様記述 続き run freeze for 3 but exactly 2 Oyakata 61 形式仕様記述
62. 結果（いくつかあるうちの1つを表示） 62 freeze前 o
63. 結果（いくつかあるうちの1つを表示） 63 freeze前 freeze後 o o’
64. 結果（いくつかあるうちの1つを表示） 64 「全管理者が凍結状態」という状態が浮かび上がる freeze前 freeze後 o o’
65. • テーブルの仕組み • ブランチの仕組み • スキーマの仕組み • など... 65 こんな形で他のPRDも形式仕様記述で書く
66. 結果 PRD15枚読み、13の不備を指摘。 うち、重要度が高いものは3件。 66
67. やってみてわかったこと • 自然言語で書かれている仕様にバグはほとんどな かった − 書かれていない仕様にバグが集中している • モデリングに苦戦することが多い • 結果を見て気付くパターンよりも、形式仕様記述を書 いている最中に仕様の不備に気づくパターンの方が 多い − 一応これも形式仕様記述で言われている効果ではある 67
68. やってみてわかったこと 68 • Alloyの文法自体がチェックリストになっている − Alloyでは関係を厳密に定義していく必要がある − 日本語の仕様に曖昧な部分があれば、Alloyで 書き起こすことを通して気づくことができる • 結論ありきなモデリングになってしまうことが多々 • αテストのフェーズで形式仕様記述を 適用するのはやはり遅い • 仕様をインクリメンタルで書いていく形が向いている気 がした
69. 今後検討していくこと • 運用を見越すと、チームとして仕様の変更に 強くなれるかどうか • 今の記述の仕方に問題がある可能性がないか − 実践経験のある人に勘所を教えてもらう必要がある • Alloyよりももっと適切なツールがあるかどうか 69
70. モデル検査 70
71. モデル検査 • Oyakataのプログラムで、考慮漏れが発生しそうな 部分を見つけ、モデル検査を適用してみる − Spin Version 6.4.8 − http://spinroot.com/spin/whatispin.html 71
72. モデル検査対象 • Oyakataではnomsを使っている − https://github.com/attic-labs/noms − nomsを簡単に説明すると、 「バージョン管理ができるデータベース」 − Go言語で書かれている • nomsに対してモデル検査を適用する − nomsの実装を読み、それをうまいことモデリング していく 72
73. nomsをモデリングしてみた結果...「挫折」 • 原因 − Promelaの表現力不足 − 高階関数を扱えない Promela で高階関数が多用された コードを表現するのが大変 − nomsの設計がモデル検査に向いていない − 直感的でない抽象をもつので、簡易的なモデル作成の決 断を下せない − モデル対象の関数が5つ6つほどスタックを積むので モデル化の範囲が広すぎる 73
74. 方針転換 • GoのプログラムをPromelaに機械的に 変換できないか − 将来的に自動生成みたいなことが できれば、モデリングのコストも減る 74
75. Go -> Promela変換の手引き書の作成 75 func Example() { // do something } 例1: 関数宣言（Go）
76. Go -> Promela変換の手引き書の作成 76 proctype Example() { bool panic = false // do something _panic: panic = true goto _defer _return: _defer: // NOTE: 関数の終了を明示する。シミュレーションランの際に // panic したのかどうかをわかりやすくするために // printf を入れている。 end: printf("Example: panic=%d\n", panic) } 例1: 関数宣言（Promela）
77. Go -> Promela変換の手引き書の作成 77 func Example() { // do something panic(err) } 例2: panic関数（Go）
78. Go -> Promela変換の手引き書の作成 例2: panic関数（Promela） 78 proctype Example() { bool panic = false // do something // NOTE: panic は goto を使う。defer もちゃんと実行される。 goto _panic _panic: panic = true goto _defer _return: _defer: end: printf("Example: panic=%d\n", panic) }
79. Goでよくあるバグを検出してみる • Understanding Real-World Concurrency Bugs in Go − https://songlh.github.io/paper/go-study.pdf 79
80. Goでよくあるバグを検出してみる wg := &sync.WaitGroup{} wg.Add(5) for i := 0; i < 5; i++ { go func() { defer wg.Done() }() wg.Wait() } 80 Understanding Real-World Concurrency Bugs in Go
81. Goでよくあるバグを検出してみる wg := &sync.WaitGroup{} wg.Add(5) for i := 0; i < 5; i++ { go func() { defer wg.Done() }() wg.Wait() } 81 Understanding Real-World Concurrency Bugs in Go Waitでブロックしてしまうので、本来はforの外に出さないといけない
82. 手続きに従って変換をかける 82 Promelaコードが長いので略
83. 検査をしてみる $ spin -a -o2 ./main.pml $ gcc -DREACH -o ./pan ./pan.c $ ./pan -c0 -e pan:1: invalid end state (at depth 17) pan: wrote main.pml1.trail （以降略） 83
84. 検査をしてみる % spin -t1 main.pml S →E spin: trail ends after 18 steps #processes: 2 rwmutexMaxReaders = 16384 _prev_golang_chan = -1 _golang_chans[0].closed = 0 （中略） _golang_chans[9].closed = 0 group.count = 2 18: proc 1 (main:1) ./../../promela-go/golang.pml:309 (state 19) 18: proc 0 (:init::1) main.pml:65 (state 5) <valid end state> 3 processes created 84
85. 検査をしてみる 309| inline sync_WaitGroup_Wait(wg) { 310| wg.count == 0 311| } 85 WaitGroup.Wait から帰ってこない状況がありうることがわかる
86. やってみてわかったこと 86 • 大きなプログラムをモデリングするのは難しい − プログラムを表現の幅と、モデリング言語の表現の幅が違う ため • モデリング自体は難しいが、 ライブラリとして提供するという手法は 継続してやっていく価値はありそう
87. 今後検討していくこと 87 • モデル検査の利用法 − 設計が正しいかどうかを確認する − こちらは個人利用にとどまる予感 − 書いたプログラムを（部分的に）静的解析する − プロジェクトで運用することを見据えるならば こちらができると嬉しい • Promelaよりももっと適切なツールがあるかどうか
88. まとめ 88 • 形式仕様記述/モデル検査を、運用込みで プロダクトに適用できるかどうかを見定めている • まだまだ道半ば