| 研究実績の概要 |
研究が多岐にわたるため、主な研究の一つについて述べる。本研究は博士前期課程学生との共同研究である。
セキュリティ型とは、例えば論理値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のあるセキュリティ型つきλ計算において機密性の証明を行うためのプログラム等価性理論の研究を行なった。
|
