SMTP

計算機言語論II
Software Security
特に「安全メール」
(2008 spring)
米澤明憲
講義の概要
0.
•
•
•
•
•
•
•
•
参考文献など
「オブジェクト指向とは」とその他の雑談
ソフトウエアセキュリティの研究の一端
オブジェクト指向言語の特徴
オブジェクト指向の意味論・実装法
並列/分散オブジェクト指向計算
オブジェクト指向言語における「型」
(型付アセンブリ言語)
(アスペクト指向プログラミング)
ソフトウエアセキュリティ研究の一端
(初心者向け)
(Software Security)研究で
想定する脅威
• 悪意や誤りのあるプログラムが
– 計算機システムを破壊
– 秘密を漏洩
• コンピュータウィルスが
– サーバプログラムの欠陥をついて侵入
• なりすまし(impersonation)
– 正当な利用者のふりをして
計算機システムを不正使用、不正接続
セキュリティホールの原因
• 事故や攻撃に対する想定に漏れがある
– 最も一般的なセキュリティホールの原因は、
想定外の入力,想定外の環境やタイミングでの動
作などにより,システムが想定外の挙動を示す
E.g., 外部からワームやウイルスを注入される
• E.g., 外部からのリクエストの組み合わせ次第で,
本来秘密の情報が漏れてしまう
よくある攻撃の例:
メールに添付されたウイルス
添付
ファイル
(readme.exe)
メール
本文
• 郵便受けは,外に向かって常に開いている
• 通常のメールシステムは悪質な添付ファイル
の存在を想定していない
– 「ユーザが判断できる」という逃げの姿勢で設計
されているシステムが多い
従来手法 (1/3)
• 攻撃パターン毎に対症療法的に対応
–
–
–
–
E.g., パッチの配布
E.g., アンチウイルスソフト
E.g., ファイアウォール
E.g., 侵入検知システム(IDS)
未知の攻撃
既知の
攻撃
正常
従来の対策法
• 添付ファイルを開かないようにする
• ワクチンで既知ウイルスを排除する
拒否
既知の
ウイルス
有害なのに
実行されてしまう
安全
未知のウィルス・
悪性プログラム
良性プログラム
我々の不正コード防御戦略
不正コード=(ウイルスもその例)
1.添付ファイル(コード)を理論の裏付けられた
方法で解析し,危険性の有無を検査
2.危険性のある箇所は,
安全なコードに書き換える
3.それができない場合,OS(あるいは
仮想機械)で監視しながら実行
サンドボックス法
サンドボックス法(Sandboxing)
サンドボックス外への
アクセスは禁止
サンドボックス
環境
システムリソース
コード
ネットワーク
サンドボックス内の
アクセスは許可
資源アクセスの制御法
1. システムコールフック
2. バイナリーコード変換
(課題:. 1、2の利点・欠点の面で比較せよ.)
3.サンドボックス作るためのOS組み込み機能
(Eg., chroot – プロセスがアクセスできるファイル名空間を、全空間の 一
部
であるsubtreeに限定する。
jail – FreeBSDのシステムコールで、Sboxをファイル+ネットワーク
のアクセスも制限する。)
4. 仮想機械や仮想OS
5.サンドボックス処理の無効化・バイパス防止
我々の防御戦略
ー3重のセーフティネット
プログラムやプロトコルの論理的解析・検証
実
行
前
セキュアな言語の使用
/実装
セキュアな実行時系・
オペレーティングシステム
実
行
中
我々の防御網
拒否
既知の 未知の
ウイルス 不正コード
(ウイルス)
安全
無害化された
プログラム
監視実行される
プログラム
この領域を
我々の研究で
できるだけ
小さくする
安全とわかる
プログラム
バッファーオーバフロー攻撃
バッファオーバーフロー (1/3)
• 指定されたメモリ領域からデータ溢れを起こす
プログラミング上のバグ
– 配列で宣言された範囲を超えたデータのアクセス
A1
A2データA
A3 A4
A5
B1
A6
B2
B3
A7
データB
B4
– 隣接したデータや制御情報を破壊
– 普通は,ソフトウェアが異常終了
– 不注意からバッファオーバーフローバグがプログラム
に入り込むことが頻繁にある
• C言語の標準的な教科書(K&R)にもこのバグが
バッファオーバーフロー (2/3)
• バッファオーバーフローを悪用した侵入法
– 悪性命令列を含む長大なデータの送信
• 悪性命令列の設置+命令制御情報の書き換え
A1
A2データA
A3 A4
A5
次の
命令
B2
B3
データB
B4
もともとのプログラム
バッファオーバーフロー (3/3)
• バッファオーバーフローを悪用した侵入法
– 悪性命令列を含む長大なデータの送信
悪
い
命 令
データA
列
次の
命令
B2
B3
データB
– データとして悪性命令列をインストール
– 命令制御情報の書き換えによって,制御を奪う
B4
安全なメールシステム
メールシステムの基本構造
LAN
LAN
サーバ
メーラ
サーバ
LAN
インターネット
サーバ
メーラ
研究対象としてのメールシステム
• 問題が凝縮されている
– サーバとクライアント
• サーバ: 公開アドレス,自律動作,ワームの脅威
• クライアント: プライベートアドレス,人間が操作,
ウイルスの脅威
– 信頼性に対する高い要求
– 古典的問題
• 盗聴,改竄,なりすまし
想定するメールシステムへの攻撃
• サーバへの攻撃
クラッキング,ワーム
サービス拒否攻撃
• 通信路への攻撃
盗聴,改竄
• クライアントへの攻撃
ウイルス添付メール
迷惑メール
システムの安全性
• サーバ
– ワームやクラッキングへの耐性
– メーリングリストなど拡張機能の安全な実行
– 故障時にはメールをどこかに退避
• メーラ
– 添付ファイルの検査
– 添付ファイルの安全な実行
• プロトコル
– 配送経路のトラッキング
– 送信否認の防止
基本的な前提 (1/2)
• ハードウェア
– 任意のタイミングで一時的に停止しうる
– 頑強なストレージ(ミラーリング,RAIDなど)を仮
定
– ハードウェアのセキュリティホールは想定外
• ネットワーク
– 任意のタイミングで一時的に切断しうる
• システムソフトウェア
– OS等のセキュリティホールは想定外
23
基本的な前提 (2/2)
• 攻撃
– ネットワーク経由の攻撃だけを仮定
– 物理攻撃は想定外
• 互換性
– 通常のメールシステムとの互換性が必要
24
我々のアプローチ (1/2)
• プログラムの検証と監視実行
• 3階層のセーフティネット
実
行
前
プログラムやプロトコルの検証
セキュアな言語の使用実装
セキュアな実行時系・
オペレーティングシステム
実
行
中
我々のアプローチ (2/2)
悪性
良性
コード書換
監視実行
悪性と判定
良性と判定
サーバに対する脅威と対策
• ワームやクラッキング
– バッファオーバーフロー攻撃などは,安全な言語
で防御
• 危険な拡張機能
– SoftwarePot (加藤和彦)を用いて
拡張機能を隔離実行
• メールの消失事故
– 消失しないことを数学的に検証
• 証明は約18,000行
• 証明支援系 Coq を利用
メーラに対する脅威とその対策
• 危険な添付ファイル
– 検査系と実行系を
プラグイン可能にするシステム構成を設計
– 検査系:未知ウイルス検知システムなど
– 実行系:SoftwarePot など
• 受信したメールの消失事故
– 検証済み
主な要素技術 (1/2)
プログラム検証
耐故障性などを
保証
新規開発
システム
安全な言語
メモリの安全性を
保証
監視実行
リソースの安全
性を保証
主な要素技術 (2/2)
ダウンロード
されたコード
プログラム検証
メモリの安全性を
保証
監視実行
リソースの安全
性を保証
プログラム検証の意義 (1/2)
• Common Criteria Evaluation Assurance Levels
–
–
–
–
EAL1: Functionally Tested
EAL2: Structurally Tested
EAL3: Methodically Tested and Checked
EAL4: Methodically Designed, Tested, and
Reviewed
– EAL5: Semiformally Designed and Tested
– EAL6: Semiformally Verified Design and Tested
– EAL7: Formally Verified Design and Tested
プログラム検証の意義 (2/2)
• 本当にクリティカルな部分は数学的検証を
行う価値がある
• 我々の経験事例
– コードサイズ 約600行
– 証明サイズ
約18,000行
– 労力
100~150人時
メールシステム構築の目的
• 安全なソフトウェアシステム構築方式を体系化
–
–
–
–
想定する攻撃は,ワーム,ウイルス,クラッキングなど
ソフトウェア技術でソフトウェアを守る
人的問題,社会的問題にはあまり踏み込まない
暗号の問題にもあまり踏み込まない
• 領域に関連した技術の統合と実証試験
• そのための例題としてメールシステムを選択
安全メールの基本機能
• 既存メールシステムとの互換性
– SMTP/POP3 をサポート
• 安全サーバ
– (機能的には普通の) SMTP サーバ
• 安全メーラ
– MIME のサポート
– Jar ファイルの実行環境
安全メールの特徴 (1/2)
• 安全プロトコル
– 改竄防止と経路認証が可能な配送プロトコル
– 既存 SMTP サーバからは透過的
– BAN論理を用いた理論的な検証
• 安全サーバ
– メモリセーフな実装
– Coq を用いた形式的かつ機械的な検証
安全メールの特徴 (2/2)
• 安全メーラ
– 検証するには複雑すぎる
• JavaMail, Java Swing などに依存
– センシティブなのは添付ファイル実行部分
– 検査器用のプラグインインタフェース
• E.g., 静的解析モジュール
• E.g., コード変換モジュール
• E.g., 動的モニタリングモジュール
– 実行器用のプラグインインタフェース
実装の状況
• Java 言語でメモリセーフに実装
• 基本機能と特徴的機能の一部が動作
• Windows 2000/XP, Solaris 7/8, Linux,
MacOS Xなどで稼動中
• 現在α版の段階
安全プロトコルの概要
• 改竄防止と経路認証
– 改竄が行われていないことを確認できる
– 送信者と中継サーバを確認できる
– 送信を否認できない
• 信頼度の判断材料
– E.g., 検査サーバが中継したメールは信頼する
• 匿名性での悪事も防ぎたい
安全
サーバ
危険
サーバ
安全プロトコルの実現
• 送信者と中継サーバが電子署名
– 中継のたびに署名を追加
• 付加情報はヘッダーに格納
– 送信者,送信先,時刻印,次のサーバ,署名など
X-Anz: [email protected],[email protected]:..
X-Anz-Sig: sn=0,si=anzenmail.is.titech.ac.jp,di=cs.titech.ac.jp,
ts=1026375710449,sa=SHA1withRSA,sg=xLsXLKk+T1P
l7DxacE1DgWZAQffJ07wQ9sn8luUQZvqlAFOVBD9CP
wZxOP5uJ6nHtQ4y74loMpMokhgfzjdWzafEQzAUMwD
9PBLQK9hlL2v+6xpFdca9pht7OSsLsTzb0BVihZmX666
F93kadO95ceLonKJDEJKAyOGUZ/ll5Eo=
課題: このプロトコルで安全でない部分を指摘し、その対策を考えよ。
安全プロトコルの検証
• ほぼ次のような性質を理論的に検証
– 最終受信者は,メッセージ m を受信した時に,
以下を確信できる
• 送信者が最初のサーバに m を送った
• 経路上の各サーバ(最後のものは除く)が次の
サーバへ m を転送した
• 正確には,もっと複雑な性質を証明してる
安全プロトコルと相互運用性
• 配送経路上にレガシー SMTP サーバが存在す
る場合
– メールの送受信は可能
– 経路認証は部分的にしか機能しない
– レガシーサーバが勝手にメールのボディを変更した場
合,改竄とみなされる
• 暗号化,受信否認の防止などについて
– 他のメッセージフォーマットやプロトコルと組み合わる
– SMTP 準拠なら組み合わせ可能
安全サーバの構成
• SMTPの送受信部,メッセージキュー管理
部などから構成される,
SMTP
protocol
SMTP
受信部
SMTP
送信部
メッセージキュー
署名
SMTP
protocol
安全サーバの検証 (1/3)
• SMTP 受信部の正当性を形式的に検証
– プロトコル仕様を満たさないリクエストを拒否する
– 致命的エラー(fatal error)が生じない限り,プロトコ
ル仕様を満たすリクエストを受理する
– Ack を返す前に,メッセージをストレージにセーブ
する(サーバが落ちてもメッセージは喪失されない)
SMTP
protocol
SMTP
受信部
安全サーバの検証 (2/3)
• 証明支援系として Coq を利用
– Java のメソッドを Coq の関数へ変換してから
検証
– オリジナルのプログラムからバグを数個発見
– 検証の規模とコスト
•
•
•
•
対象は約600行のJavaソースコード
仕様のサイズは約300行
証明のサイズは約5,000行
要した労力は,約100人時+2CPU分
安全サーバの検証 (3/3)
• 検証を可能とした条件
– 検証の対象が比較的小さかった
– サーバの記述は,オブジェクト指向的でなく,
型安全な命令型
– スレッド間の干渉が実質的にない
安全メーラ (1/2)
• 見かけは普通のメーラに近い
– フォルダの一覧
– 選択されたフォルダ内のメール一覧
– 選択されたメールの内容表示
• MIME タイプに応じて,検証系と表示・実
行系を選択
– 検査系や表示・実行系はプラグイン可能
安全メーラ の見かけ
安全メーラの構成 (1/2)
• 検証系と実行系を追加できる
検証
V4
モジュール
機能拡張
E4
モジュール
V1 V2 V3
E1 E2 E3
安全メーラ
JavaMail1.2
JVM
安全メーラの構成 (2/2)
検証
モジュール
外部
検証器
危険
V1 V2 V3 V4
安全
A
E1
A
添付コード
E2
E3
E4
安全メーラ
Java Security Architecture
OS & other resources
外部検証&実行モジュール
• 署名の検証系
– Jar ファイルの署名を検査
• SoftwarePot
– Linux/x86, Solaris のバイナリをサンドボックス内で実
行
• 資源使用解析
– 資源の利用順序に依存する性質を静的に検査
• アンチウイルスエンジン
まとめ
• 安全な配送プロトコルの設計と検証
– 改竄と送信・転送の否認を防止
• サーバの構築と検証
– シンプルな設計
– コア部の検証
• クライアントの設計と構築
– 本体の検証は当面行わない
– 添付ファイルの安全な実行をめざす