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 101
- Downloads 0
Neural Network Classification of White Blood Cell using Microscopic Images
With the technological advances in medical field, the need for faster and more accurate analysis tools becomes essential for better patients’ diagnosis. In this work, the image recognition problem of white blood cells (W...
A Computational Model of Extrastriate Visual Area MT on Motion Perception
Human vision system are sensitive to motion perception under complex scenes. Building motion attention models similar to human visual attention system should be very beneficial to computer vision and machine intelligence...
A Coreference Resolution Approach using Morphological Features in Arabic
Coreference resolution is considered one of the challenges in natural language processing. It is an important task that includes determining which pronouns are referring to which entities. Most of the earlier approaches...
Fast Hybrid String Matching Algorithm based on the Quick-Skip and Tuned Boyer-Moore Algorithms
The string matching problem is considered as one of the most interesting research areas in the computer science field because it can be applied in many essential different applications such as intrusion detection, search...
Comparing the Usability of M-Business and M-Government Software in Saudi Arabia
This study presents a usability assessment of mobile presence in the Kingdom of Saudi Arabia (KSA), with a particular focus on the variance between M-business and M-government presence. In fact, a general hypothesis was...