Model and formal verification of the C language for secure construction of embedded software
| Project/Area Number |
24500051
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
AFFELDT Reynald 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415641)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
OIWA Yutaka 産業技術総合研究所, 情報技術研究部門, 研究グループ長 (20415649)
|
|---|
| Project Period (FY) |
2012-04-01 – 2016-03-31
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥5,070,000 (Direct Cost: ¥3,900,000、Indirect Cost: ¥1,170,000)
Fiscal Year 2014: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2013: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2012: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
|
|---|
| Keywords | 形式検証 / C言語 / アセンブリ言語 / 組込みソフトウェア / 定理証明支援系 / Coq / 多倍長整数演算 / セキュリティプロトコル / TLS / 詳細化 |
|---|
| Outline of Final Research Achievements |
Formal verification is a technique to guarantee the correctness of software with a high level of confidence. Yet, when software is written in low-level programming languages such as C or assembly, there are so many details that it is difficult in practice to perform such a verification. With embedded software as an objective, we formalize a model and a logic for C that takes platform-dependent details into account. More precisely, to allow for the verification of programs mixing C and assembly, we developed in the Coq proof-assistant a formal library whose validity is assessed by substantial case-studies.
|
Report
(5 results)
Research Products
(25 results)
