Formal Proofs of Realistic Programs using Separation Logic
| Project/Area Number |
21700048
|
|---|
| Research Category |
Grant-in-Aid for Young Scientists (B)
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
Software
|
|---|
| Research Institution | National Institute of Advanced Industrial Science and Technology |
|---|
Principal Investigator |
AFFELDT Reynald 独立行政法人産業技術総合研究所, セキュアシステム研究部門, 研究員 (40415641)
|
|---|
| Project Period (FY) |
2009 – 2011
|
| Project Status |
Completed (Fiscal Year 2011)
|
| Budget Amount *help |
¥3,250,000 (Direct Cost: ¥2,500,000、Indirect Cost: ¥750,000)
Fiscal Year 2011: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2010: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2009: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Keywords | 仕様技術 / 形式手法 / 形式検証 / 定理証明支援系 / ホーア論理 / 分離論理 / 多倍長整数関数 / 疑似乱数生成器 / 符号付き多倍長整数 / 情報理論 / 形式的証明 / 定理証明支援器 / プログラム変換 |
|---|
| Research Abstract |
With the dissemination of embedded systems, it has become important to provide strong security guarantees for low-level programs. According to international standards, the most reliable evaluation assurance method is formal verification. Unfortunately, given the current state of the art, it is still difficult to perform formal verification of large programs. Yet, low-level programs are characterized by detailed memory manipulations, for which the formalism of Separation Logic has been proposed by researchers. In this project, we have developed an environment for formal verification based on Separation Logic, whose usefulness is demonstrated by realistic case studies(SmartMIPS implementations of a pseudorandom number generator and signed multi-precision arithmetic, including the binary extended GCD algorithm, as used in the implementation of cryptographic schemes).
|
Report
(4 results)
Research Products
(34 results)
