ENSOFT の研究 · 検証
ENSOFT の研究は、3,700 万行、66,609 件のロックインスタンスという規模で Linux カーネルを検証し、認証用の証拠のスキーマ、不可視の制御フローの解決、コンパイラの等価性、人間と機械の協働を開発しています。
もともと米国国防総省（DoD）向けに開発されたソフトウェアの検証と理解の技術を応用し、厳しいリアルタイム性能と小さなメモリフットプリントの制約下で動作するレガシーな自動車ソフトウェアおよび組込みソフトウェアのサイバーセキュリティ脆弱性を検出します。
Payas Awadhutkar, Ahmed Tamrawi, Jeremías Sauceda10.4271/2025-01-8088
eXtensible Common Software Graph（XCSG）を導入します。XCSG は、単独の自動化ではスケールしない検証問題において、人間と機械の協働のために設計された意味論的グラフ表現およびクエリ言語です。XCSG 上に構築された検証ツールは、3,700 万行のコードにわたる安全性とセキュリティの特性の監査に使用され、確認済みのバグを 8 件発見しました。
Jon Mathews, Theodore Murdock, Jeremías Sauceda, Ahmed Tamrawi, Suresh Kothari論文を読む →
SymPy 上に構築され Atlas に統合された非可換環であるパス代数を導入し、パスを列挙することなく実行時の振る舞いの「ソフトな無限」を表現します。実行パスは変数の積、分岐は和、ループは除算としてモデル化され、ループ本体は一度だけ表現されます。これにより、C、C++、Java、Simulink、バイトコード、バイナリにわたって、スケーラブルで透明な検証と脆弱性分析が可能になります。
Suresh Kothari論文を読む →
この手法は、コンパイラの正しさを抽象的に証明しようとするのではなく、監査対象の特定のプログラムについて、コンパイル済みバイナリの制御フローがソースと一致していることを検証します。等価性は、意味を保存する変換の後にCFG の同型性を確認することで確立され、アビオニクス、自動車、医療ソフトウェアにおける手作業でのクロスチェックとツール認定に適した証拠を生成します。
Payas Awadhutkar, Ahmed Tamrawi, Ryan Goluch, Suresh Kothari10.1016/j.cose.2022.102608
数学的解析をソースレベルのソフトウェアの振る舞いに直接結び付ける、簡潔で監査可能な視覚的証明を伝えるソフトウェア認証用の証拠のスキーマを示します。これにより、安全性とセキュリティが重要な認証において人間による照合が可能になります。
Suresh Kothari, Payas Awadhutkar, Ahmed Tamrawi論文を読む →
安全性またはセキュリティの特性に関連するプログラムの振る舞いを切り出すための数学的基礎を定義し、プログラム全体のパス列挙を避けてその射影を直接計算する射影制御グラフ（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
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
ポインタ解析と型システムに基づくオブジェクト不変性解析を、Java 8 のソースとコンパイル済みバイトコードを対象に Atlas 上で再実装し、大規模な実アプリケーションでの精度とスケーラビリティを評価するための実験用ツールボックスと精度ベンチマークを導入します。
Benjamin Holland, Ganesh Ram Santhanam, Suresh Kothari10.1109/ICST.2017.55
動的束縛、関数ポインタ、非同期コールバックによって生じる不可視の制御フロー（ICF）を解決するための、Atlas 上での対話的な人間と機械の協働による手法を紹介し、Linux カーネルにおける複雑な同期のバグを発見します。
Suresh Kothari, Ahmed Tamrawi, Jon Mathews10.1109/ICPC.2016.7503727
Linux Driver Verification（LDV）ツールの実証的な監査を通じて、産業界で形式検証を導入する際の実務上の障壁を、検証結果のクロスチェック、認証用の証拠、IDE との統合に焦点を当てて検討します。
Suresh Kothari, Payas Awadhutkar, Ahmed Tamrawi10.1109/ISSREW.2016.9
証拠に基づく協働検証（EECV）と Atlas 上の L-SAP ツールを紹介します。インスタンス検証キット（IVK）を生成し、Linux カーネルの 3 つのバージョン（37 MLOC）にわたる 66,609 件のロックインスタンスを検証します。
Suresh Kothari, Ahmed Tamrawi, Jeremías Sauceda, Jon Mathews10.1145/2889160.2889192
従来の単独の形式検証と、扱いきれない検証問題に対して人間による照合のための簡潔な視覚的証拠を生成する、人間と機械の協働のフレームワークとを対比します。
Suresh Kothari, Ahmed Tamrawi, Jon Mathews10.1145/2889160.2891046
学術的なプログラム分析とモデリングの研究を、アビオニクス、自動車システム、NASA の Orion 宇宙船プログラム、DARPA APAC および STAC のサイバーセキュリティ施策で運用される産業用ツールへと展開してきた 20 年の歩みをたどります。
Suresh C. Kothari10.1145/2897022.2897032
パス依存解析におけるパスの指数的増加とパス実行可能性の複雑さを克服するため、射影制御グラフ（PCG）という抽象化を導入します。3 つのバージョンの Linux カーネル（66,609 件のロックインスタンス）で制御フローグラフ（CFG）から PCG への縮約を評価し、Linux Driver Verification（LDV）ツールが見逃した同期のバグを明らかにしています。
Ahmed Tamrawi, Suresh Kothari10.1109/APSEC.2016.026
完全に自動化された静的解析では誤検知が過剰になる、またはスケールしない、複雑で横断的なソフトウェア異常を診断し解決するための、対話的なヒューマン・イン・ザ・ループの推論手法を紹介します。
Suresh Kothari, Akshay Deepak, Ahmed Tamrawi, Benjamin Holland, Sandeep Krishnan10.1109/SMC.2014.6974210
プログラムのインデックス作成をドメイン固有の分析から切り離す、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論文を読む →
ENSOFT のグラフベースの検証手法の原点を振り返ります。Linux カーネルにおけるネットワークスタックとポインタ参照外しの横断的なバグの追跡から、1,000 を超える mutex_lock と mutex_unlock の呼び出し箇所の体系的な検証へと至った経緯です。
Suresh Kothari, Jeremías Sauceda論文を読む →