Verifying Weak Probabilistic Noninterference
Journal Title: International Journal of Advanced Computer Science & Applications - Year 2017, Vol 8, Issue 10
Abstract
Weak probabilistic noninterference is a security property for enforcing confidentiality in multi-threaded programs. It aims to guarantee secure flow of information in the program and ensure that sensitive information does not leak to attackers. In this paper, the problem of verifying weak probabilistic noninterference by leveraging formal methods, in particular algorithmic verification, is discussed. Behavior of multi-threaded programs is modeled using probabilistic Kripke structures and formalize weak probabilistic noninterference in terms of these structures. Then, a verification algorithm is proposed to check weak probabilistic noninterference. The algorithm uses an abstraction technique to compute quotient space of the program with respect to an equivalence relation called weak probabilistic bisimulation and does a simple check to decide whether the security property is satisfied or not. The progress made is demonstrated by a real-world case study. It is expected that the proposed approach constitutes a significant step towards more widely applicable secure information flow analysis.
Authors and Affiliations
Ali A. Noroozi, Jaber Karimpour, Ayaz Isazadeh, Shahriar Lotfi
Keywords
Related Articles
- EP ID EP262229
- DOI 10.14569/IJACSA.2017.081026
- Views 91
- Downloads 0
Voltage Variation Signals Source Identification and Diagnosis Method
Power Quality (PQ) problem has become an important issue for generating bad impact to the users nowadays. It is important to detect and identify the source of the PQ problem. This paper presents a voltage variation signa...
Factors Influencing Cloud Computing Adoption in Saudi Arabia’s Private and Public Organizations: A Qualitative Evaluation
Cloud Computing is becoming an important tool for improving productivity, efficiency and cost reduction. Hence, the advantages and potential benefits of cloud computing are no longer possible to be ignored by organizatio...
New Deep Kernel Learning based Models for Image Classification
Deep learning system is used for solving many problems in different domains but it gives an over-fitting risk when richer representations are increased. In this paper, three different models with different deep multiple...
An Approach for External Preference Mapping Improvement by Denoising Consumer Rating Data
In this study, denoising data was advocated in sensory analysis field to remove the existing noise in consumer rating data before processing to External Preference Mapping (EPM). This technique is a data visualization us...
One-Year Survival Prediction of Myocardial Infarction
Myocardial infarction is still one of the leading causes of death and morbidity. The early prediction of such disease can prevent or reduce the development of it. Machine learning can be an efficient tool for predicting...