Copyright Statement: This is an open access article licensed under a Creative Commons Attribution 4.0 International License, which permits unrestricted use, distribution, and reproduction in any medium, even commercially as long as the original work is properly cited.
Digital Object Identifier (DOI) : 10.14569/IJACSA.2017.081026
Article Published in International Journal of Advanced Computer Science and Applications(IJACSA), Volume 8 Issue 10, 2017.
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.
Ali A. Noroozi, Jaber Karimpour, Ayaz Isazadeh and Shahriar Lotfi, “Verifying Weak Probabilistic Noninterference” International Journal of Advanced Computer Science and Applications(IJACSA), 8(10), 2017. http://dx.doi.org/10.14569/IJACSA.2017.081026