← DARPA STAC
第 8–11 節

発表論文と講演

RULER：ソフトウェア内のリソース使用の脆弱性を検出するシステム

目次

8. 発表論文と講演

8.1 学術誌論文

  1. Ahmed Tamrawi and Suresh Kothari, “Projected Control Graph for Computing Relevant Program Behaviors”, Science of Computer Programming Volume 163, Pages 93-114, October 2018.

8.2 書籍の章

  1. Suresh Kothari, Ganesh Ram Santhanam, Payas Awadhutkar, Benjamin Holland, Jon Mathews, and Ahmed Tamrawi, “Catastrophic Cyber Physical Malware,” Springer Verlag Publishers, October 2018, Pages 1-41.

8.3 査読付き会議論文

  1. Payas Awadhutkar, Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari, “DISCOVER: Detecting Algorithmic Complexity Vulnerabilities,” 27th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE).
  2. Derrick Lockwood, Benjamin Holland, Suresh Kothari, “MOCKINGBIRD: A Framework for Enabling Targeted Dynamic Analysis of Java Programs,” 41st International Conference on Software Engineering (ICSE 2018), Montreal, May 2019.
  3. Ahmed Tamrawi, Sharwan Ram, Payas Awadhutkar, Benjamin Holland, Ganesh Ram Santhanam, Suresh Kothari, “DySDoc3 – DynaDoc: Automated On-Demand Context-Specific Documentation,” 2018 DOCGEN Challenge Workshop at the IEEE International Conference on Software Maintenance Evolution (ICSME 2018), Madrid, Spain, September 25, 2018, (Best Tool Award).
  4. Suresh Kothari, “Demystifying Cyber-Physical Malware,” 40th International Conference on Software Engineering (ICSE 2018), Technical Briefing, Sweden, Gothenburg, May 27-June 3 2018.
  5. Benjamin Holland, Payas Awadhutkar, Suresh Kothari, Ahmed Tamrawi, Jon Mathews, “COMB: Computing Relevant Program Behaviors,” 40th International Conference on Software Engineering (ICSE 2018), Sweden, Gothenburg, May 27-June 3 2018.
  6. Ganesh Ram Santhanam, Ben Holland, Suresh Kothari, Nikhil Ranade, “Human-on-the-loop-automation for Detecting Software Side Channel Vulnerabilities,” 13th International Information Systems Security Conference (ICISS 2017), Bombay I.I.T., Springer LNCS 10717, pp. 209-230, December 2017.
  7. Payas Awadhutkar, Ganesh Ram Santhanam, Ben Holland, Suresh Kothari, “Intelligence Amplifying Loop Complexity Characterizations for Detecting Algorithmic Complexity Vulnerabilities,” the 24th Asia-Pacific Software Engineering Conference (APSEC), December 2017.
  8. Suresh Kothari, Payas Awadhutkar, Ahmed Tamrawi, Jon Mathews, “Modeling Lessons from Verifying Large Software Systems for Safety and Security,” Proceedings of the 2017 Winter Simulation Conference, November 2017.
  9. Ganesh Ram Santhanam*, Ben Holland, Jon Mathews, Suresh Kothari, “Interactive Visualization Toolbox to Detect Sophisticated Android Malware,” the 14th IEEE Symposium on Visualization for Cyber Security (VizSec), October 2017.
  10. Ben Holland, Ganesh Ram Santhanam, Suresh Kothari, “Transferring state-of-the-art immutability analyses: An experimentation toolbox and accuracy benchmark,” IEEE International Conference on Software Testing, Verification and Validation, Tokyo, Japan, March 2017.
  11. Ahmed Tamrawi, Suresh Kothari, “APSEC 2016 – Projected Control Graph for Accurate and Efficient Analysis of Safety and Security Vulnerabilities,” 23rd Asia-Pacific Software Engineering Conference, Hamilton, New Zealand, December 6-9, 2016. (Invited for journal publication)
  12. Benjamin Holland+, Ganesh Santhanam*, Payas Awadhutkar+, Suresh Kothari, “Statically-informed Dynamic Analysis Tools to Detect Algorithmic Complexity Vulnerabilities,” IEEE Source Code Analysis and Manipulation (SCAM) Conference, Raleigh, North Carolina, October 1-3, 2016.
  13. Ahmed Tamrawi, Payas Awadhutkar, Suresh Kothari, “Insights for Practicing Engineers from a Formal Verification Study of the Linux Kernel,” Formal Verification for Practicing Engineers Workshop, IEEE ISSRE 2016, Ottawa, Canada, October 23-27, 2016 (Invited for journal publication).
  14. Suresh Kothari, Ahmed Tamrawi, and Jon Mathews, “Human-Machine Resolution of Invisible Control Flow,” IEEE International Conference on Program Comprehension (ICPC 2016), pp. 226-229, May 15-16, Austin, Texas, May 15-16, 2016.
  15. Suresh Kothari, Ahmed Tamrawi, and Jon Mathews, “Refactoring Verification: Accuracy, Efficiency and Scalability through Human-Machine Collaboration,” A Technical Briefing Paper, IEEE International Conference on Software Engineering (ICSE 2016), Austin, Texas, May 15-19, 2016.
  16. Suresh Kothari, Ahmed Tamrawi, Jeremías Sauceda, and Jon Mathews, “Let’s Verify Linux: Accelerated Learning of Analytical Reasoning through Automation and Collaboration,” a Software Engineering Education Track (SEET) paper, IEEE International Conference on Software Engineering (ICSE 2016), Austin, Texas, May 15-19, 2016.
  17. Suresh Kothari, “Software Engineering Research Lab to Airplanes, Orion and Beyond,” a Software Engineering Research and Industry Practice (SER&IP) Workshop paper, IEEE International Conference on Software Engineering (ICSE 2016), Austin, Texas, May 15-19, 2016 (Best Paper Award).

8.4 Suresh Kothari による基調講演と招待講演

  1. “An 18th-century Mathematician, a $336 Million Patent, and Software Verifiability,” CyLab Distinguished Seminar Series at Carnegie Mellon University, April 2019.
  2. “An 18th-century Mathematician, a $336 Million Patent, and Software. Experimentation,” International Conference on Security and Privacy, Jaipur, India, January 11, 2019 (Keynote Talk).
  3. “An 18th-century Mathematician, a $336 Million Patent, and Software Experimentation,” Computer Science Department, University of British Columbia, October 2019.
  4. “Software Security Headaches: Analgesic or Hospital,” Security of Information and Networks (SIN 2017), Manipal University, Jaipur, India, October 14, 2017 (Keynote talk).
  5. “Reflections on Applying Mathematics to Solve Hard Software Problems,” University of Central Florida, August 29, 2017.
  6. “Demystifying Cybersecurity for CPS Community,” MathWorks Research Summit, Boston, June 4, 2017.
  7. “Euler, the 336 Million Dollar Software Patent: Reflecting on How to Solve Hard Software Problems,” ACSS2017, Patna, India, March 19, 2017.
  8. “Euler, the 336 Million Dollar Software Patent: Reflecting on How to Solve Hard Software Problems,” University of Auckland, Auckland, New Zealand, December 2, 2016.
  9. “Euler, the 336 Million Dollar Software Patent: Reflecting on How to Solve Hard Software Problems,” Auckland University of Technology, Auckland, New Zealand, December 1, 2016.
  10. “Euler, the 336 Million Dollar Software Patent: Reflecting on How to Solve Hard Software Problems,” Fraunhofer Institute, Baltimore, November 3, 2016.
  11. Insights for Practicing Engineers from a Formal Verification Study of the Linux Kernel,” Plenary Talk, Formal Verification for Practicing Engineers Workshop at ISSRE 2016, October 5, 2016 (Plenary Talk).
  12. Technical Briefing, International Conference on Software Engineering, Austin, May 17, 2016.
  13. “Rethinking Verification: Accuracy, Efficiency, and Scalability through Human-Machine Collaboration,” Georgia Institute of Technology, Atlanta, May 12, 2016.
  14. “Rethinking Malware Detection: Accuracy, Efficiency, and Scalability through Human-Machine Collaboration,” University of Maryland, Baltimore, February 17, 2016.
  15. “Program Analysis and Reasoning for Hard-to-Detect Software Vulnerabilities,” Jadavpur University, Kolkata, India, December 17, 2015.
  16. “Modeling Critical Software Systems for Cybersecurity and Safety,” Tata Research Design and Development Center (TRDDC), Pune, India, December 7, 2015.
  17. “Evidence-Enabled Collaborative Verification for Cybersecurity and Safety of Critical Software Systems,” Government of India Center for Development of Advanced Computing (CDAC), Pune, November 24, 2015.
  18. “Visual Models to Solve Hard Problems at the Intersection of Cybersecurity and Software Reliability,” Rockwell Collins Headquarters, Cedar Rapids, Iowa, October 22, 2015.

8.5 チュートリアルと短期講座

  1. Suresh Kothari, “Software Engineering and Cybersecurity,” short course at Indian Institute of Technology, Jammu, India, January 7-9, 2019.
  2. Suresh Kothari and Ben Holland, “Systematic Exploration of Critical Software for Catastrophic Cyber-Physical Malware,” MILCOM Tutorial, Baltimore, October 29, 2018.
  3. Suresh Kothari, “How Mathematics can save us from catastrophic cyber attacks,” ICISS Tutorial, Bombay I.I.T., India, December 17, 2017.
  4. Suresh Kothari, Ben Holland, “Learn to analyze and verify large software for cybersecurity and safety,” MILCOM Tutorial, Baltimore, October 25, 2017.
  5. Suresh Kothari, GIAN 2017 – Analytical Reasoning and Experiential Learning with Applications to Software Analysis, MNIT, Jaipur, India, October 9-15, 2017.
  6. Suresh Kothari, Workshop on Learn to Understand, Analyze, and Verify Large Software, National Institute of Technology, Patna, India, March 20-22, 2017.
  7. Suresh Kothari, Ben Holland, Discovering Information Leakage Using Visual Program Models, MILCOM 2016, Baltimore, November 2, 2016.
  8. Suresh Kothari, Jeremías Sauceda, Mission-Critical Software Assurance Engineering Beyond Testing, Bug Finders, Metrics, Reliability Analysis, and Formal Verification, ISSRE 2016, Ottawa, Canada, October 25, 2016.
  9. Suresh Kothari, Ben Holland, GIAN 2016 – Managing Complexity, Security, and Safety of Large Software, MNIT, Jaipur, India, September 12-16, 2016. (Sponsored by the Government of India).
  10. Suresh Kothari, Ben Holland, Learn to Build Automated Software Analysis Tools with Graph Paradigm and Interactive Visual Framework, ASE 2016, Singapore, September 4, 2016.
  11. Suresh Kothari, Ben Holland, Practical program analysis for discovering Android malware, The Premier International Conference for Military Communications (MILCOM 2015), Tampa, Florida, October 28, 2015. http://www.afcea.org/events/milcom/Tutorials/tutorials.pdf
  12. Suresh Kothari, Ben Holland, Hard problems at the intersection of cybersecurity and software reliability, International Symposium on Software Reliability Engineering (ISSRE 2015), NIST, Gaithersburg, Maryland, November 3, 2015.
  13. Suresh Kothari, Ben Holland, Computer-aided collaborative validation of large software, IEEE Automated Software Engineering Conference (ASE 2015), Lincoln, Nebraska, November 3, 2015. http://ase2015.unl.edu/#computer-aided-collaborative-validation-tutorial
  14. Suresh Kothari, Program Analysis and Reasoning for Hard to Detect Software Vulnerabilities, International Conference on Information Systems Security (ICISS 2015), Kolkata, India, December 17, 2015. http://www.iciss.org.in/iciss/tutorialsp.html

9. 参考文献

  1. Turing, Alan, “On computable numbers, with an application to the Entscheidungsproblem,” Proceedings of the London Mathematical Society, Vol. 2, no. 42, pp. 230-265, 1936.
  2. “Continuum hypothesis”, http://en.wikipedia.org/wiki/Continuum_hypothesis. Accessed October 18, 2019.
  3. “Gödel's incompleteness theorems”, https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems Accessed October 18, 2019.
  4. “Paul Cohen (mathematician),” http://en.wikipedia.org/wiki/Paul_Cohen_(mathematician). Accessed October 18, 2019.
  5. Wei, Tao, Jian Mao, Wei Zou, and Yu Chen. "A new algorithm for identifying loops in decompilation." In International Static Analysis Symposium, pp. 170-183. Springer, Berlin, Heidelberg, 2007.
  6. Ahmed Tamrawi and Suresh Kothari, “Projected Control Graph for Computing Relevant Program Behaviors”, Science of Computer Programming Vol. 163, Pages 93-114, October 2018.

10. 付録

10.1 Atlas プラットフォーム

RULER は Eclipse プラグインの集合として実装されており、それらは XCSG のリファレンス実装として Atlas を使用する。

Atlas は Soot を使用して、Java バイトコードの Jimple 中間表現を生成する。Jimple は、型付きの 3 番地コードであり、わずか 15 種類の命令だけを含む、バイトコードの簡略化された表現である。Soot と Jimple の詳細は、Soot の Sable ホームページで参照できる。

Atlas は Jimple を解析し、eXtensible Common Software Graph（XCSG）に準拠したプログラムグラフに取り込む。以下の説明は、ユーザーが使い始めるのを助けるための非常に簡単な概要であり、Jimple に関わる XCSG に焦点を当てる。

簡単に言えば、XCSG は、AST の情報と、制御フローとデータフローの保守的な近似を表現する。ほとんどのノードは Contains エッジを用いて字句的なネストに従って整理され、その部分グラフは木を形成する。可視化すると、Contains エッジはノードの中にネストしたノードとして表示される。

Contains エッジに沿って Method まで下る典型的なパスは、次の XCSG タグを持つノードを通る：Project -> Package -> Type -> Method。Field は、Type の下で Method の兄弟である。

可能な呼び出しは、Method 間の Call エッジで表現される。

ControlFlow_Node と DataFlow_Node は Method の下に埋め込まれる。すべての DataFlow_Node は、（Contains エッジによって）ControlFlow_Node の直下にある。Jimple 向けの XCSG では、ControlFlow_Node が TrapRegion の下に現れることがある。

ControlFlow_Node は ControlFlow_Edge で接続される。DataFlow_Node も同様に DataFlow_Edge で接続される。Operator は DataFlow_Node の下位の種類である。Atlas による変換では、各 Field は 1 つのノードで表現され、その結果、オブジェクト非依存の近似となる。RULER によってほかの近似が追加されることもある。

Smart Views を解釈するためのさらなる助けとして、「Element Detail View」を開く（Window -> Show View -> Other… を使用する）。Element Detail View は、選択したノードとエッジのタグと属性を、それがテキストエディタ内にあるかグラフ内にあるかにかかわらず表示する。Element Detail View のツールバーのボタンを使うと、現在の選択に関連する XCSG のタグ階層のグラフを表示できる。

XCSG の詳細は、XCSG の wiki ページで参照できる。

Atlas の API の詳細は、Atlas の wiki で参照できる。

本報告書の 2026 年の再公開にあたり、ENSOFT の現在のブランドに合わせるための軽微な変更と、内容に影響しないその他の軽微な更新を行った。

11. 記号、略語、頭字語の一覧

  • AC - アルゴリズム計算量
  • API - Application Programming Interface
  • CFG - 制御フローグラフ
  • CFR - Class File Reader
  • ExCFG - 例外的な制御フローを含む制御フローグラフ
  • IO - 入出力
  • IPCG - 手続き間の射影制御グラフ
  • JDK - Java Development Kit
  • LCG - ループコールグラフ
  • LTC - ループの終了条件
  • LTD - ループ終了依存グラフ
  • PCG - 射影制御グラフ
  • RULER - Resource Usage vuLnerability identifiER
  • SC - サイドチャネル
  • STRU - 時空間リソース使用
  • TDA - 対象を絞った動的解析
  • TDG - 終了依存グラフ
  • XCSG - eXtensible Common Software Graph