AC時間 · 空間
アルゴリズム計算量
比較的小さな入力で引き起こせる、時間計算量または空間計算量の高い実行パスです。コストは入力が制御するループから生じるため、解析はすべてのループについて、何がそのループを終わらせ、何がその上限を決め、何を呼び出し、外部からの入力が到達するかどうかを知る必要があります。
ENSOFT の研究 · DARPA STAC · 2015–2019
Space/Time Analysis for Cybersecurity
DARPA の STAC プログラムは、Java ソフトウェアが時間とメモリをどう使うかに潜む脆弱性を見つけることを目指しました。ループを極端なリソース消費に追い込む小さな入力や、秘密情報を漏らす実行時間やメモリ使用量の差です。完全に自動化された検出は、停止問題を解くことに等しくなります。チームの答えは RULER でした。RULER は、自動化された解析と人間の分析者を組み合わせる Atlas 上の知能増幅システムであり、7 回の DARPA エンゲージメントで試されました。
空間と時間の脆弱性
SC時間 · 空間
サイドチャネル
秘密情報に結びついた実行パスの集合であり、それらのパスに沿った実行時間やメモリ使用量の変動から、攻撃者が秘密情報を推測できるものです。これを見つけるには、秘密情報に依存するパスと、それぞれのパスのコストについて推論する必要があります。
DARPA I2O · AFRLSTAC の 2 つの軸
規模と速度
STAC は、進歩を 2 つの軸で測りました。規模とは、数十万行のネットワークサービスや、数百万行から数千万行のシステムを扱える解析のことです。速度とは、自動化ツールの助けを借りた人間の分析者が、そのコードを読み進める速さのことです。このプログラムは、米国の政府、軍、経済が依存するソフトウェアを対象としました。
数千 → 数百万1 時間あたりのコード行数：数千行から引き上げることをプログラムが目指した、分析者の速さです。
RULER
Resource Usage vuLnerability identifiERAtlas · Eclipse
知能増幅
RULER は Atlas 上の Eclipse プラグインの集合として動作し、作業を機械と分析者で分担します。自動化は、バイトコード内のすべてのループと分岐を特徴付け、疑わしいコードを指し示します。分析者は仮説を立て、関連する振る舞いだけを示すグラフでそれを検証し、問題のコードだけをファジングすることで確かめます。報告書は、この手法を Frederick Brooks の主張にちなんで位置付けています。知能増幅は AI に勝り、機械と心は、単独で動作する、心を模倣する機械に勝てるという主張です。
図 1 · RULER のシステムアーキテクチャエグゼクティブサマリー →
完全な自動化第 4–4.2 節
疑わしいプログラムセグメントの発見
カタログは、すべてのループについて 65 の属性を、すべての分岐について 44 の特性を記録し、Java 8 のラムダ式が形成するラムダループも記録します。射影制御グラフはメソッドのパスを AC と SC に関連する振る舞いにまとめ、テイント解析は外部からの入力が到達する箇所に印を付け、JDK のサブシステムのタグは各ループがどの API に触れるかを示します。
図 1–8 · 表 1読む →
ヒューマン・オン・ループの静的解析第 4.3 節
裏付けとなる証拠の収集
分析者は仮説を、16 のプロパティとスメルを備えたダッシュボード、選択したイベントにわたって手続き間の PCG を計算する PCG ビルダー、サブシステムを呼び出すループを残すビルダー、Jimple の横に並ぶデコンパイラビュー、フィルタービュー、18 の Smart Views で検証します。
図 9–13読む →
ヒューマン・オン・ループの動的解析第 4.4–5 節
対象を絞った動的解析
Mockingbird フレームワークは、Atlas の解析器で疑わしいコードを抽出し、その Object Mocker がテストハーネスを自動的に構築します。これにより、AFL ファザーが Kelinci を通じてそのコードだけをバイナリ入力で動かし、脆弱性がエクスプロイト可能かどうかを示します。この章は、時間と空間における AC と SC の問いに対する分析者のワークフローで締めくくられます。
Mockingbird · AFL · Kelinci読む →
RULER の内部
結果
7 回のエンゲージメント · 2016–2019第 6–7 節
エンゲージメントを通じた正答率
Blue チームは、ライブと持ち帰りの 7 回の DARPA エンゲージメントに取り組みました。チームの正答率はチャレンジアプリケーションのセットごとに上がり、E5 と E6 では 100% に達しました。E7 ではすべてのチームがすべての問いに答えることを求められ、正答率はわずかに下がりました。エンゲージメントは手法の弱点を明らかにし、一つひとつの改良の方向を示しました。プログラムマネージャーは、IA 技術を採用候補として推奨しました。
図 14 · エンゲージメントの成績読む →
AFRL-RI-RS-TR-2019-232 · AD1088526
最終報告書
- 1エグゼクティブサマリー
RULER の背景にある研究課題と、RULER が取り組むプログラム分析の課題の 5 つの分類です。
- 2–3はじめにと技術的アプローチ
チーム、DARPA 自身の言葉によるプログラムの目標、3 つの分析指針です。
- 4–4.2疑わしいプログラムセグメントの発見
アーキテクチャ、4 つのカタログ、ループコールグラフ、射影制御グラフ、テイント解析、サブシステムのタグ付けです。
- 4.3裏付けとなる証拠の収集
ダッシュボード、PCG ビルダーとループとサブシステムの相互作用ビルダー、デコンパイラビュー、フィルタービュー、Smart Views です。
- 4.4–5対象を絞った動的解析とチャレンジアプリケーション
Mockingbird フレームワークと、時間と空間における AC と SC に対する分析者のワークフローです。
- 6–7結果と結論
7 回のエンゲージメントと、プログラム分析に知能増幅を用いる論拠です。
- 8–11発表論文と講演
学術誌論文 1 本、書籍の章 1 本、会議論文 17 本、基調講演と招待講演 18 件、チュートリアル 14 件、参考文献、Atlas に関する付録、頭字語の一覧です。
概要: STAC プログラムにより、我々は大きな進歩を遂げることができた。最も重要な進歩は、AC 脆弱性と SC 脆弱性を検出するための知能増幅（IA）技術であると考えている。本報告書では、直面した課題と、我々がそれらにどのように対処したかを述べる。我々の成績は、手法の進歩とともに着実に向上した。我々は DARPA のチャレンジエンゲージメントで最高の成績を収めた。持ち帰りとオンサイトのエンゲージメントは、研究を推進するうえで非常に有用であった。エンゲージメントによって、我々は手法の弱点を特定でき、手法を洗練するための具体的な方向性を得た。
主な論文
ACM ESEC/FSE · 2019アルゴリズム計算量
DISCOVER: アルゴリズム計算量脆弱性の検出
Java のソースとバイトコードにおけるアルゴリズム計算量脆弱性（ACV）を、ループの自動的な特徴付け、疑わしいループのフィルタリング、対話的な監査によって検出する、3 段階のヒューマン・オン・ザ・ループのツールスイート DISCOVER を紹介します。
Payas Awadhutkar, Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari10.1145/3338906.3341177
Science of Computer Programming · 2018PCG のジャーナル論文
関連するプログラムの振る舞いを計算するための射影制御グラフ
安全性またはセキュリティの特性に関連するプログラムの振る舞いを切り出すための数学的基礎を定義し、プログラム全体のパス列挙を避けてその射影を直接計算する射影制御グラフ（PCG）を導入します。Linux カーネルのロック検証と、Java バイトコードにおけるサイドチャネル脆弱性の対話的な検出で評価されています。
Ahmed Tamrawi, Suresh Kothari10.1016/j.scico.2018.04.003
Springer · 2018ICS とサイバーフィジカルシステム
壊滅的なサイバーフィジカルマルウェア
高度なサイバーフィジカルマルウェア（Industroyer など）が、産業用制御システム、電気通信、ミッションクリティカルなソフトウェアにおいて、センサー駆動のトリガーとアプリケーション固有のペイロードをどのように悪用するかを検討し、振る舞いの爆発に対抗するための仮説駆動型のプログラム分析手法を概説します。
Suresh Kothari, Ganesh Ram Santhanam, Payas Awadhutkar, Benjamin Holland, Jon Mathews, Ahmed Tamrawi10.1007/978-3-319-97643-3_7
IEEE ICSME DOCGEN Challenge · 2018Best Tool Award
DynaDoc: オンデマンドで状況に応じたドキュメントの自動生成
Atlas と XCSG 上に構築されたオンデマンドのドキュメント生成エンジンで、数百万行規模のコードベースから、制御フローグラフ、コールグラフ、データフローグラフを、課題とコミットの履歴とともに抽出します。Apache POI で実証され、データフローの射影によって文書化されていないパラメータ制約が明らかになり、これまで報告されていなかった欠陥が発見されました。
Ahmed Tamrawi, Sharwan Ram, Payas Awadhutkar, Benjamin Holland, Ganesh Ram Santhanam, Suresh Kothari10.1109/DYSDOC3.2018.00009
ACM/IEEE ICSE Companion · 2018テクニカルブリーフィング
サイバーフィジカルマルウェアの解明
センサー駆動のトリガーとドメイン固有のペイロードによって従来のウイルスやトロイの木馬のシグネチャを回避する、高度なサイバーフィジカルマルウェアを特徴付け検証するために必要な、数学的基礎、プログラム分析手法、実世界のケーススタディをまとめます。
Suresh Kothari10.1145/3183440.3183459
ICSE · 2018PCG ツールボックス
COMB: 関連するプログラムの振る舞いの計算
射影制御グラフ（PCG）の抽象化を用いて、プログラムの全パスを列挙することなく関連する実行時の振る舞いを直接導出する、多言語対応の対話型プログラム理解・検証ツール COMB を紹介します。Linux カーネルの検証を含む C と Java のケーススタディで実証されています。
Benjamin Holland, Payas Awadhutkar, Suresh Kothari, Ahmed Tamrawi, Jon Mathews10.1145/3183440.3183476
Springer ICISS · 2017サイドチャネル脆弱性
ソフトウェアのサイドチャネル脆弱性を検出するためのヒューマン・オン・ザ・ループ自動化
正準的なサイドチャネルパターン、プログラム成果物のフィルター、パラメータ化されたグラフモデルを導入し、分析者が時間と空間におけるソフトウェアのサイドチャネル脆弱性（SSCV）の仮説を定式化し検証できるようにします。
Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari, Nikhil Ranade10.1007/978-3-319-72598-7_13
IEEE APSEC · 20175,000 ループ · DARPA アプリ 18 本
アルゴリズム計算量脆弱性を検出するための知能増幅型ループ特徴付け
アルゴリズム計算量脆弱性を含む可能性の高い複雑なループを絞り込むためのループの抽象化と振る舞いのパターンを定義し、4 つのオープンソースライブラリと 18 本の DARPA STAC チャレンジアプリケーションに含まれる 5,000 を超えるループで評価します。
Payas Awadhutkar, Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari論文を読む →
Winter Simulation Conference · 2017Linux のロック 66,609 件
安全性とセキュリティのための大規模ソフトウェアシステム検証から得たモデリングの教訓
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
IEEE VizSec · 2017DARPA Android アプリ 77 本
高度な Android マルウェアを検出するための対話型可視化ツールボックス
Android の複雑なセマンティクスを対話的に探索するための Android Malicious Flow Visualization Toolbox（AMFVT）を紹介し、77 本の高度な DARPA チャレンジ Android アプリケーションにおける監査の精度と効率を報告します。
Ganesh Ram Santhanam, Benjamin Holland, Suresh Kothari, Jon Mathews10.1109/VIZSEC.2017.8062197
IEEE ICST · 2017Java の不変性ベンチマーク
最先端の不変性解析の移植: 実験用ツールボックスと精度ベンチマーク
ポインタ解析と型システムに基づくオブジェクト不変性解析を、Java 8 のソースとコンパイル済みバイトコードを対象に Atlas 上で再実装し、大規模な実アプリケーションでの精度とスケーラビリティを評価するための実験用ツールボックスと精度ベンチマークを導入します。
Benjamin Holland, Ganesh Ram Santhanam, Suresh Kothari10.1109/ICST.2017.55
APSEC · 2016パス依存解析
安全性とセキュリティの脆弱性を正確かつ効率的に分析するための射影制御グラフ
パス依存解析におけるパスの指数的増加とパス実行可能性の複雑さを克服するため、射影制御グラフ（PCG）の抽象化を導入します。Linux カーネルの 3 つのバージョン（ロックインスタンス 66,609 件）にわたって制御フローグラフ（CFG）から PCG への縮約を評価し、Linux Driver Verification（LDV）ツールが見逃した同期のバグを明らかにします。
Ahmed Tamrawi, Suresh Kothari10.1109/APSEC.2016.026
IEEE SCAM · 2016静的情報に基づく動的解析
アルゴリズム計算量脆弱性を検出するための静的情報に基づく動的解析ツール
Atlas 上での静的なグラフ探索によって候補となるループを切り出す手法と、選択したループを様々な入力で評価して過剰な空間・時間の消費を引き起こし確認する、対象を絞った動的解析とを組み合わせます。
Benjamin Holland, Ganesh Ram Santhanam, Payas Awadhutkar, Suresh Kothari10.1109/SCAM.2016.23
IEEE ISSRE Workshops (FVPE) · 2016形式検証の実践
Linux カーネルの形式検証研究から得た実務エンジニアへの知見
Linux Driver Verification（LDV）ツールの実証的な監査を通じて、産業界で形式検証を導入する際の実務上の障壁を、検証結果のクロスチェック、認証用の証拠、IDE との統合に焦点を当てて検討します。
Suresh Kothari, Payas Awadhutkar, Ahmed Tamrawi10.1109/ISSREW.2016.9
IEEE ICPC · 2016不可視の制御フロー
人間と機械による不可視の制御フローの解決
動的束縛、関数ポインタ、非同期コールバックによって生じる不可視の制御フロー（ICF）を解決するための、Atlas 上での対話的な人間と機械の協働による手法を紹介し、Linux カーネルにおける複雑な同期のバグを発見します。
Suresh Kothari, Ahmed Tamrawi, Jon Mathews10.1109/ICPC.2016.7503727
ACM ICSE Companion · 2016人間と機械の協働
検証の再考: 人間と機械の協働による正確性、効率、スケーラビリティ
従来の単独の形式検証と、扱いきれない検証問題に対して人間による照合のための簡潔な視覚的証拠を生成する、人間と機械の協働のフレームワークとを対比します。
Suresh Kothari, Ahmed Tamrawi, Jon Mathews10.1145/2889160.2891046
ACM ICSE Companion · 201637 MLOC · L-SAP
Linux を検証しよう: 自動化と協働による分析的推論の加速学習
証拠に基づく協働検証（EECV）と Atlas 上の L-SAP ツールを紹介します。インスタンス検証キット（IVK）を生成し、Linux カーネルの 3 つのバージョン（37 MLOC）にわたる 66,609 件のロックインスタンスを検証します。
Suresh Kothari, Ahmed Tamrawi, Jeremías Sauceda, Jon Mathews10.1145/2889160.2889192
ACM/IEEE SER&IP · 2016最優秀論文賞
ソフトウェア工学研究室から航空機、Orion、そしてその先へ
学術的なプログラム分析とモデリングの研究を、アビオニクス、自動車システム、NASA の Orion 宇宙船プログラム、DARPA APAC および STAC のサイバーセキュリティ施策で運用される産業用ツールへと展開してきた 20 年の歩みをたどります。
Suresh C. Kothari10.1145/2897022.2897032