| Project/Area Number |
12133206
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research on Priority Areas
|
| Allocation Type | Single-year Grants |
|---|
| Review Section |
Science and Engineering
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology (JAIST) |
|---|
Principal Investigator |
FUTATSUGI Kokichi Japan Advanced Institute of Science and Technology (JAIST), School of Information Science, Professor, 情報科学研究科, 教授 (50251971)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
IIDA Shusaku Senshu University, Lecturer, ネットワーク情報学部, 専任講師 (80338590)
OGATA Kazuhiro Japan Advanced Institute of Science and Technology (JAIST), School of Information Science, Assistant, 情報科学研究科, 助手 (30272991)
MORI Akira National Inst. of Advanced Industrial Sci. and Tech., Group Leader, サイバーアシストセンター, グループリーダー (30311682)
NAKAMURA Masaki Japan Advanced Institute of Science and Technology (JAIST), School of Information Science, Assistant, 情報科学研究科, 助手 (40345658)
天野 憲樹 北陸先端科学技術大学院大学, 情報科学研究科, 助手 (30313703)
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| Project Period (FY) |
2000 – 2003
|
| Project Status |
Completed (Fiscal Year 2003)
|
| Budget Amount *help |
¥30,800,000 (Direct Cost: ¥30,800,000)
Fiscal Year 2003: ¥5,800,000 (Direct Cost: ¥5,800,000)
Fiscal Year 2002: ¥10,700,000 (Direct Cost: ¥10,700,000)
Fiscal Year 2001: ¥14,300,000 (Direct Cost: ¥14,300,000)
|
|---|
| Keywords | system security / system verification / unknown virus detection / authentication protocol / e-commerce protocol / formal methods / behavioral specification / CafeOBJ / CafeOBJ / 検証 / ウィルス検査 / 振舞モデル検査 / 安全性 / 自動証明器PigNose / UNITY / CadeOBJ / Java仮想機械 / 安全性検証 / セキュアプロトコル / 実時間システム / 移動コード / 抽象機械 |
|---|
| Research Abstract |
The following results have been gotten by doing research for developing the verification technology which is highly applicable and flexible, and is amenable for automation.
(1)Inspection Technology for Unknown Viruses : Based on the logics of behavioral specifications, a technology for modeling behavior s of programs and automatically inspecting their safety is developed. A virus inspection program is developed for Windows OS, and the effectiveness of developed technology has been proved.
(2) Safety Verification Technology based on Behavior Specification : By formalizing requirements and/or specifications in behavior level, a verification technology is developed which can verify the safety properties of systems in the level which is more honest to users or application logics. The technology has been applied to railway signal systems, software components, concurrent and distributed systems, and secure protocols, and is proved to be effective. In particular, verifications of several practical e-commerce protocols have been done using the technology.
(3) Model Checking Technology based on Behavioral Specification : Based on behavioral specifications, a model checking technology which is effective for software with infinite states is developed.
|
