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

2016 年度 実績報告書

高階・型付きの計算体系に基づくプログラミングの理論と応用の展開

研究課題

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

研究代表者

住井 英二郎  東北大学, 情報科学研究科, 教授 (00333550)

研究期間 (年度) 2015-04-01 – 2020-03-31
キーワードセキュリティ型 / declassification / 環境双模倣 / 秘密性・機密性 / プログラム等価性
研究実績の概要

研究が多岐にわたるため、主な研究の一つについて述べる。本研究は博士前期課程学生との共同研究である。
セキュリティ型とは、例えば論理値true, falseにラベルH, Lをつけてtrue_H, true_L, false_H, false_Lのようにセキュリティレベルを表し、それらの論理値の型boolにもbool_Hやbool_Lのようにラベルをつけた型のことである。ラベルの意味としては秘密性(secrecy)ないし機密性(confidentiality)や完全性(integrity)が考えられるが、ここでは説明を簡単にするため、秘密性・機密性のみを考えることとする。高機密な論理値true_H, false_Hは型bool_Hを持ち、低機密な論理値true_L, false_Lは型bool_Lを持つ。また、値xが高機密型bool_Hを持つならば、それに依存する式if x then e1 else e2にも高機密型を与えることにより、間接的な情報漏えいをも防止する。しかし、そのように一切の情報漏えいを許さない型付けは厳格すぎる場合も多いため、高機密型から低機密型への意図的な変換(declassification)を考える。研究代表者らは、自身らの環境双模倣(environmental bisimulation)の理論を発展させ、declassificationのあるセキュリティ型つきλ計算において機密性の証明を行うためのプログラム等価性理論の研究を行なった。

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

本研究課題は複数の理論から成り立っており、個々の理論によって度合いに差はあるが、全体としては順調に進展している。

今後の研究の推進方策

引き続き研究計画のとおり、高階・型付きのプログラミング言語理論にもとづく研究を行う。

  • 研究成果

    (5件)

すべて 2017 2016

すべて 雑誌論文 (3件) (うち査読あり 3件、 オープンアクセス 1件、 謝辞記載あり 2件) 学会発表 (2件) (うち国際学会 1件)

  • [雑誌論文] Specialization of Generic Array Accesses After Inlining2017

    • 著者名/発表者名
      Ryohei Tokuda, Eijiro Sumii, Akinori Abe
    • 雑誌名

      Proceedings ML Family / OCaml Users and Developers workshops, ML Family/OCaml 2015, Vancouver, Canada, 3rd & 4th September 2015, Electronic Proceedings in Theoretical Computer Science

      巻: 241 ページ: 45-53

    • DOI

      10.4204/EPTCS.241.4

    • 査読あり / オープンアクセス / 謝辞記載あり
  • [雑誌論文] 無限の入出力を行う関数型プログラムのK正規化の形式的検証2017

    • 著者名/発表者名
      水野 雅之, 住井 英二郎
    • 雑誌名

      コンピュータソフトウェア

      巻: 印刷中 ページ: 印刷中

    • 査読あり
  • [雑誌論文] A Sound and Complete Bisimulation for Contextual Equivalence in λ-Calculus with Call/cc2016

    • 著者名/発表者名
      Taichi Yachi, Eijiro Sumii
    • 雑誌名

      Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, Lecture Notes in Computer Science

      巻: 10017 ページ: 171-186

    • DOI

      10.1007/978-3-319-47958-3_10

    • 査読あり / 謝辞記載あり
  • [学会発表] A Sound and Complete Bisimulation for Contextual Equivalence in λ-Calculus with Call/cc2016

    • 著者名/発表者名
      Taichi Yachi, Eijiro Sumii
    • 学会等名
      14th Asian Symposium on Programming Languages and Systems
    • 発表場所
      Hanoi, Vietnam
    • 年月日
      2016-11-21
    • 国際学会
  • [学会発表] 無限の入出力を行う関数型プログラムのK正規化の形式的検証2016

    • 著者名/発表者名
      水野 雅之, 住井 英二郎
    • 学会等名
      日本ソフトウェア科学会大会
    • 発表場所
      東北大学(仙台市)
    • 年月日
      2016-09-09

URL: 

公開日: 2018-01-16  

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

Powered by NII kakenhi