著者

奥田 哲矢 中林 美郷 荒井 研一 菊池 亮 千田 浩司

雑誌

研究報告コンピュータセキュリティ(CSEC) (ISSN:21888655)

巻号頁・発行日

vol.2021-CSEC-95, no.17, pp.1-8, 2021-11-01

---

本研究では,TEE (Trusted Execution Environment) を応用したクラウドサービス群である Confidential Computing について,データおよびプログラムの両者を秘匿したまま利用できる Confidential Program Execution を提案し,その安全性を評価する.前提として,Intel SGX,AMD SEV のようなサーバサイドにおける TEE を使えば,クラウド事業者に対してデータを秘匿しつつ,クラウドサービスを利用することができる.さらにその発展として,Felsen らは,データを有するユーザとプログラムを有するユーザが,互いにそれぞれのデータとプログラムを自身以外(クラウド事業者を含む)には秘匿したまま,プログラムの実行結果を享受できる方式を提案している.しかし Felsen らの方式は,実行毎にデータとプログラムをクラウド事業者にアップロードする必要があり,かつ方式の安全性証明は与えられていなかった.本稿では,Felsen らと同様にデータとプログラムを秘匿しつつ実行結果を得られ,且つ実行毎にデータとプログラムをクラウド事業者にアップロードする必要がない方式を提案し,その方式の安全性を,形式検証ツールである ProVerif を用いて評価した.評価の結果,本研究の提案プロトコルが,各データおよびプログラムの秘匿の要件,および各エンティティの認証の要件を充足することが分かった.また,本研究の提案および評価を通じて分かった,TEE 応用プロトコル設計時に,TEE がユーザとは独立したエンティティとしてふるまう点,および,TEE を含めたマルチパーティの攻撃者モデルを想定すべき点は,今後多くの TEE 応用プロトコルが設計される際に,プロトコル設計者の参考になると期待される.

著者

岡崎 裕之 布田 裕一 師玉 康成 荒井 研一

出版者

信州大学

雑誌

基盤研究(C)

巻号頁・発行日

2017-04-01

---

本研究では、形式的定理証明系Mizarとモデル検査器ProVerifを用いて、計算機援用による暗号システムの安全性形式的評価システムを開発した。Mizarでは暗号理論に関わる形式化数学ライブラリを開発した。本成果は確率、統計、関数解析、計算アルゴリズムや計算量等の計算機科学の基礎の形式化であるので、暗号理論以外にも応用できる。一方、ProVerifでは、基本的な暗号プロトコルのみならず、従来より抽象度が低くより現実のシステムや実装に近いモデルでの安全性検証手法を提案した。これにより暗号学的ハッシュ関数やブロック暗号の利用モード等の開発時の設計支援や形式的安全性検証を行うことが可能となった。

著者

小林 透 深江 一輝 今井 哲郎 荒井 研一 宮崎 禎一郎 辻野 彰

出版者

The Institute of Electronics, Information and Communication Engineers

雑誌

電子情報通信学会論文誌 D (ISSN:18804535)

巻号頁・発行日

vol.J105-D, no.10, pp.533-545, 2022-10-01

---

本研究では,人型コミュニケーションロボットが,一人暮らしの高齢者との自然会話を基に認知症の予兆検知を行い,認知症の疑いがあれば,ソーシャルメディアを介して離れて暮らす家族やソーシャルワーカ等に通知する認知症予兆発見システムを開発した.著者らは,これまで,スマホが使えない高齢者とLINEを介した双方向のコミュニケーションが可能なソーシャルメディア仲介ロボットを開発した.本研究では,本ロボットに,“認知症予兆発見方式”を追加することで認知症予兆発見システムを実現した.認知症予兆発見方式では,臨床的に信頼性が高い改定長谷川式簡易知能評価スケール(HDS-R)から自然会話シナリオを生成し,シナリオに基づくロボットと高齢者との対面会話による認知度の自動スコアリングが特徴である.本システムは,高齢者に相対する人型コミュニケーションロボットと全体を制御するクラウドサービスから構成されている.開発したプロトタイプシステムを用いた高齢者に対する評価実験により,従来の医師が実施する認知症診断結果と本システムによる評価結果を比較することで,本システムの有効性を明らかにした.