Analysis for Probabilistic Information Flow Security Properties
Zhao Bao · Chinese Journal of Computers · 2006
Information flow analysis technology is an essential method used in analyzing computer system security problems, such as private data leak, covert channels and deadlock.This article uses process algebra as the tool for analyzing information flow security properties. Secure Process Algebra (SPA) is extended to probabilistic systems, and then it is called Probabilistic Secure Process Algebra (PSPA). This article employs PSPA to model probabilistic systems, and analyzing probabilistic information flow security properties based on probabilistic weak bisimulation equivalence. Several secure properties based on Nondeducibility on Compositions(NDC), such as P_PBNDC, S_PBNDC, CP_PBNDC, are presented, and the relations between these properties are given. At the end, a real probabilistic system example is presented.