2016 Fiscal Year Annual Research Report
高階・型付きの計算体系に基づくプログラミングの理論と応用の展開
| Project/Area Number |
15H02681
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
|
|---|
| Project Period (FY) |
2015-04-01 – 2020-03-31
|
| Keywords | セキュリティ型 / declassification / 環境双模倣 / 秘密性・機密性 / プログラム等価性 |
|---|
| Outline of Annual Research Achievements |
研究が多岐にわたるため、主な研究の一つについて述べる。本研究は博士前期課程学生との共同研究である。
セキュリティ型とは、例えば論理値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のあるセキュリティ型つきλ計算において機密性の証明を行うためのプログラム等価性理論の研究を行なった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究課題は複数の理論から成り立っており、個々の理論によって度合いに差はあるが、全体としては順調に進展している。
|
| Strategy for Future Research Activity |
引き続き研究計画のとおり、高階・型付きのプログラミング言語理論にもとづく研究を行う。
|
Research Products
(5 results)
-
[Journal Article] Specialization of Generic Array Accesses After Inlining2017
Author(s)
Ryohei Tokuda, Eijiro Sumii, Akinori Abe
-
Journal Title
Proceedings ML Family / OCaml Users and Developers workshops, ML Family/OCaml 2015, Vancouver, Canada, 3rd & 4th September 2015, Electronic Proceedings in Theoretical Computer Science
Volume: 241
Pages: 45-53
DOI
Peer Reviewed / Open Access / Acknowledgement Compliant
-
-
-
-
