ENSOFT の研究 · バイナリとコンパイラ
ENSOFT のバイナリとコンパイラの研究は、最小限のインプレースのバイナリマイクロパッチ、制御フロー等価性によるコンパイルの健全性、セーフティクリティカルシステムのためのバイナリ脆弱性分析を対象としています。
レガシーな航空宇宙システムや組込みシステムでは、ソースコードやビルド環境が失われているために再コンパイルが不可能なことが多く、一方で従来のトランポリン方式はバイナリを肥大化させます。本研究では、バイナリ成果物と参照関係をモデル化して最小限のインプレースパッチを算出するグラフ中間表現を導入します。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論文を読む →
この手法は、コンパイラの正しさを抽象的に証明しようとするのではなく、監査対象の特定のプログラムについて、コンパイル済みバイナリの制御フローがソースと一致していることを検証します。等価性は、意味を保存する変換の後にCFG の同型性を確認することで確立され、アビオニクス、自動車、医療ソフトウェアにおける手作業でのクロスチェックとツール認定に適した証拠を生成します。
Payas Awadhutkar, Ahmed Tamrawi, Ryan Goluch, Suresh Kothari10.1016/j.cose.2022.102608