| 講演名 | 2003/11/21 時間制約付き制御フローグラフの弱双模倣等価性検証およびWebセキュリティ検査への応用(VLSIの設計/検証/テスト及び一般 テスト)(デザインガイア2003 -VLSI設計の新しい大地を考える研究会-) 佐々木 俊, 谷本 匡亮, 中田 明夫, 東野 輝夫, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 近年、実時間制約を伴うハードウェア・ソフトウェアプログラムの効率的な開発手法が求められている。プログラム開発においては、プロファイラを用いた分岐構造の変更などが行われるが、そのような場合においても、入出力など外部観測点の間に指定された実時間制約が保存されていることを検証したい。そのような検証には、Global Timed Bisimulationの検証が有用である。本論文では、実時間制約が与えられたプログラムから制御構造と時間制約を抽出したモデルである、Timed CFG(Control Flow Graph)のGlobal Timed Bisimulation等価性検証を、時間強双模倣等価性検証に帰着して行う手法を提案する。WebブラウザのTiming Attackに対する脆弱性検証への応用例も示す。 |
| 抄録(英) | In recent years, the effective development methodology for software with real-time constraints is desired. Programmers sometimes change blanch structure in their codes to improve performance. This may change timing of I/O action of programs. Thus, programmers want to check whether timing behavior of I/O action is equivalent between original codes and optimized ones. In such verification, we think that verification of global timed bisimulation equivalence is useful. In this paper, we propose timed CFGs (Control Flow Graph), which represent control structure with real-time constraints of real-time software. And we show that verification of global timed bisimulation equivalence for timed CFGs can result in existing parametric verification of strong timed bisimulation equivalence. We also apply our approach to checking for timing attacks on Web privacy. |
| キーワード(和) | 実時間制約 / Timed CFG / Global Timed Bisimulation / 時間強双模倣 / Timing Attack |
| キーワード(英) | Real Tune Constraints / Timed CFG / Global Timed Bisimulation / Strong Timed Bisimulation / Timing Attack |
| 資料番号 | ICD2003-147 |
| 発行日 |
| 研究会情報 | |
| 研究会 | ICD |
|---|---|
| 開催期間 | 2003/11/21(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Integrated Circuits and Devices (ICD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 時間制約付き制御フローグラフの弱双模倣等価性検証およびWebセキュリティ検査への応用(VLSIの設計/検証/テスト及び一般 テスト)(デザインガイア2003 -VLSI設計の新しい大地を考える研究会-) |
| サブタイトル（和） | |
| タイトル（英） | Global Timed Bisimulation on Timed Control Flow Graph And Application to Checking for Timing Attacks on Web Privacy |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 実時間制約 / Real Tune Constraints |
| キーワード(2)（和/英） | Timed CFG / Timed CFG |
| キーワード(3)（和/英） | Global Timed Bisimulation / Global Timed Bisimulation |
| キーワード(4)（和/英） | 時間強双模倣 / Strong Timed Bisimulation |
| キーワード(5)（和/英） | Timing Attack / Timing Attack |
| 第 1 著者 氏名（和/英） | 佐々木 俊 / Suguru SASAKI |
| 第 1 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 2 著者 氏名（和/英） | 谷本 匡亮 / Tadaaki TANIMOTO |
| 第 2 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 3 著者 氏名（和/英） | 中田 明夫 / Akio NAKATA |
| 第 3 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 第 4 著者 氏名（和/英） | 東野 輝夫 / Teruo HIGASHINO |
| 第 4 著者 所属（和/英） | 大阪大学大学院情報科学研究科 Graduate School of Information Science and Technology, Osaka University |
| 発表年月日 | 2003/11/21 |
| 資料番号 | ICD2003-147 |
| 巻番号（vol） | vol.103 |
| 号番号（no） | 478 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |