日本応用数理学会2015年度年会
「数理的技法による情報セキュリティ」(FAIS)
オーガナイズド・セッション
日本応用数理学会2015年度年会が 2015.9.9(水)〜2015.9.11(金) に
金沢大学角間キャンパスにて開催されます:
[年会 ホームページ]
http://annual2015.jsiam.org/
「数理的技法による情報セキュリティ」(FAIS)研究部会も, 下記の日程で
オーガナイズド・セッション(OS)を開催いたします.
★今回は特別講演として次の2件のご講演をお願いしております！★
An Intrinsic Encoding of a Subset of C and its Application to
TLS Network Packet Processing
○Reynald Affeldt (National Institute of Advanced Industrial Science and Technology)
QUICの安全性解析
○井関 正也 (東京工業大学), 藤崎 英一郎 (NTTセキュアプラットフォーム研究所)
奮ってご参加下さいますようお願い申し上げます.
【日時】
9月11日(金) 9:30-12：00
【会場】
金沢大学角間キャンパス (石川県金沢市)
http://www.kanazawa-u.ac.jp/university/access
【参加方法】
年会ホームページをご覧ください.
【プログラム】(○: 登壇者)
研究部会OS: 数理的技法による情報セキュリティ(1)［9月11日：09:30-10:50：104］
座長: 花谷 嘉一 （(株)東芝 研究開発センター）
9:30-10:10
[特別講演]
An Intrinsic Encoding of a Subset of C and its Application to
TLS Network Packet Processing
○Reynald Affeldt (National Institute of Advanced Industrial Science and Technology)
[概要]
TLS (a.k.a. SSL) is a widespread security protocol and errors in its
implementation have disastrous consequences. For example, in 2014,
the Heartbleed bug of OpenSSL allowed theft of private keys, thus
compromising any security guarantee. To ensure the correctness of
the implementation of TLS, programmers face two difficulties: an
official specification with the ambiguities of natural language and
error-prone low-level parsing of network packets. We report on the
construction in the Coq proof-assistant of libraries to formally
model, specify, and verify C programs that process TLS packets. More
precisely, we built an encoding of the core subset of C, a
Separation logic that enables byte-level reasoning, and an encoding
of a significant part of the official specification of TLS. We also
verified a parsing function of an existing implementation of TLS,
namely PolarSSL. We were able to correct bugs in the C source code
and to spot ambiguities in the RFC.
10:10-10:30
統計的手法によるプログラムの定量的情報流解析
Chothia, Tom (University of Birmingham, UK),
○Kawamoto, Yusuke (AIST, Japan), Novakovic, Chris (Imperial College London, UK)
[概要]
定量的情報流解析は、システムの出力データに漏洩する秘密情報の量を計算
する解析技術であり、最近十数年間、盛んに研究されてきた。この解析技術
では、システムの出力データと秘密情報の間の対応関係を、情報理論におけ
る通信路行列としてモデル化し、エントロピーを用いて秘密情報の量を定義
する。本研究では、従来技術における状態爆発を避けるために、統計的手法
を用いて、プログラムから漏洩する秘密情報の量を推定する手法を提案する。
具体的には、Javaプログラムをランダムに何度も実行して得られるトレース
集合から漏洩情報量を統計的に推定し、95%信頼区間を計算する。本発表では、
我々が開発した解析ツールleakiEstとLeakWatchを紹介し、様々なシステムの
解析例を通じて、技術の有効性を実証する。
10:30-10:50
MizarによるProbability Distribution Ensemble の形式定義について
○岡崎 裕之 (信州大学), 布田 裕一 (北陸先端技術大学院大学)
[概要]
報告者等は定理証明システムを用いた安全性証明検証システムの開発を進め
ている． 暗号理論において，必要不可欠である識別不能性の形式化定義を行
う際に必要なProbability Distribution Ensembleのよく知られた定義が，そ
のまま形式化を行うには十分にフォーマルであるとは必ずしも言えない．そ
こで報告者らは形式化記述言語Mizarでの形式化に適したProbability
Distribution Ensembleの定義に関する考察を行う．
研究部会OS: 数理的技法による情報セキュリティ(2)［9月11日：11:00-12:00：104］
座長: 吉田 真紀 (情報通信研究機構)
11:00-11:40
[特別講演]
QUICの安全性解析
○井関 正也 (東京工業大学), 藤崎 英一郎 (NTTセキュアプラットフォーム研究所)
[概要]
2013 年にQuick UDP Internet Connections (QUIC) と呼ばれる通信プロトコ
ルがGoogle によって開発された 。QUICはIEEE S&P2015でQACCEというモデル
のもと安全であることが証明されたが、同時にサーバの負荷を増加させる攻
撃も発見された。本発表ではその攻撃を防ぐための改善案を提案し、その攻
撃に対応した新しい安全性モデルについて説明する。
11:40-12:00
形式検証に向けたQUICの安全性定義の検討
○櫻田 英樹 (NTT コミュニケーション科学基礎研究所), 米山 一樹 (茨城大学),
吉田 真紀 (情報通信研究機構), 花谷 嘉一 (東芝 研究開発センター)
[概要]
Webの通信を安全に行うためのセキュアトランスポートプロトコルとしてTLS
が広く使われているが、通信を確立するためのレイテンシが比較的大きいと
いう問題がある。そのためGoogleはこれにかわるプロトコルとしてQUICを提
案している。QUICはTLSと異なり、パケットの再送などをTCPに頼らずUDPを用
いて独自に行い、また鍵共有のためのラウンド数を少く抑えることで遅延を
小さくしている。QUICの安全性を解析した研究として、Lychevらによる研究
がある。本発表ではLychevらによるQUICのモデルをもとに、プロトコル検証
ツールProVerifを用いてQUICの安全性検証を行った結果について述べる。
最新情報は年会のホームページでご確認ください.
【問い合わせ先】
櫻田 英樹 (NTTコミュニケーション科学基礎研究所)
sakurada.hideki(at)lab.ntt.co.jp
最終更新: 2015.8.7