記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：UNIV CINCINNATI INDUSTRIAL ENGINEERING  

A model-checking approach to analyze the robustness of procedures that suffer from human-made faults is proposed. Many procedures executed by humans incorporate fault detection and recovery tasks to recover from human-made faults. Examining whether such recovery tasks work as expected is crucial to preserve the trust and reliability inherent in safety-critical domains. To achieve this, we have employed a fault-injection method that injects a set of human-made faults into a fault-free model for a given procedure. This fault set is selected according to Swain's discrete action classification. The proposed approach uses a model checker to determine paths to error states within the model, and its properties are formalized via calculus of communicating systems and linear temporal logic. The effectiveness of the proposed method is demonstrated by investigating the recoverability of a real-world procedure.

Web of Science

researchmap

記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：University of Cincinnati  

A model-checking approach to analyze the robustness of procedures that suffer from human-made faults is proposed. Many procedures executed by humans incorporate fault detection and recovery tasks to recover from human-made faults. Examining whether such recovery tasks work as expected is crucial to preserve the trust and reliability inherent in safety-critical domains. To achieve this, we have employed a fault-injection method that injects a set of human-made faults into a fault-free model for a given procedure. This fault set is selected according to Swain's discrete action classification. The proposed approach uses a model checker to determine paths to error states within the model, and its properties are formalized via calculus of communicating systems and linear temporal logic. The effectiveness of the proposed method is demonstrated by investigating the recoverability of a real-world procedure.

Scopus

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Springer Verlag  

We propose a model-checking approach for analyzing the robustness of procedures that suffer from human-made faults. Many procedures executed by humans incorporate fault detection and recovery tasks to recover from human-made faults. Examining whether such recovery tasks work as expected is crucial for preserving the trust and reliability inherent in safety-critical domains. To achieve this, we used a type of fault-injection method that injects a set of human-made faults into a fault-free model of a given procedure
the fault set is selected according to Swain's discrete action classification. We use a model checker to determine paths to error states within the model and its properties formalized via CCS and LTL. We show the effectiveness of our method by investigating the recoverability of a real-world procedure. © Springer International Publishing Switzerland 2014.

DOI： 10.1007/978-3-319-08222-6

Scopus

researchmap

記述言語：日本語   出版者・発行元：電子情報通信学会  

researchmap

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：IEEE  

We algebraically characterize a class of enforceable security policies that by execution monitoring using a modal logic. We regard monitors as processes in Milner's CCS and security policies as formulas in the modal logic. We show that a set of processes occurring in a monitor must be within the greatest fixed point for the formula, following Schneider's definition on execution monitors. We also consider monitors that can derive some sequences from a single captured action sequence. To discuss such monitors, we introduce variables ranging over sets of processes in CCS. We then show that there is fixed points under the extension. This work may help its to understand such monitors to detect covert channels at run time and to analyze safety properties for multithreads, which need to examine multiple paths.

DOI： 10.1109/CRISIS.2008.4757483

Web of Science

researchmap

記述言語：日本語   出版者・発行元：[日本ソフトウェア科学会]  

CiNii Books

researchmap

記述言語：日本語   出版者・発行元：社団法人情報処理学会  

モニタにより強制可能なセキュリティーポリシの特徴について議論する.ここでいうモニタとはプログラムの振舞を監視し,もしそれがポリシに違反するときにはそのプログラムを強制的に停止することによりポリシを強制する強制機構のことである.もちろん,このような強制機構ではすべてのポリシが強制可能であるわけではない.なぜなら,モニタはプログラムの有限の振舞しか観測できず,未来の情報を利用することが出来ないからである.F.B.Schneiderはこのような特徴をもつポリシはLamportの安全性の特徴を充たすことを示した.また,そのような安全性を受理するようなオートマトンが存在し,それをセキュリティーオートマトンと呼んでいる.さらに,我々はモニタは単にプログラムの振舞を観測するだけでなくもっと多くの情報を利用できると考える.そのとき,ポリシがどのような特徴を持つか明らかにすることを試みる.これまでに,観測した有限の振舞の部分的な振舞を利用することにより情

researchmap

記述言語：日本語   出版者・発行元：社団法人電子情報通信学会  

モニタにより強制可能なセキュリティーポリシの特徴について議論する.ここでいうモニタとはプログラムの振舞を監視し,もしそれがポリシに違反するときにはそのプログラムを強制的に停止することによりポリシを強制する強制機構のことである.もちろん,このような強制機構ではすべてのポリシが強制可能であるわけではない.なぜなら,モニタはプログラムの有限の振舞しか観測できず,未来の情報を利用することが出来ないからである.F.B.Schneiderはこのような特徴をもつポリシはLamportの安全性の特徴を充たすことを示した.また,そのような安全性を受理するようなオートマトンが存在し,それをセキュリティーオートマトンと呼んでいる.さらに,我々はモニタは単にプログラムの振舞を観測するだけでなくもっと多くの情報を利用できると考える.そのとき,ポリシがどのような特徴を持つか明らかにすることを試みる.これまでに,観測した有限の振舞の部分的な振舞を利用することにより情

researchmap

記述言語：日本語   出版者・発行元：一般社団法人情報処理学会  

柔軟な分散計算システムを構築するための便利な抽象化機構としてさまざまな形態の異動コードが注目されてきた．固定的なネットワークシステムから移動・遍在計算機環境へとシフトするうえで，移動コードの重要性が増している．しかし，実際の応用システムで移動コードを採用するうえで，解決しなければならないセキュリティ上の問題はまだ多い．さらに，移動コードを用いてシステムを構成するためには，コードの移動がひきおこすさまざまな変化に対処できる必要がある．そしてセキュリティモデルもそのために拡張可能（あるいは適応的）である必要があり，さらにそういったセキュリティモデルのためのポリシー記述はむずかしい．今回の発表では，まずアプリケーション依存のセキュリティポリシーについて述べ，次にそういったポリシーを強制する方法の提案について説明する．対象とする移動コードは，ここではJava クラスファイルとする．我々の方式は，主としてロード時のバイトコード変換によって監視付き実行を行うコードを挿入するものであるが，そのためのポリシーをPolaris という特別な言語によって記述する．Polaris は基本的には有限状態プロセス言語であるが，変数間のデータ依存関係を扱えるようになっている．これによって監視のコストを抑えることができる．記述の具体例として，我々が構築しつつある拡張可能メールクライアントの一部を示す．Mobile code has been regarded as a convenient abstraction mechanism to construct flexi-ble/evolvable distributed computing systems. It has now gained prominence, mainly due to the current shift from stationary to mobile/ubiquitous computing environment. Although de-signing a system using mobile code is appealing, its deployment is still a security risk. Further, a system using mobile code is inherently dynamic; we need an extensible/adaptable security model. In this talk, we first claim that application-dependent and special-purpose security policies are increasingly important especially for modern distributed computing environment. Then we present a set of techniques that may be used to enforce such policies on mobile objects (Java classes). The main technique is a load-time bytecode modification that enforces user-defined policies via monitored execution. The policies are written in a language called Polaris, which is basically a finite process language enhanced to deal with data-dependencies among variables. Use of data-dependencies reduced the cost of monitoring. As an example, we show a code portion from our extensible e-mail client system.

CiNii Books

researchmap