プロトコルの形式検証と脆弱性発見の現実- Case of CCS Injection 株式会社レピダム 林 達也 (@lef )HAYASHI, Tatsuya / Lepidum Co. Ltd.
"CRYPTREC シンポジウム 2015"(2015/3/20)
https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

自己紹介・業務領域
名前林 達也 ( @lef )所属株式会社レピダム 代表取締役
Internet Society Japan Chapter
Online Identity WG チェア/
プログラム委員



OpenID Foundation Japan
事務局長



Identity Conference ( #idcon )オーガナイザー

https://lepidum.co.jp/

業務領域
応用・実用研究
標準化支援
アイデンティティ、プライバ
シー

認証・認可

ソフトウェア&ネットワークセ
キュリティ, 脆弱性ネットワーク技術プログラミング言語処理系
 コンパイラ, インタプリタ,
言語設計
各種コンサルテーション

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

Focus Area | Lepidum
Applied Research and Development
 Personal Data, Digital Identity and Privacy
 Secure and Safety Software Technology
 Web and Internet Technology De-Facto and Forum Standardization


Keywords:
https://lepidum.co.jp/

Personal Data, Trust Framework, Privacy, ID Federation,
Authentication/Authorization, Protocol Specification,* of Things(IoT, WoT), Software Defined Network,
Autonomic Network, etc...
Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

Projects | Lepidum
LACCOONS(Large-scale Automatic Configuration and Control OverOpen Network for SvDI)
 HTTP Mutual Access Authentication Protocol(New protocol for preventing Phishing attacks against
Web systems)
 IDzumo (Digital Identity Components)
 Skyeye (Wi-Fi Connect with AuthN/Z Components)
 Fail-Safe C (Memory-safe implementation of the full
ANSI C language Compiler and libraries) Service Defined Network (SvDI)
https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

Acknowledgement
暗号の専門家ではないので不正確な部分がある可能性があります 発表者は脆弱性の発見者ではありません(発見者：レピダム 菊池正史)
 コードの細部等、技術的に突っ込んだ点には回答出来ないかもしれませんが、お許し下さい

https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

Point of View
脆弱性発見者

脆弱性対応者

エンジニア・(組織の経営者)の視点(非サービス事業者)の視点

標準化策定者の視点

基盤技術の脆弱性

脆弱性発見経験を

基盤技術の

発見の意味

踏まえて

重要性

瀬戸際ぎりぎりを適切な情報開示と事後より事前のリ

歩くような危うさ

共有

ソースの投入https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

プロトコルの形式検証と脆弱性発見の現実- Case of CCS Injection -CCS INJECTIONの発見とその経緯

https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

CCS Injection脆弱性とは


CCS = Change Cipher Spec
TLS/SSLのメッセージ "ここから暗号を変えますよ！"


CCS Injection脆弱性
1.
2.
3.

4.

https://lepidum.co.jp/

中間者(攻撃者)がCCSを挿入するとOpenSSLが適切な検証をせず受理してしまい
変なタイミングで暗号が変わって中間者が通信を完全に解読できる
Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

通常のCCS処理(1)

最初は鍵はないクライア
ント

https://lepidum.co.jp/

？

？

暗
号

暗
号

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

サーバー通常のCCS処理(2)PKIを使って鍵が交換される

クライア
ント

https://lepidum.co.jp/

鍵

鍵

暗
号

暗
号

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

サーバー通常のCCS処理(3)

CCSメッセージを送って暗号を有効化
鍵

鍵

CCS
クライア
ント

暗
号

暗
号
CCS

https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

サーバー通常のCCS処理(4)

暗号通信の開始

クライア
ント

https://lepidum.co.jp/

鍵

鍵

暗
号

暗
号

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

サーバー

CCS Injection攻撃(1)

最初は鍵はない (同じ)

クライア
ント

https://lepidum.co.jp/

？

？

暗
号

暗
号

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

サーバー

CCS Injection攻撃(2)

黒いところにいる攻撃者がCCSを送る
？

？

CCS
クライア
ント

暗
号

暗
号
CCS

https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

サーバー

CCS Injection攻撃(3)

謎の鍵を使って暗号通信を開始してしまう

クライア
ント

https://lepidum.co.jp/

？

？

暗
号

暗
号

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

サーバー

CCS Injection攻撃(4)

謎の鍵は初期値0から作られた自明なもの

クライア
ント

https://lepidum.co.jp/

０

０

暗
号

暗
号

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

サーバー

CCS Injection攻撃(5)
実際はこの後にPKIの処理が走ったり、鍵交換の結果を検証するメッセージ等がある
 それらの辻褄をうまく合わせるように改竄することで自明な鍵を維持したままハンドシェークを完了させることが出来た



https://lepidum.co.jp/

謎の鍵等を含めOpenSSLが本来想定している内部状態が異常になっているので、つじつま合わ
せには技術的な苦労がCopyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

発見の背景(1)

元々、TLS/SSLの安全性に関するソフトウェ
ア的な研究を行っていた
NICT「通信プロトコルとその実装の安全性評価に関する研究開発 -形式手法による プロトコル
実装の検証技術と形式仕様に基づく網羅的ブ
ラックボックス検査技術の開発-」
 平成22～24年度 (産業技術総合研究所/レピダム)
 定理証明支援系 "Coq" 等を利用https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

発見の背景(2)Internet Engineering Task Force (IETF)でのHTTP
やTLSに関係する標準化活動の中で、Beast
AttackやCRIME Attackの対応・影響を間近に体験https://lepidum.co.jp/

実際に、CRIME Attack公開時にはHTTP Basic認証への影響に気づいた為、PoCデモの作成を行い、発見者との情報交換等もCopyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

発見の経緯社内のエンジニア(発見者の菊池)が状態機械の一番複雑な部分がChangeCipherSpecにおける遷移だと考え、既存実装(OpenSSL)の動作を確認したところ検査が不適切であることに気づいた
https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

発見者の初期モチベーション「みんながバグ探し競争してるので効率的に探したい」
 「Coqもどこかで使いたい」
 「バグのありそうなモジュールを経験的に決めうちする」 「意味不明なコードを理解する足がかりが欲しい」

https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

発見者の初期モチベーション「みんながバグ探し競争してるので効率的に探したい」
 「Coqもどこかで使いたい」
しかし…
 「バグのありそうなモジュールを経験的にCoqを使うまでもなく決めうちする」
脆弱性発覚
 「意味不明なコードを理解する足がかりが欲しい」

https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

Coqとは？


定理証明支援系(formal proof management system)

フランス国立情報学自動制御研究所(INRIA)で開発されている(OCaml等を開発している)
 命題と証明を記述すると、"証明が正しいこと"を自動で検証してくれる

一部は自動での証明も行う"プログラミング Coq"

https://lepidum.co.jp/

http://www.iij-ii.co.jp/lab/techdoc/coqt/
Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

脆弱性実証コードの作成
rubyで300行くらい 暗号プリミティブはopensslライブラリを使用
 二日ほどで完成
 壊れた状態でハンドシェークを完了させるた
めに、細かな工夫(試行錯誤)が必要
『結局Coqのコードは100行ぐらいしかできなかった』(継続したいのでスポンサーを募集しております)https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

CCS Injection Vulnerabilityの課題1


このバグはOpenSSLの最初のリリースから存在しており、該当コードは16年そのままだった


しかも、修正のチャンスも3回ほどあった(1) CVE-2004-0079
new_cipherが設定されているときだけ
ChangeCipherSpecを受理するように
 しかしnew_cipherはServerHelloの段階で設定される為、正しい実装にならなかった

https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

CCS Injection Vulnerabilityの課題2(2) CVE-2009-1386
 DTLSで、いきなりChangeCipherSpecを受け取った場合に落ちる問題が修正されたが、やはり正しい実装にならなかった(3) DTLS fragment retransmission bug (OpenSSL bug #1950)
 更にDTLSにおいて、運悪くパケットの順番が入れ替
わってChangeCipherSpecを受け取った場合の検査が追加され、DTLSでは正しい実装に
 未計算のマスターシークレットが暗号に使われた結果、ランダムなメモリを読み出してハンドシェークが失敗すると分析されているが、実はランダムなメモリではなく空のバイト列だった
 これに気付いていれば攻撃の可能性が分かったはず…
https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

プロトコルの形式検証と脆弱性発見の現実- Case of CCS Injection -脆弱性発見とその報告・公開

https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

どこに報告すべきか？
日本語？英語？
 OpenSSL？CERT？
 正しく影響範囲が伝わるか？
 そもそも自分達の解析は正しいのか？
 検証と社内統制
https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

報告した後…


0-day攻撃の可能性も含め危機管理・情報管
理が必要に
基本的には連絡を待つことしか出来ない 他社・他組織との相談等は事実上行えない 箝口令を引かれているスタッフの危機感
 特にレスポンスがないと「本当に報告プロセスは正しかったのか？」等の焦燥感
 影響範囲が大きい(すぎる)と適切な報告先の選択すら難しいhttps://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

報告した後…


0-day攻撃の可能性も含め危機管理・情報管
理が必要に
基本的には連絡を待つことしか出来ない 他社・他組織との相談等は事実上行えない
本当につらいです 箝口令を引かれているスタッフの危機感
 特にレスポンスがないと「本当に報告プロセスは正しかったのか？」等の焦燥感
 影響範囲が大きい(すぎる)と適切な報告先の選択すら難しいhttps://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

何があると良いのか？

各組織で身を切ってやる意味はない！

情報公開・共有の基盤が必要
レスポンスの早い専門組織とその枠組
適切なガイドライン

国内だけでなく国際的にも(この状況でInternet of Things…？！)
https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

情報公開(Blogサイト準備)
ドメイン取得検討 (ドメインドロップ対策も) 広告の非掲載を徹底 (信頼の為)⇒ 是非の議論

こういう反省点を共有したい (1)

負荷対策

CDN検討・検証 (CloudFront VS CloudFlare) キャッシュが有効なBlog構成
 CDNとBlogの動作検証


サイト更新手順の確認
 情報収集・管理体制の構築、徹底 etc...
https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

「正確な」情報公開のポリシーは？


誰かが明確に提示してくれるわけではない

対外発表の機会と日程調整直後にInterop
Tokyoで暗号通信に関する登壇がネーミングが直接的すぎてDNS更新すら危ぶむ羽目にこういう反省点を共有したい (2)

ルールやガイドはない

https://lepidum.co.jp/

良識で判断 ⇒ ？良識？
Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

公開当日


公開時刻は不明なので手動確認！


CERTを含め、誰も発見者に教えてくれるわけではない

取材・お問い合わせ等

メディア、英語対応、お客様、ご相談、SNS…
The Guardian, New York Times, etc...
 適切な取材とそうでない取材
 お取引先への調整

Blogを公開してなかったら耐えられなかった可能性が高い

情報更新
情報の更新などのキャッチアップ
 有識者からの連絡とそうでないものの分別https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

公開当日


公開時刻は不明なので手動確認！


CERTを含め、誰も発見者に教えてくれるわけではない

取材・お問い合わせ等

メディア、英語対応、お客様、ご相談、SNS…

全社体制！
(業務停止)
Blogを公開してなかったら耐えられなかった可能性が高The Guardian, New York Times, etc...
 適切な取材とそうでない取材
 お取引先への調整






い

情報更新
情報の更新などのキャッチアップ
 有識者からの連絡とそうでないものの分別https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

FAQ・その他
なぜロゴを作ったのか？
 『どのくらい儲かりました？』 エンジニア達のケア 経営者的な苦悩

https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

情報管理の重要性
不要な危機感は煽りたくない でも必要なところには『適切に』情報が届いて欲しい 『準備が出来たら』広域に対策をアナウン
スしたい

昨日とか今日の状況と比較してもらえると嬉しいですhttps://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

脆弱性公開の厳しさ

協力依頼も出来ないし、
もちろん誰も助けてなんてくれません
変な会社だから出来たし、企業組織だから耐えられた自負はあります

https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

脆弱性公開の厳しさ


協力依頼も出来ないし、
もちろん誰も助けてなんてくれません

それでも 変な会社だから出来たし、やってよかったと企業組織だから耐えられた自負はあります
思っていますhttps://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

プロトコルの形式検証と脆弱性発見の現実- Case of CCS Injection -暗号技術基盤の脆弱性と現実

https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

CCS Injection発見を踏まえて
CCS Injectionは基盤技術の応用研究に

偶然見つかったに

もっと力を入れる

等しい

必要がある

国内には貢献できる能力を持つエンジニ
ア・研究者が山程いる

https://lepidum.co.jp/

信頼と安全のバランスが崩れている事例

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

TLS/SSL関係のみ！

"The HTTPS-Only Standard""All publicly accessible Federal
websites and web services[1] only provide service over asecure connection.
The strongest privacy
protection currently available
for public web connections is
Hypertext Transfer Protocol
Secure (HTTPS)."

https://lepidum.co.jp/

https://https.cio.gov/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

国内の政府機関サイト
「日本政府機関Webサイト(.go.jp)のTLS対応状況について」( Next Internet Technology and Society Project )"httpsで接続出来た機関は調査を行った35機関中19機関でした。しかし接続出来た機関のうち10機関は404や403エラーなどで正しく表示出来ませんでした。"( https://awa.sfc.keio.ac.jp/2015/03/04/survey-of-supporting-tls-atjapanese-governemnts-website/ )「go.jpドメインのHTTPSサイトの状況について私もみてみました(2015年3月4日時点)」https://lepidum.co.jp/"イベントで一時的に立ち上がってたサイトや停止したサーバーなどがあり、インターネットからアクセス可能なgo.jpドメインの
HTTPSサイトは882中、722であり、 今回は722のgo.jpドメインサイ
トを調査対象としました。 "( http://blog.livedoor.jp/k_urushima/archives/1763144.html )Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

Secure by Default (ex. Google Chrome)"Marking HTTP As Non-Secure"( https://www.chromium.org/Home/chromiumsecurity/marking-http-as-non-secure )"gradually change their UX to display non-secure
origins as affirmatively non-secure. " (まだ試験版(Canary)の話で、さらに設定も必要)"Gradually sunsetting SHA-1"( http://googleonlinesecurity.blogspot.jp/2014/09/gradually-sunsetting-sha-1.html )https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

インターネット基盤技術の課題
信頼できる基盤 • 我々は技術とは？

なにを信頼していたのか？

なぜバラバラに • サイロ化が一番いけない
やってるのか？

https://lepidum.co.jp/

分野なのに…

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

脆弱性発見時の課題"世界平和活動"すぎる

コストがかかりすぎるhttps://lepidum.co.jp/

非効率すぎるあまりにもプロ

セスや体制が成熟していないCopyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

形式検証の重要性
形式検証というプロセス• 頭を少し使うだけで見つかるそのものが重要最初から検証され• ダメなサイクルていることが望ましい
しかし、後からでも手を動かすべき

https://lepidum.co.jp/• 仕様⇒ 実装⇒ 普及(制御不能)⇒ パッチ⇒ 仕様⇒...
• 人間はスケールしない• 安全な領域を少しでも増やし未来に繋ぐ

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

実装の重要性「実装してから仕様を書いて欲しい」「そうすれば実装が複雑で不具合が出そうな部分がわかる
はず」「TLSぐらいの複雑さのプロトコルをCoqでいじるには先に普通に実装した経験がないとつらいと思う」

https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

FREAK Attackの注目点


発見者：miTLS Team

技術的・工学的なアプローチで安全性向上が可能！

"miTLS is a joint project between Inria and Microsoft Research."

miTLS "A verified reference TLS implementation"( https://www.mitls.org/ )F#によるTLS実装"The technical report gives more details on the formal verificationof miTLS and its cryptographic model." "State-machine attacks [2015]
Early CCS Attack and SMACK Attack are prevented as the typebased proof for miTLS guarantees that its state machine conforms
to its logical specification."( https://www.mitls.org:2443/wsgi/tls-attacks )https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

今後の暗号通信の変化
TLS 1.3 (IETF TLS WG)"IP Stack Evolution Program" (IAB)"QUIC:Quick UDP Internet Connections"
tcpcrypt (IETF TCPINC WG)
https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

Heartbleedはひとつの例にすぎない
今後も同じようなことは高い確率で起きうるWrote in2014/6

皆、薄々知っていた

https://lepidum.co.jp/"OpenSSL iswritten bymonkeys" (2009)(peereboom.us)
しかし、「皆」とは実際には
誰なのか？

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

CCS Injection発見を踏まえて(再掲)
CCS Injectionは基盤技術の応用研究に

偶然見つかったに

もっと力を入れる

等しい

必要がある

国内には貢献できる能力を持つエンジニ
ア・研究者が山程いる

https://lepidum.co.jp/

信頼と安全のバランスが崩れている事例

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

我々はどうするべきか？
インターネットは想定を超えたスケールに成長してしまったかもしれない
所与のものではなく、改善し、育て、作り上げていく必要がある
そして、もっと深刻になるべき
その為には、選択と集中、
適切なリソースの投入が必要
https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

我々はどうするべきか？
インターネットは想定を超えたスケールに成長してしまったかもしれない
所与のものではなく、改善し、育て、作り上げていく必要がある

Let's Work !!

そして、もっと深刻になるべき
その為には、選択と集中、
適切なリソースの投入が必要
https://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.

Please contact us

https://lepidum.co.jp/ @lepidum
mailto:hayashi@lepidum.co.jp / @lefhttps://lepidum.co.jp/

Copyright © 2004-2015 Lepidum Co. Ltd. All rights reserved.