文献

J-GLOBAL ID：201802236409883993   整理番号：18A0073121

Androidのセキュリティメカニズムの形式的モデルに基づく解析と試験に向けて【Powered by NICT】

Towards formal model-based analysis and testing of Android’s security mechanisms

著者 (6件)： Betarte Gustavo (Fac. de Ingenieri ́a, Universidad de la Repu ́blica, Montevideo, Uruguay) ,  Campo Juan (Fac. de Ingenieri ́a, Universidad de la Repu ́blica, Montevideo, Uruguay) ,  Cristia Maximiliano (CIFASIS, Universidad Nacional de Rosario, Rosario, Argentina) ,  Gorostiaga Felipe (FCEIA, Universidad Nacional de Rosario, Rosario, Argentina) ,  Luna Carlos (Fac. de Ingenieri ́a, Universidad de la Repu ́blica, Montevideo, Uruguay) ,  Sanz Camila (Fac. de Ingenieri ́a, Universidad de la Repu ́blica, Montevideo, Uruguay)
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2017  号： CLEI  ページ： 1-10  発行年： 2017年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 本論文では,アンドロイドのセキュリティ機構を検証するために形式的手法を適用した経験について報告した。Androidの認可モデルの包括的な形式的仕様記述,定義されたアクセス制御ポリシーを強制する手順の期待される挙動を確立する特性を提示し,証明するために使われてきたを開発した。機構の実際の実装に関する保証を与えるが行われ始めている。は基本的性質を形式的に軽量モデルベース技術を用いた実際の実装の試験で検証した理想化されたモデルの使用を組み合わせた検証手法である。定式化モデルを記述し,定理証明支援系Coqを用いて検証されているセキュリティ特性現在と認証アルゴリズムの使用に依存する試験法を検討した。Copyright 2018 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【Powered by NICT】

シソーラス用語： アルゴリズム ,  *セキュリティ ,  認証 ,  許認可 ,  定式化 ,  アクセス制御 ,  定理証明
準シソーラス用語： 試験方法 ,  モデルベース ,  軽量 ,  形式的仕様記述 ,  *アンドロイド , 【Automatic Indexing@JST】

分類 (2件)： 計算機システム開発  (JD02010R) ,  計算理論  (JB02000A)

タイトルに関連する用語 (6件)： Android ,  セキュリティ ,  メカニズム ,  モデル ,  解析 ,  試験