Language：English   Publishing type：Research paper (scientific journal)   Publisher：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

Language：English   Publishing type：Research paper (scientific journal)   Publisher：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

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：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

Language：Japanese   Publisher：電子情報通信学会  

researchmap

Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：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

Language：Japanese  

CiNii Books

researchmap

Language：Japanese   Publisher：社団法人情報処理学会  

We discuss a characterization of security policies to be enforced with a monitor. The monitor is a enforcement mechanism that work by observing a behavior of a program and terminating its execution if it violates a security policy being enforced. Unfortunately, the monitors is able to enforce not all of security policies in order to limit to observe for a finite behavior and not to use future informations. F.B.Schneider show that policies having the trait become to satisfy Lamport's safety property. Also, there exist Buchi automata to recognize the safety properties and he calls them security automata. Therefore we introduce automata using more information and show that these automata can enforce information flow policies with respect to noninterference.

researchmap

Language：Japanese   Publisher：社団法人電子情報通信学会  

We discuss a characterization of security policies to be enforced with a monitor. The monitor is a enforcement mechanism that work by observing a behavior of a program and terminating its execution if it violates a security policy being enforced. Unfortunately, the monitors is able to enforce not all of security policies in order to limit to observe for a finite behavior and not to use future informations. F.B.Schneider show that policies having the trait become to satisfy Lamport's safety property. Also, there exist Biichi automata to recognize the safety properties and he calls them security automata. Therefore we introduce automata using more information and show that these automata can enforce information flow policies with respect to noninterference.

researchmap

Language：Japanese   Publisher：Information Processing Society of Japan (IPSJ)  

Mobile code has been regarded as a convenient abstraction mechanism to construct flexible/evolvable distributed computing systems. It has now gained prominence, mainly due to the current shift from stationary to mobile/ubiquitous computing environment. Although designing 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. Web site of this project: http://www.psg.cs.titech.ac.jp/sc/

CiNii Books

researchmap