Infer入門

Transcript

1. Infer 入門 Kernel/VM探検隊@東京 No18 Riru Oda (@ri5255) 1
2. Inferとは 2
3. 具体例 3
4. 具体例 4
5. 目標 5 Inferの仕組みを理論から 完全に 理解する
6. Inferの理論的基礎 6 1. Incorrectness Separation Logic 2. Bi-abduction
7. 7 10分じゃムリ!
8. 目標 8 Inferの仕組みを理論から 完全に 理解する ほんのり
9. 理論的基礎: Incorrectness Separation Logic 9 𝑃 𝐶 𝜖: 𝑄 ∀𝜎𝑞 ∈ 𝑄. ∃𝜎𝑝 ∈ 𝑃. 𝜎𝑝 , 𝜎𝑞 ∈ 𝐶 𝜖 Qを満たす任意の状態は、Pを満たすある状態から プログラムCを実行することで到達可能
10. 理論的基礎: Incorrectness Separation Logic 10 𝑣 → 𝑎 ∗ 𝑎 → − 𝑝𝑢𝑠ℎ_𝑏𝑎𝑐𝑘 𝑣 𝑜𝑘: ∃𝑎′. 𝑣 → 𝑎′ ∗ 𝑎′ → − ∗ 𝑎 ↛ nondet()がtrueを返す実行パスのみを考えている
11. 理論的基礎: Incorrectness Separation Logic 特定の実行パスに注目(underapproximation) 𝐶 (𝑃) True positive False negative 11
12. 具体例 12 𝑣 → 𝑎 ∗ 𝑎 → − client(𝑣) 𝑒𝑟𝑟(11): ∃𝑎′. 𝑣 → 𝑎′ ∗ 𝑎′ →∗ 𝑎 ↛ Bug finding = 成り立つISL論理式の(自動)探索
13. 具体例 13 𝑣 → 𝑎 ∗ 𝑎 → − client(𝑣) 𝑒𝑟𝑟(11): ∃𝑎′. 𝑣 → 𝑎′ ∗ 𝑎′ →∗ 𝑎 ↛ Bug finding = 成り立つISL論理式の(自動)探索 どうやって?
14. 理論的基礎: Bi-Abduction 14 𝑝 ∗ 𝐹 ⊢ 𝑞 ∗ 𝑀 𝑝, 𝑞が与えられたとき、以下を満たすF, Mを推論する
15. 理論的基礎: Symbolic Execution 15 𝑝0 𝐶0[𝜖0 : 𝑞0 ]𝐶 → [𝑝]𝐶0 ; 𝐶[𝑞] 𝑝0 𝐶0 [𝜖0 : 𝑞0 ]からCを実行すると[𝑝]𝐶0 ; 𝐶[𝑞]が成り立つ 気持ち: • 現在の状態が𝑞0 • Cを実行するのに追加で必要な仮定を𝑝0 に足したのがp • Cの実行結果と𝑞0 の変化しない部分を足したのがq
16. 具体例 16 以下をBi-Abduction + Symbolic Executionで見つける 𝑣 → 𝑎 ∗ 𝑎 → − client(𝑣) 𝑒𝑟𝑟(11): ∃𝑎′. 𝑣 → 𝑎′ ∗ 𝑎′ →∗ 𝑎 ↛
17. 具体例 17 𝑒𝑚𝑝 s𝑘𝑖𝑝 𝑜𝑘: 𝑒𝑚𝑝 skipから開始
18. 具体例 18 𝑣 → 𝑢 ∗ 𝐹 ⊢ 𝑒𝑚𝑝 ∗ 𝑀を解いて、 𝐹 = 𝑒𝑚𝑝, 𝑴 = 𝒗 → 𝒖 𝑒𝑚𝑝 s𝑘𝑖𝑝 𝑜𝑘: 𝑒𝑚𝑝 x := [v] → 𝒗 → 𝒖 skip; x := [v] [𝑜𝑘: 𝑣 → 𝑢 ∗ 𝑥 = 𝑢]
19. 具体例 19 𝑣 → 𝑎 ∗ 𝑎 → 𝑤 ∗ 𝐹 ⊢ 𝑣 → 𝑢 ∗ 𝑥 = 𝑢 ∗ 𝑀を解いて、 𝐹 = 𝒙 = 𝒖 ∗ 𝒂 = 𝒖 , 𝑀 = 𝒖 → 𝒘 𝑣 → 𝑢 skip; x := [v] 𝑜𝑘: 𝑣 → 𝑢 ∗ 𝑥 = 𝑢 𝑝𝑢𝑠ℎ_𝑏𝑎𝑐𝑘(𝑣) → 𝑣 → 𝑢 ∗ 𝒖 → 𝒘 skip; x := [v]; push_back(v) 𝑜𝑘: 𝑣 → 𝑎′ ∗ 𝑎′ → 𝑤′ ∗ 𝑎 ↛∗ 𝒙 = 𝒖 ∗ 𝒂 = 𝒖 𝑣 → 𝑎 ∗ 𝑎 → 𝑤 𝑝𝑢𝑠ℎ_𝑏𝑎𝑐𝑘 𝑣 𝑜𝑘: ∃𝑎′. 𝑣 → 𝑎′ ∗ 𝑎′ → − ∗ 𝑎 ↛
20. 具体例 20 𝑣 → 𝑢 ∗ 𝑢 → 𝑤 skip; x := [v]; push_back(v); 𝑜𝑘: 𝑞11 𝑥 ≔ 88 → 𝑣 → 𝑢 ∗ 𝑢 → 𝑤 skip; x := [v]; push_back(v); [x] ≔ 88 𝑒𝑟𝑟 11 : 𝑞11 𝑞11 = (𝑣 → 𝑎′ ∗ 𝑎′ → 𝑤′ ∗ 𝑎 ↛∗ 𝑥 = 𝑢 ∗ 𝑎 = 𝑢)とすると、 𝑞11 ⊢ 𝑥 ↛ ∗ 𝑡𝑟𝑢𝑒だから
21. まとめ • Inferはプログラムの静的解析ツール • Incorrectness Separation LogicとBi-abductionが理論的基礎 • OpenSSLを約15分で解析できる[4] 21 実際にInferで発見されたメモリバグ: https://github.com/openssl/openssl/pull/15834
22. 参考文献 1. Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. 2001. Local Reasoning about Programs that Alter Data Structures. In Proceedings of the 15th International Workshop on Computer Science Logic (CSL '01). Springer-Verlag, Berlin, Heidelberg, 1–19. 2. Peter W. O'Hearn. 2012. A Primer on Separation Logic (and Automatic Program Verification and Analysis). In Software Safety and Security; Tools for Analysis and Verification. NATO Science for Peace and Security Series, vol 33, pp286-318, 2012. 3. Azalea Raad, Josh Berdine, Hoang-Hai Dang, Derek Dreyer, Peter O’Hearn, and Jules Villard. 2020. Local Reasoning About the Presence of Bugs: Incorrectness Separation Logic. In Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21–24, 2020, Proceedings, Part II. Springer-Verlag, Berlin, Heidelberg, 225–252. https://doi.org/10.1007/978-3-030-53291-8_14 4. Quang Loc Le, Azalea Raad, Jules Villard, Josh Berdine, Derek Dreyer, and Peter W. O'Hearn. 2022. Finding real bugs in big programs with incorrectness logic. Proc. ACM Program. Lang. 6, OOPSLA1, Article 81 (April 2022), 27 pages. https://doi.org/10.1145/3527325 5. Peter W. O'Hearn. 2019. Incorrectness logic. Proc. ACM Program. Lang. 4, POPL, Article 10 (January 2020), 32 pages. https://doi.org/10.1145/3371078 6. Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. 2007. Footprint analysis: a shape analysis that discovers preconditions. In Proceedings of the 14th international conference on Static Analysis (SAS'07). Springer-Verlag, Berlin, Heidelberg, 402–418. 7. Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2011. Compositional Shape Analysis by Means of Bi- Abduction. J. ACM 58, 6, Article 26 (December 2011), 66 pages. https://doi.org/10.1145/2049697.2049700 22
23. 参考文献 8. Kwangkeun Yi and Xavier Rival. 2020. Introduction to static Analysis: An Abstract Interpretation Perspective. MIT Press. 9. J. Villard. 2025. Build your own scalable static analysis with the Infer Platform. Presented at VeTSS Summer School ’23, June 27, 2025. YouTube video. Retrieved August 8, 2025 from https://www.youtube.com/watch?v=6A9w8tX-rMg 23
24. 文献案内 • Separation Logicが知りたい⇒ 1, 2 (特に2がおすすめ) • Incorrectness Separation Logicが知りたい⇒ 3, 4, 5 • Bi-abductionが知りたい⇒ 6, 7 • Static Analyzerを作ってみたい⇒ 8, 9 (特に9がおすすめ) 24