• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2006 年度 実績報告書

ソフトウェアの安全性向上のための型理論

研究課題

研究課題/領域番号 17300003
研究機関東北大学

研究代表者

小林 直樹  東北大学, 大学院情報科学研究科, 教授 (00262155)

研究分担者 住井 英二郎  東北大学, 大学院情報科学研究科, 助教授 (00333550)
五十嵐 淳  京都大学, 大学院情報学研究科, 助教授 (40323456)
キーワード型システム / プログラム解析 / 割り込み / 並行プログラム / 資源使用法解析 / プログラム等価性 / 双模倣 / 情報流解析
研究概要

ブログラムの安全性向上のために型理論に基づいたプログラム解析・検証・変換などの研究を行っている.本年度の主な研究成果は以下のとおり.
1.並行プログラムのための型システムの改良
型に基づいて並行プログラムのデッドロックなどの解析を行う手法を改良し,従来よりも精度よく解析できるようにした.また,プログラマが必要に応じて型宣言を行えるように型検査アルゴリズムを改良した.
さらに,割り込みが入った計算体系においてデッドロックが起きないことを検証するための型システムも考案した.
2.資源使用法解析の拡張
ファイルやメモリなどの計算資源が正しく使用されているかどうかを型を用いて検証する枠組みにおいて未解決であった,プログラムから推論された使用方法が仕様に適合することを検査するためのアルゴリズムを考案し,その正当性を証明した.
3.プログラムの等価性の検証手法の研究
高階関数・プロセスを持つ言語のプログラムの等価性や定義や証明のための一般的な手法がこれまで提案されておらず,個々の言語ごとにアドホックな手法が提案されていた.そこで,高階言語のための一般的な定義方法・証明手法として環境双模倣の枠組みを提案・定式化した.
4.割り込みの入った計算体系のためのデッドロック型とモデル検査の組み合わせによる情報流解析の手法の研究
ブログラムが機密情報を漏洩していないことを検証するための新しい手法として,型システムとモデル検査を融合した手法を考案した.これにより,モデル検査のみを使うよりも高速で,型のみによる手法と異なり,情報が漏れる場合の具体例を生成することができる.

  • 研究成果

    (6件)

すべて 2007 2006

すべて 雑誌論文 (6件)

  • [雑誌論文] 計算資源使用法検証における計算資源の仕様と実際の使用法の間の適合性検証アルゴリズム2007

    • 著者名/発表者名
      岩間 太, 五十嵐 淳, 小林 直樹
    • 雑誌名

      情報処理学会プログラミング研究会論文誌 48・SIG4

      ページ: 48-61

  • [雑誌論文] Environmental Bisimulations for Higher-Order Languages2007

    • 著者名/発表者名
      Davide Sangiorgi, Naoki kobayashi, Eijiro Sumii
    • 雑誌名

      Proceedings of IEEE Symposium on Logic in Computer Science (LICS 2007) (出版決定)

  • [雑誌論文] Type-Based Analysis of Deadlock for a Concurrent Calculus with Interrupts2007

    • 著者名/発表者名
      Kohei Suenaga, Naoki Kobayashi
    • 雑誌名

      Proceedings of 16th European Symposium on Programming (ESOP'07), Springer Lecture Notes in Computer Science 4421

      ページ: 490-504

  • [雑誌論文] Resource Usage Analysis for the Pi-Calculus2006

    • 著者名/発表者名
      Naoki Kobayashi, Kohei Suenaga, Lucian Wischik
    • 雑誌名

      Logical Methods in Computer Science 22・2:3

      ページ: 1-42

  • [雑誌論文] A New Type System for Deadlock-Free Processes2006

    • 著者名/発表者名
      Naoki Kobayashi
    • 雑誌名

      Proceedings of CONCUR 2006, Springer Lecture Notes in Computer Science 4137

      ページ: 233-247

  • [雑誌論文] Combining Type-Based Analysis and Model Checking for Finding Counterexamples against Non-Interference2006

    • 著者名/発表者名
      Hiroshi Unno, Naoki Kobayashi, Akinori Yonezawa
    • 雑誌名

      Proceedings of ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS 2006)

      ページ: 17-26

URL: 

公開日: 2008-05-08   更新日: 2016-04-21  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi