| 研究課題/領域番号 |
26540025
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
関 浩之 名古屋大学, 情報科学研究科, 教授 (80196948)
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| キーワード | データベース / k-安全性 / セキュリティ / 量的情報流 |
|---|
| 研究実績の概要 |
データベース内の機密情報の漏洩を防ぐ一般的な手法としてアクセス制御がある．アクセス制御とは，データベースに対し，機密情報が得られるような問合せの実行をアクセス権のあるユーザのみに許可するというものである．以下では，問合せを許可問合せと禁止問合せに分類することによりアクセス制御を行うと仮定する．このようにユーザごとに許可問合せ，禁止問合せが適切に指定されていれば機密情報の漏えいは直接的には生じない．しかし，ユーザがデータベースに対して許可問合せ，データベーススキーマ，問合せのコード（意味）等の公開情報を組み合わせることで，禁止問合せの結果を推論できることがある．このようなユーザの行為を推論攻撃という．推論攻撃によって禁止問合せの結果がk 個未満に絞りこめないとき，データベースインスタンスは（これらの問合せとスキーマに対して）k-安全であるという．本研究ではXML データベーススキーマ，問合せ，インスタンスが与えられたとき，これらを命題論理式のモデル計数問題に帰着してk-安全性を検査する手法の提案を行った．この手法では，スキーマの適合性や問合せの入出力関係を充足可能性問題に帰着し，命題論理式のモデル（命題論理式を充足するような，論理変数への真偽値割り当て）を数えることによりk-安全性を判定する．
入力を制約式に変換するツールを実装し，既存のSugar（順序符号化を行うツール）やsharpCDCL（射影を指定可能なモデル計数ツール）といったツールを用いて提案するk-安全性検査法に基づいた検査システムを実装し，性能評価のための実験を行った．
また，提案する手法では候補データベースのサイズに上限をおいているという点で十分条件を判定しているといえる．そこで禁止問合せがない場合について，提案する手法で判定可能なk-安全性の必要十分条件を与えた．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究で提案する具体的な検証手順は以下の通りである．まず，与えられた適合性制約，禁止問合せの入出力関係制約，許可問合せの入出力関係制約を制約式（範囲付整数を含んだ命題論理式）として表現する．次に制約式を順序符号化を用いて連言標準形命題論理式（CNF 式）に変換し，最後に，このCNF 式を禁止問合せの結果を表す変数に射影した論理式に対してモデル（論理式を真とするような，論理変数への真偽値割り当て）の計数を行い，得られたモデル数（禁止問合せの結果の候補数）を参照することでk-安全性であるかどうかを判定する．つまり入力を命題論理式のモデル計数問題に帰着することでk-安全性の検査を行う．
しかし上記の検証法では生成される命題論理式のサイズが膨大となり検査に大きな時間を要したため，スキーマや問合せの情報を積極的に利用することで生成される命題論理式のサイズを小さくすることで高速化を行う手法も提案した．
ベンチマークを用いた実験では，上記の工夫を行うことにより，生成された論理式の論理変数および節の数が100分の1以下に減少し，検証に要するCPU時間も20分の1以下に減少した．これらにより，提案手法は十分有効であり，研究はおおむね順調に進んでいるといえる．
|
| 今後の研究の推進方策 |
今年度はk-安全性という具体的な量的尺度を設定し，その効果的な解析法を実装することができた．今年度用いたツールはSATソルバー（命題論理式の充足可能性判定ツール）であった．一方，SMTソルバー（背景理論をもつ命題論理式の充足可能性判定ツール）が最近注目されている．整数や実数の線形制約などの有用な背景理論を用いることにより，量的尺度の計算がさらに効率的に行える可能性があり，先行研究もいくつか発表されている．今後はSMTソルバーを活用した解析法の開発に取り組む予定である．
|
| 次年度使用額が生じた理由 |
学会発表２件と，期待通りの研究成果が得られたが，当初予定していた新たな計算機の価格が安価となったこと，アルバイト雇用による研究調査が予想よりも短い時間で済んだこと，旅費に関しては学外の同一分野の研究者との研究討論を出張ではなくテレビ会議で済ますことができたことにより，次年度使用額が生じた．
|
| 次年度使用額の使用計画 |
SMTソルバーを用いた研究を実施する予定であり，高負荷の処理に耐える計算サーバの購入および，研究成果の国際会議における発表旅費のために，次年度使用額分を効果的に利用する予定である．
|
