ENSOFT の研究 · DARPA プログラム
ENSOFT による複数年にわたる DARPA サイバーセキュリティ研究プログラムには、DARPA APAC（Automated Program Analysis for Cybersecurity）と DARPA STAC（Space/Time Analysis for Cybersecurity）があります。
イベント駆動のコールバック、マルチスレッド、フレームワークライブラリにわたって悪意ある振る舞いが隠蔽される Android アプリケーションにおいて、新種のマルウェアを検出するプログラムです。本プログラムでは、Atlas 上の理解駆動型分析プラットフォーム、対話型の Android Security Toolbox、そして大規模ライブラリから簡潔な情報フローの要約をマイニングする FlowMiner を開発しました。フェーズ I では Blue チーム中で最高の成績を、フェーズ II では上位 3 位に入りました。
最終技術報告書 AFRL-RI-RS-TR-2015-186、2015年7月報告書を読む →
Java バイトコードにおけるアルゴリズム計算量とサイドチャネルの脆弱性を特定するプログラムです。アルゴリズム計算量攻撃は、小さな入力から実行パスを極端な時間やメモリの消費に追い込みます。サイドチャネル攻撃は、実行パス間のリソースの変動から秘密情報を推測します。本プログラムでは、ループと分岐のカタログ、射影制御グラフ、対象を絞った動的解析を組み合わせた RULER を開発し、7 回の DARPA チャレンジエンゲージメントに適用しました。
最終技術報告書 AFRL-RI-RS-TR-2019-232、2019年12月報告書を読む →
AFRL-RI-RS-TR-2015-186 · ADA621995
Atlas 上に構築された DARPA APAC の Android Security Toolbox を実演します。このツールボックスにより、Red チームの敵対的アプリケーションに対して、Android のソースと Java バイトコードにわたるヒューマン・イン・ザ・ループのマルウェア監査が可能になります。
Benjamin Holland, Tom Deering, Suresh Kothari, Jon Mathews, Nikhil Ranade10.1109/ICSE.2015.235
DARPA APAC プログラムのもとで開発された、理解駆動型でヒューマン・イン・ザ・ループのマルウェア検出手法を定式化します。この手法は、Red チームによる敵対的な Android マルウェアに対して、DoD および商用のモバイルマーケットプレイスを審査するためのものです。
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論文を読む →
完全に自動化された静的解析では誤検知が過剰になる、またはスケールしない、複雑で横断的なソフトウェア異常を診断し解決するための、対話的なヒューマン・イン・ザ・ループの推論手法を紹介します。
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
Simulink と SimDiff によるドメイン固有のグラフィカルモデリングと、Atlas によるプログラムグラフのクエリモデリングを組み合わせた、問題駆動型のモデリングカリキュラムを紹介します。2 イベントのグラフモデルを、オペレーティングシステムのメモリリーク、Linux カーネルのロックの対応付け、DARPA APAC における Android マルウェアの検出に適用します。
Suresh Kothari, Jeremías Sauceda論文を読む →
AFRL-RI-RS-TR-2019-232 · AD1088526
Java のソースとバイトコードにおけるアルゴリズム計算量脆弱性（ACV）を、ループの自動的な特徴付け、疑わしいループのフィルタリング、対話的な監査によって検出する、3 段階のヒューマン・オン・ザ・ループのツールスイート DISCOVER を紹介します。
Payas Awadhutkar, Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari10.1145/3338906.3341177
安全性またはセキュリティの特性に関連するプログラムの振る舞いを切り出すための数学的基礎を定義し、プログラム全体のパス列挙を避けてその射影を直接計算する射影制御グラフ（PCG）を導入します。Linux カーネルのロック検証と、Java バイトコードにおけるサイドチャネル脆弱性の対話的な検出で評価されています。
Ahmed Tamrawi, Suresh Kothari10.1016/j.scico.2018.04.003
高度なサイバーフィジカルマルウェア（Industroyer など）が、産業用制御システム、電気通信、ミッションクリティカルなソフトウェアにおいて、センサー駆動のトリガーとアプリケーション固有のペイロードをどのように悪用するかを検討し、振る舞いの爆発に対抗するための仮説駆動型のプログラム分析手法を概説します。
Suresh Kothari, Ganesh Ram Santhanam, Payas Awadhutkar, Benjamin Holland, Jon Mathews, Ahmed Tamrawi10.1007/978-3-319-97643-3_7
Atlas と XCSG 上に構築されたオンデマンドのドキュメント生成エンジンで、数百万行規模のコードベースから、制御フローグラフ、コールグラフ、データフローグラフを、課題とコミットの履歴とともに抽出します。Apache POI で実証され、データフローの射影によって文書化されていないパラメータ制約が明らかになり、これまで報告されていなかった欠陥が発見されました。
Ahmed Tamrawi, Sharwan Ram, Payas Awadhutkar, Benjamin Holland, Ganesh Ram Santhanam, Suresh Kothari10.1109/DYSDOC3.2018.00009
センサー駆動のトリガーとドメイン固有のペイロードによって従来のウイルスやトロイの木馬のシグネチャを回避する、高度なサイバーフィジカルマルウェアを特徴付け検証するために必要な、数学的基礎、プログラム分析手法、実世界のケーススタディをまとめます。
Suresh Kothari10.1145/3183440.3183459
射影制御グラフ（PCG）の抽象化を用いて、プログラムの全パスを列挙することなく関連する実行時の振る舞いを直接導出する、多言語対応の対話型プログラム理解・検証ツール COMB を紹介します。Linux カーネルの検証を含む C と Java のケーススタディで実証されています。
Benjamin Holland, Payas Awadhutkar, Suresh Kothari, Ahmed Tamrawi, Jon Mathews10.1145/3183440.3183476
正準的なサイドチャネルパターン、プログラム成果物のフィルター、パラメータ化されたグラフモデルを導入し、分析者が時間と空間におけるソフトウェアのサイドチャネル脆弱性（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論文を読む →
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
Android の複雑なセマンティクスを対話的に探索するための Android Malicious Flow Visualization Toolbox（AMFVT）を紹介し、77 本の高度な DARPA チャレンジ Android アプリケーションにおける監査の精度と効率を報告します。
Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari, Jon Mathews10.1109/VIZSEC.2017.8062197
ポインタ解析と型システムに基づくオブジェクト不変性解析を、Java 8 のソースとコンパイル済みバイトコードを対象に Atlas 上で再実装し、大規模な実アプリケーションでの精度とスケーラビリティを評価するための実験用ツールボックスと精度ベンチマークを導入します。
Benjamin Holland, Ganesh Ram Santhanam, Suresh Kothari10.1109/ICST.2017.55
パス依存解析におけるパスの指数的増加とパス実行可能性の複雑さを克服するため、射影制御グラフ（PCG）の抽象化を導入します。Linux カーネルの 3 つのバージョン（ロックインスタンス 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
Linux Driver Verification（LDV）ツールの実証的な監査を通じて、産業界で形式検証を導入する際の実務上の障壁を、検証結果のクロスチェック、認証用の証拠、IDE との統合に焦点を当てて検討します。
Suresh Kothari, Payas Awadhutkar, Ahmed Tamrawi10.1109/ISSREW.2016.9
動的束縛、関数ポインタ、非同期コールバックによって生じる不可視の制御フロー（ICF）を解決するための、Atlas 上での対話的な人間と機械の協働による手法を紹介し、Linux カーネルにおける複雑な同期のバグを発見します。
Suresh Kothari, Ahmed Tamrawi, Jon Mathews10.1109/ICPC.2016.7503727
従来の単独の形式検証と、扱いきれない検証問題に対して人間による照合のための簡潔な視覚的証拠を生成する、人間と機械の協働のフレームワークとを対比します。
Suresh Kothari, Ahmed Tamrawi, Jon Mathews10.1145/2889160.2891046
証拠に基づく協働検証（EECV）と Atlas 上の L-SAP ツールを紹介します。インスタンス検証キット（IVK）を生成し、Linux カーネルの 3 つのバージョン（37 MLOC）にわたる 66,609 件のロックインスタンスを検証します。
Suresh Kothari, Ahmed Tamrawi, Jeremías Sauceda, Jon Mathews10.1145/2889160.2889192
学術的なプログラム分析とモデリングの研究を、アビオニクス、自動車システム、NASA の Orion 宇宙船プログラム、DARPA APAC および STAC のサイバーセキュリティ施策で運用される産業用ツールへと展開してきた 20 年の歩みをたどります。
Suresh C. Kothari10.1145/2897022.2897032