ENSOFT の研究 · サイバーセキュリティ
ENSOFT のサイバーセキュリティ研究は、アルゴリズム計算量とサイドチャネルの脆弱性を検出し、ディープファジングのためにループの終了パターンをカタログ化し、サイバーフィジカルおよび Android のマルウェアを分析します。あわせて、レガシーシステムとセーフティクリティカルシステムのためのバイナリ修復にも取り組んでいます。
レガシーな航空宇宙システムや組込みシステムでは、ソースコードやビルド環境が失われているために再コンパイルできないことが多く、一方で従来のトランポリン方式ではバイナリが肥大化します。本研究は、バイナリ成果物と参照関係をモデル化するグラフ中間表現を導入し、最小限のインプレースパッチを計算します。PowerPC で実証し、4 バイトの機能修正に必要なパッチは、再アセンブルなしで合計 139 バイトです。
Payas Awadhutkar, Ahmed Tamrawi, Jeremías SaucedaIEEE/AIAA DASC 2026 · Best of Session
ソース変更がバイナリレベルに及ぼす影響を正確に計算し、実行ファイル全体を再生成するのではなく、局所的なバイト単位のパッチを生成するバイナリ書き換え手法を示します。再コンパイルすれば数千バイトが変わる変更をわずか数バイトで表すため、OTA の帯域を削減し、認証済みの航空宇宙および自動車ソフトウェアへの影響を最小限に抑えます。
Payas Awadhutkar, Jeremías Sauceda, Ahmed Tamrawi10.4271/2026-01-0088
もともと米国国防総省（DoD）向けに開発されたソフトウェアの検証と理解の技術を応用し、厳しいリアルタイム性能と小さなメモリフットプリントの制約下で動作するレガシーな自動車ソフトウェアおよび組込みソフトウェアのサイバーセキュリティ脆弱性を検出します。
Payas Awadhutkar, Ahmed Tamrawi, Jeremías Sauceda10.4271/2025-01-8088
SymPy 上に構築され Atlas に統合された非可換環であるパス代数を導入し、パスを列挙することなく実行時の振る舞いの「ソフトな無限」を表現します。実行パスは変数の積、分岐は和、ループは除算としてモデル化され、ループ本体は一度だけ表現されます。これにより、C、C++、Java、Simulink、バイトコード、バイナリにわたって、スケーラブルで透明な検証と脆弱性分析が可能になります。
Suresh Kothari論文を読む →
一般的なループ終了パターンの経験的なカタログに基づく、後方探索型のファジング手法を導入します。ループを通常の分岐と同様に扱うと、従来のファザーはカバレッジ 15〜20% 前後で行き詰まります。そうする代わりに、パターンを考慮したループ要約により、テスト生成が複雑なループを通り抜け、深い制御フローの状態に到達できるようにします。
Jeremías Sauceda, Payas Awadhutkar, Tim Fraser論文を読む →
Java のソースコードとバイトコードにおけるアルゴリズム計算量の脆弱性（ACV）を、ループの自動特性評価、疑わしいループのフィルタリング、対話的な監査によって検出する、3 段階のヒューマン・オン・ザ・ループ型ツールスイート DISCOVER を示します。
Payas Awadhutkar, Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari10.1145/3338906.3341177
高度なサイバーフィジカルマルウェア（Industroyer など）が、産業制御システム、電気通信、ミッションクリティカルなソフトウェアにおいて、センサー駆動のトリガーとアプリケーション固有のペイロードをどのように悪用するかを検討し、振る舞いの爆発に対抗するための仮説駆動型のプログラム分析技術を概説します。
Suresh Kothari, Ganesh Ram Santhanam, Payas Awadhutkar, Benjamin Holland, Jon Mathews, Ahmed Tamrawi10.1007/978-3-319-97643-3_7
センサー駆動のトリガーとドメイン固有のペイロードによって従来のウイルスやトロイの木馬のシグネチャを回避する高度なサイバーフィジカルマルウェアを特徴付け、検証するために必要な数学的基礎、プログラム分析技術、実世界のケーススタディを総合的にまとめます。
Suresh Kothari10.1145/3183440.3183459
安全性またはセキュリティの特性に関連するプログラムの振る舞いを切り出すための数学的基礎を定義し、その射影を直接計算する射影制御グラフ（PCG）を導入することで、プログラム全体のパス列挙を回避します。Linux カーネルのロック検証と、Java バイトコードにおけるサイドチャネル脆弱性の対話的な検出で評価しています。
Ahmed Tamrawi, Suresh Kothari10.1016/j.scico.2018.04.003
標準的なサイドチャネルパターン、プログラム成果物のフィルター、パラメーター化されたグラフモデルを導入し、分析者が時間と空間に関するソフトウェアのサイドチャネル脆弱性（SSCV）の仮説を立てて検証できるようにします。
Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari, Nikhil Ranade10.1007/978-3-319-72598-7_13
アルゴリズム計算量の脆弱性を含む可能性が高い複雑なループを絞り込むためのループ抽象化と振る舞いパターンを定義し、4 つのオープンソースライブラリと 18 の DARPA STAC チャレンジアプリケーションに含まれる 5,000 以上のループで評価しています。
Payas Awadhutkar, Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari論文を読む →
Android の複雑なセマンティクスを対話的に探索するための Android Malicious Flow Visualization Toolbox（AMFVT）を示し、高度な DARPA チャレンジの Android アプリケーション 77 本における監査の正確さと効率を報告します。
Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari, Jon Mathews10.1109/VIZSEC.2017.8062197
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
パス依存解析におけるパスの指数的増加とパス実行可能性の複雑さを克服するため、射影制御グラフ（PCG）という抽象化を導入します。3 つのバージョンの Linux カーネル（66,609 件のロックインスタンス）で制御フローグラフ（CFG）から PCG への縮約を評価し、Linux Driver Verification（LDV）ツールが見逃した同期のバグを明らかにしています。
Ahmed Tamrawi, Suresh Kothari10.1109/APSEC.2016.026
Atlas 上の静的なグラフ探索で候補となるループを切り出し、選択したループをさまざまな入力で評価する的を絞った動的解析と組み合わせることで、過剰な空間・時間の消費を引き起こして確認します。
Benjamin Holland, Ganesh Ram Santhanam, Payas Awadhutkar, Suresh Kothari10.1109/SCAM.2016.23
学術的なプログラム分析とモデリングの研究を、アビオニクス、自動車システム、NASA の Orion 宇宙船プログラム、DARPA APAC および STAC のサイバーセキュリティ施策で運用される産業用ツールへと展開してきた 20 年の歩みをたどります。
Suresh C. Kothari10.1145/2897022.2897032
Atlas 上に構築された DARPA APAC の Android セキュリティツールボックスを実演します。このツールボックスにより、レッドチームの敵対的アプリケーションに対して、Android のソースコードと Java バイトコードにわたるヒューマン・イン・ザ・ループのマルウェア監査が可能になります。
Benjamin Holland, Tom Deering, Suresh Kothari, Jon Mathews, Nikhil Ranade10.1109/ICSE.2015.235
DoD および商用のモバイルマーケットプレイスを、レッドチームによる敵対的な Android マルウェアから守るための審査を目的として DARPA APAC プログラムで開発された、理解駆動型でヒューマン・イン・ザ・ループのマルウェア検出手法を定式化します。
Suresh Kothari, Tom Deering, Ben Holland, Ahmed Tamrawi, Akshay Deepak, Sandeep Krishnan, Damanjit Singh, Vani Bojja, Ganesh Santhanam, Jeremías Sauceda, Jon Mathews, Nikhil Ranade論文を読む →
安全でないスレッド同期、メモリリーク、スマートフォンからのデータ流出などのソフトウェア脆弱性を、制御フローパス上のイベントノードの順序付きの出現としてモデル化し、脆弱性に関連する順序を保存しながら指数的な CFGを縮約する、サイズ削減のグラフ変換を定義します。
Akshay Deepak, Ahmed Tamrawi, Suresh Kothari論文を読む →