ENSOFT の研究 · 代数とグラフ
パス代数は、実行の振る舞いを非可換環としてモデル化します。そこでは積、和、因数分解が、パス、分岐、ループを表します。eXtensible Common Software Graph（XCSG）、射影制御グラフ（PCG）、イベントフローグラフ（EFG）はその振る舞いの準同型な射影であり、すべてのパスを列挙することなく Atlas プラットフォーム上でクエリできます。
グラフ問題のための代数的フレームワークを、Dijkstra 法や Bellman–Ford 法などの探索アルゴリズムに代わる手法として、最短経路問題で実証します。パスの区間を代数式としてモデル化し、負のエッジ重みや負の閉路を持つグラフを含めて、反復的な状態更新ではなく方程式の求解と因数分解によって最短経路を導出します。また、明示的なグラフ探索が手に負えなくなる「全パス」問題についても検討します。
Suresh C. Kothari, Payas Awadhutkar論文を読む →
SymPy 上に構築され Atlas に統合された非可換環であるパス代数を導入し、パスを列挙することなく実行時の振る舞いの「ソフトな無限」を表現します。実行パスは変数の積、分岐は和、ループは除算としてモデル化され、ループ本体は一度だけ表現されます。これにより、C、C++、Java、Simulink、バイトコード、バイナリにわたって、スケーラブルで透明な検証と脆弱性分析が可能になります。
Suresh Kothari論文を読む →
eXtensible Common Software Graph（XCSG）を導入します。XCSG は、単独の自動化ではスケールしない検証問題において、人間と機械の協働のために設計された意味論的グラフ表現およびクエリ言語です。XCSG 上に構築された検証ツールは、3,700 万行のコードにわたる安全性とセキュリティの特性の監査に使用され、確認済みのバグを 8 件発見しました。
Jon Mathews, Theodore Murdock, Jeremías Sauceda, Ahmed Tamrawi, Suresh Kothari論文を読む →
安全性またはセキュリティの特性に関連するプログラムの振る舞いを切り出すための数学的基礎を定義し、プログラム全体のパス列挙を避けてその射影を直接計算する射影制御グラフ（PCG）を導入します。Linux カーネルのロック検証と、Java バイトコードにおけるサイドチャネル脆弱性の対話的な検出で評価されています。
Ahmed Tamrawi, Suresh Kothari10.1016/j.scico.2018.04.003
射影制御グラフ（PCG）の抽象化を用いて、プログラムの全パスを列挙することなく関連する実行時の振る舞いを直接導出する、多言語対応の対話型プログラム理解・検証ツール COMB を紹介します。Linux カーネルの検証を含む C と Java のケーススタディで実証されています。
Benjamin Holland, Payas Awadhutkar, Suresh Kothari, Ahmed Tamrawi, Jon Mathews10.1145/3183440.3183476
Atlas と XCSG 上に構築されたオンデマンドのドキュメント生成エンジンで、数百万行規模のコードベースから、制御フローグラフ、コールグラフ、データフローグラフを、課題とコミットの履歴とともに抽出します。Apache POI で実証され、データフローの射影によって文書化されていないパラメータ制約が明らかになり、これまで報告されていなかった欠陥が発見されました。
Ahmed Tamrawi, Sharwan Ram, Payas Awadhutkar, Benjamin Holland, Ganesh Ram Santhanam, Suresh Kothari10.1109/DYSDOC3.2018.00009
パス依存解析におけるパスの指数的増加とパス実行可能性の複雑さを克服するため、射影制御グラフ（PCG）という抽象化を導入します。3 つのバージョンの Linux カーネル（66,609 件のロックインスタンス）で制御フローグラフ（CFG）から PCG への縮約を評価し、Linux Driver Verification（LDV）ツールが見逃した同期のバグを明らかにしています。
Ahmed Tamrawi, Suresh Kothari10.1109/APSEC.2016.026
プログラムのインデックス作成をドメイン固有の分析から切り離す、Atlas ソフトウェア分析プラットフォームを紹介します。多項式時間の静的解析器がプログラムの属性付きグラフデータベースを構築し、エンジニアはそれを対話的に、または分析スクリプトを通じてクエリします。Linux カーネルの同期検証と Android マルウェアの検出で検証されています。
Tom Deering, Suresh Kothari, Jeremías Sauceda, Jon Mathews10.1145/2591062.2591065
制御フローグラフのパスを、線形時間の変換によってイベントフローグラフ（EFG）へと写し、同値類に分割します。EFG は CFG から導かれる簡潔なグラフであり、そのパスは特性に関連するすべてのイベントトレースを保存します。Linux カーネル（v3.12）のスピンロックの安全な同期について評価し、パス数の多い CFG で 99% 近い削減を達成するとともに、統制実験によって人間にとっての理解しやすさを示しています。
Ahmed Tamrawi, Suresh Kothari論文を読む →
安全でないスレッド同期、メモリリーク、スマートフォンからのデータ流出などのソフトウェア脆弱性を、制御フローパス上のイベントノードの順序付きの出現としてモデル化し、脆弱性に関連する順序を保存しながら指数的な CFGを縮約する、サイズ削減のグラフ変換を定義します。
Akshay Deepak, Ahmed Tamrawi, Suresh Kothari論文を読む →