scholarly journals Bisimulation for Secure Information Flow Analysis of Multi-Threaded Programs

2019 ◽  
Vol 24 (2) ◽  
pp. 64 ◽  
Author(s):  
Ali A. Noroozi ◽  
Jaber Karimpour ◽  
Ayaz Isazadeh
Keyword(s):  
Model Checking ◽  
Information Flow ◽  
Flow Analysis ◽  
Operational Semantics ◽  
Kripke Model ◽  
Probabilistic Model Checking ◽  
Sensitive Information ◽  
Information Flow Analysis ◽  
Secure Information

Preserving the confidentiality of information is a growing concern in software development. Secure information flow is intended to maintain the confidentiality of sensitive information by preventing them from flowing to attackers. This paper discusses how to ensure confidentiality for multi-threaded programs through a property called observational determinism. Operational semantics of multi-threaded programs are modeled using Kripke structures. Observational determinism is formalized in terms of divergence weak low-bisimulation. Bisimulation is an equivalence relation associating executions that simulate each other. The new property is called bisimulation-based observational determinism. Furthermore, a model checking method is proposed to verify the new property and ensure that secure information flow holds in a multi-threaded program. The model checking method successively refines the Kripke model of the program until the quotient of the model with respect to divergence weak low-bisimulation is reached. Then, bisimulation-based observational determinism is checked on the quotient, which is a minimized model of the concrete Kripke model. The time complexity of the proposed method is polynomial in the size of the Kripke model. The proposed approach has been implemented on top of PRISM, a probabilistic model checking tool. Finally, a case study is discussed to show the applicability of the proposed approach.

scholarly journals DEVELOPING COMPUTER-BASED SCHEDULE DELAY ANALYSIS METHODS BASED ON INFORMATION FLOW ANALYSIS: A CASE STUDY

2013 ◽  
Vol 19 (6) ◽  
pp. 823-835 ◽  
Author(s):  
Ming-Kuan Tsai ◽  
Jyh-Bin Yang ◽  
Nie-Jia Yau
Keyword(s):  
Mathematical Model ◽  
Information Flow ◽  
Flow Analysis ◽  
Delay Analysis ◽  
Information Flow Analysis ◽  
Schedule Delay ◽  
Analysis Methods ◽  
Computer Based ◽  
Model Schedule

Schedule analysts often resolve diverse schedule delay problems in construction projects based on their subjective experiences. Although various process-based and mathematical-model schedule delay analysis methods are available for effective schedule delay analysis, these methods require time-consuming manual operation. The use of computer-based schedule delay analysis methods seems to be a solution. However, schedule analysts still have difficulty developing computer-based schedule delay analysis methods. Therefore, this study applies information flow analysis to classify the necessary work to develop computer-based schedule delay analysis methods. In contrast to numerous studies that focus only on computerizing a process-based or a mathematical-model schedule delay analysis method, this study constructs a computer-based method that integrates two process-based schedule delay analysis methods simultaneously. In a tested case study, the delay liability for the project owner and contractor was classified successfully. Importantly, this study provides a useful reference for similar applications in project management.

scholarly journals Non-termination and secure information flow

2011 ◽  
Vol 21 (6) ◽  
pp. 1183-1205
Author(s):  
GEOFFREY SMITH ◽  
RAFAEL ALPÍZAR
Keyword(s):  
Information Flow ◽  
Thought Experiment ◽  
Flow Analysis ◽  
Fundamental Property ◽  
Fast Simulation ◽  
Information Flow Analysis ◽  
Probabilistic Simulation ◽  
Secure Information ◽  
Reachability Property ◽  
Probabilistic Programs

In secure information flow analysis, the classic Denning restrictions allow a program's termination to be affected by the values of its H variables, resulting in potential information leaks. In an effort to quantify such leaks, in this paper we study a simple imperative language with random assignments. As a thought experiment, we propose a ‘stripping’ operation on programs, which eliminates all ‘high computation’, and prove the fundamental property that stripping cannot decrease the probability of any low outcome. To prove this property, we first introduce a new notion of fast probabilistic simulation on Markov chains and show that it implies a key reachability property. Viewing the stripping function as a binary relation, we then prove that stripping is a fast simulation. As an application, we prove that, under the Denning restrictions, well-typed probabilistic programs are guaranteed to satisfy an approximate probabilistic non-interference property, provided that their probability of non-termination is small.

Sign in / Sign up

Export Citation Format

Share Document