モデル検査グリッドセキュリティ

PAGLIARECCI F.; SPALAZZI L.; SPEGNI F.

文献

J-GLOBAL ID：201302279600025014 整理番号：13A0148935

モデル検査グリッドセキュリティ

Model checking grid security

出版者サイト複写サービスで全文入手 {{ this.onShowCLink("http://jdream3.com/copy/?sid=JGLOBAL&noSystem=1&documentNoArray=13A0148935&COPY=1") }}
高度な検索・分析はJDreamⅢで {{ this.onShowJLink("http://jdream3.com/lp/jglobal/index.html?docNo=13A0148935&from=J-GLOBAL&jstjournalNo=A0620C") }}

著者 (3件)： , ,
資料名：
巻： 29 号： 3 ページ： 811-827 発行年： 2013年03月
JST資料番号： A0620C ISSN： 0167-739X 資料種別：逐次刊行物 (A)
記事区分：原著論文発行国：オランダ (NLD) 言語：英語 (EN)

グリッドコンピューティングは高性能計算の先導形式の1つである。グリッド環境におけるセキュリティは設計者を誤りへと導き得る多くの微妙な点を含む複雑系として特徴付けられる挑戦課題である。これは自動検証技法(特にモデル検査)が設計時に非常に有用であると証明されたセキュリティプロトコルに対して起こった事と類似している。本論文ではグリッドシステムに対するセキュリティ検証のホスティングに対して適用できるモデル検査に基づいた形式検証方法論を提案した。提案方法論はグリッドシステムがパラメータ化モデルとして記述でき,セキュリティ要求が超特性として記述できる事を考慮に入れなければならない。不幸にも,パラメータ化モデル検査及び超特性検証双方は,概して,決定可能でない。しかしながら,ジョブがそれらの編成において何らかの規則性を持つ時にこの問題が決定可能となる事が証明された。それ故に,本論文では与えられたグリッドシステムモデルを”切断”定理(即ち,切断サイズまでの有限ジョブ数を用いてシステムによって要求が満足される時に限って任意のジョブ数を用いてシステムによって要求が満足される)が適用可能となるモデルへと低減する検証方法論を提示した。本方法論はその証明を本論文中で提示した定理の集合によって支持される。本方法論をCondorシステムのケーススタディの手段によって説明した。Copyright 2013 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.

, , , , , ,
, ,

計算機網 , データ保護 , 計算機システム開発 , 通信網

前のページに戻る