| 研究課題/領域番号 |
24500051
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウエア
|
|---|
| 研究機関 | 国立研究開発法人産業技術総合研究所 |
|---|
研究代表者 |
Affeldt Reynald (AFFELDT Reynald) 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415641)
|
|---|
| 研究分担者 |
大岩 寛 産業技術総合研究所, 情報技術研究部門, 研究グループ長 (20415649)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2016-03-31
|
| 研究課題ステータス |
完了 (2015年度)
|
| 配分額 *注記 |
5,070千円 (直接経費: 3,900千円、間接経費: 1,170千円)
2014年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2013年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2012年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
|
|---|
| キーワード | 形式検証 / C言語 / アセンブリ言語 / 組込みソフトウェア / 定理証明支援系 / Coq / 多倍長整数演算 / セキュリティプロトコル / TLS / 詳細化 |
|---|
| 研究成果の概要 |
ソフトウェアに対して信頼性の高い保証を与える技術として、形式検証が注目されている。しかし、ソフトウェアはＣやアセンブリなどの低レベル言語で書かれると、技術的な詳細が多くなるため、現状では形式検証による安全性の完全な保証はまだ困難である。本研究では組込み応用向けのプログラムの検証のため、プラットフォームによって異なる意味論を表現し、C言語のモデルとその論理を形式化した。具体的には、共通の形式定理のライブラリに基づき、アセンブリ言語とC言語、それぞれの形式検証基盤を構築し、現実的なケーススタディーを用いてその有効性を確かめ、以上の検証実験を公開した。
|
