ENSOFT の研究
ENSOFT の研究では、複雑なソフトウェアの検証とセキュリティ確保のためのプログラム分析、グラフ表現、代数的手法を開発しています。対象は、オペレーティングシステムのカーネルやモバイルアプリケーションから、セーフティクリティカルな組込みシステムのコンパイル済みバイナリにまで及びます。
注目の論文
グラフ問題のための代数的フレームワークを、Dijkstra 法や Bellman–Ford 法などの探索アルゴリズムに代わる手法として、最短経路問題で実証します。パスの区間を代数式としてモデル化し、負のエッジ重みや負の閉路を持つグラフを含めて、反復的な状態更新ではなく方程式の求解と因数分解によって最短経路を導出します。また、明示的なグラフ探索が手に負えなくなる「全パス」問題についても検討します。
Suresh C. Kothari, Payas Awadhutkar論文を読む →
SymPy 上に構築され Atlas に統合された非可換環であるパス代数を導入し、パスを列挙することなく実行時の振る舞いの「ソフトな無限」を表現します。実行パスは変数の積、分岐は和、ループは除算としてモデル化され、ループ本体は一度だけ表現されます。これにより、C、C++、Java、Simulink、バイトコード、バイナリにわたって、スケーラブルで透明な検証と脆弱性分析が可能になります。
Suresh Kothari論文を読む →
レガシーな航空宇宙システムや組込みシステムでは、ソースコードやビルド環境が失われているために再コンパイルが不可能なことが多く、一方で従来のトランポリン方式はバイナリを肥大化させます。本研究では、バイナリ成果物と参照関係をモデル化して最小限のインプレースパッチを算出するグラフ中間表現を導入します。PowerPC で実証され、4 バイトの機能修正に必要なパッチは、再アセンブルなしで合計 139 バイトでした。
Payas Awadhutkar, Ahmed Tamrawi, Jeremías SaucedaIEEE/AIAA DASC 2026 · Best of Session
この手法は、コンパイラの正しさを抽象的に証明しようとするのではなく、監査対象の特定のプログラムについて、コンパイル済みバイナリの制御フローがソースと一致していることを検証します。等価性は、意味を保存する変換の後にCFG の同型性を確認することで確立され、アビオニクス、自動車、医療ソフトウェアにおける手作業でのクロスチェックとツール認定に適した証拠を生成します。
Payas Awadhutkar, Ahmed Tamrawi, Ryan Goluch, Suresh Kothari10.1016/j.cose.2022.102608
1,200 万行を超える Linux カーネルにわたる 66,609 件のロックインスタンスを対象とした、実証的な検証研究です。高水準の振る舞いモデルはインスタンスの 99.3% を検証し（形式検証ツール Linux Driver Verification では 65.7%）、従来の検証結果の欠陥を明らかにし、カーネル開発者によって確認・修正された 7 件の安全でないロックの欠陥を発見しました。
Suresh Kothari, Payas Awadhutkar, Ahmed Tamrawi, Jon Mathews10.1109/WSC.2017.8247886
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
Atlas と XCSG 上に構築されたオンデマンドのドキュメント生成エンジンで、数百万行規模のコードベースから、制御フローグラフ、コールグラフ、データフローグラフを、課題とコミットの履歴とともに抽出します。Apache POI で実証され、データフローの射影によって文書化されていないパラメータ制約が明らかになり、これまで報告されていなかった欠陥が発見されました。
Ahmed Tamrawi, Sharwan Ram, Payas Awadhutkar, Benjamin Holland, Ganesh Ram Santhanam, Suresh Kothari10.1109/DYSDOC3.2018.00009
プログラムのインデックス作成をドメイン固有の分析から切り離す、Atlas ソフトウェア分析プラットフォームを紹介します。多項式時間の静的解析器がプログラムの属性付きグラフデータベースを構築し、エンジニアはそれを対話的に、または分析スクリプトを通じてクエリします。Linux カーネルの同期検証と Android マルウェアの検出で検証されています。
Tom Deering, Suresh Kothari, Jeremías Sauceda, Jon Mathews10.1145/2591062.2591065