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

マルチスレッド再帰プログラムの自動検証のための形式モデル

研究課題

研究課題/領域番号 21700045
研究種目

若手研究(B)

配分区分補助金
研究分野 ソフトウエア
研究機関高知工科大学

研究代表者

高田 喜朗  高知工科大学, 工学部, 准教授 (60294279)

研究期間 (年度) 2009 – 2010
研究課題ステータス 完了 (2010年度)
配分額 *注記
3,640千円 (直接経費: 2,800千円、間接経費: 840千円)
2010年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円)
2009年度: 2,210千円 (直接経費: 1,700千円、間接経費: 510千円)
キーワード自動検証 / モデル検査 / 形式モデル / プッシュダウンシステム / 形式的検証 / 形式言語理論 / マルチスレッド
研究概要

Java仮想機械等のプログラム実行系にはスタック検査と呼ばれる汎用的なアクセス制御機構が導入されている、プログラム中,重要な資源にアクセスする箇所の直前にアクセス権検査文を置くことで,信頼されていないモジュールがその資源にアクセスすることを防止できる.本研究では,スタック検査の拡張である履歴ベースアクセス制御(HBAC)を対象に,与えられたセキュリティ仕様を満たすようにアクセス権検査文を自動的にプログラムに挿入する方法について検討した、まずアクセス権検査文挿入問題の枠組を定義した後,この問題のco-NP困難性を示した.また,プッシュダウンシステムのモデル検査法を利用してこの問題を解くアルゴリズムを示し,試作システムを例題に適用した.

報告書

(3件)
  • 2010 実績報告書   研究成果報告書 ( PDF )
  • 2009 実績報告書
  • 研究成果

    (4件)

すべて 2010

すべて 雑誌論文 (2件) (うち査読あり 2件) 学会発表 (2件)

  • [雑誌論文] Automatic generation of history-based access control from information flow specification, Automated Technology for Verification and Analysis, ATVA 20102010

    • 著者名/発表者名
      Yoshiaki Takata, Hiroyuki Seki
    • 雑誌名

      Lecture Notes in Computer Science Vol.6252

      ページ: 259-275

    • 関連する報告書
      2010 研究成果報告書
    • 査読あり
  • [雑誌論文] Automatic generation of history-based access control from information flow specification2010

    • 著者名/発表者名
      Yoshiaki Takata, Hiroyuki Seki
    • 雑誌名

      8th International Symposium on Automated Technology for Verification and Analysis

      巻: LNCS 6252 ページ: 259-275

    • 関連する報告書
      2010 実績報告書
    • 査読あり
  • [学会発表] 情報流仕様に基づくアクセス権検査文自動挿入法2010

    • 著者名/発表者名
      高田喜朗
    • 学会等名
      日本ソフトウェア科学会第12回プログラミングとプログラミング言語ワークショップ
    • 発表場所
      香川県琴平温泉
    • 年月日
      2010-03-04
    • 関連する報告書
      2010 研究成果報告書
  • [学会発表] 情報流仕様に基づくアクセス権検査文自動挿入法2010

    • 著者名/発表者名
      高田喜朗, 森田剛正, 関浩之
    • 学会等名
      日本ソフトウェア科学会第12回プログラミングおよびプログラミング言語ワークショップ
    • 発表場所
      香川県仲多度郡琴平町
    • 年月日
      2010-03-04
    • 関連する報告書
      2009 実績報告書

URL: 

公開日: 2009-04-01   更新日: 2016-04-21  

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

Powered by NII kakenhi