| Project/Area Number |
12133202
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research on Priority Areas
|
| Allocation Type | Single-year Grants |
|---|
| Review Section |
Science and Engineering
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
KOBAYASHI Naoki Tokyo Institute of Technology, Graduate School of Information Science and Engineering, Assoc. Prof., 大学院・情報理工学研究科, 助教授 (00262155)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
IGARASHI Atsushi Kyoto University, Graduate School of Informatics, Lecturer, 大学院・情報学研究科, 講師 (40323456)
|
|---|
| Project Period (FY) |
2000 – 2003
|
| Project Status |
Completed (Fiscal Year 2003)
|
| Budget Amount *help |
¥14,600,000 (Direct Cost: ¥14,600,000)
Fiscal Year 2003: ¥1,900,000 (Direct Cost: ¥1,900,000)
Fiscal Year 2002: ¥6,200,000 (Direct Cost: ¥6,200,000)
Fiscal Year 2001: ¥6,500,000 (Direct Cost: ¥6,500,000)
|
|---|
| Keywords | type system / security / concurrent program / safety / proof assistant / static analysis of communication / resource / information flow analysis / 様相論理 / Coq / Java / ライブロック |
|---|
| Research Abstract |
The aim of this research project was to study type-based methods for verification of programs. The main results are summarized as follows.
-Type sytems for analyzing communication behavior of concurrent programs Flaws and security holes of concurrent programs often reside in description of communications. We have developed type systems for statically detecting such flaws (e.g., deadlock, livelock, and race conditions).
-Type systems for resource usage analysis Computer programs access various resources such as files, memory, and network. We have developed type systems for statically verifying that those resouces are properly accessed. For example, our type system can verify that a file that has been opended is eventually closed.
-Type systems for information flow analysis The purpose of information flow analysis is to statically check that programs do not leak secret information about secret data such as passwords. We have developed type systems for information flow analysis for low-level languages and concurrent languages.
-Verification of concurrent programs using proof assistant Coq We have formalized and verified the correctness of a part of AnZen mail server using proof assistant Coq. Based on that experiment, we have also constructed a Coq library for verifying concurrent programs.
|
