Towards Formal Security Analysis of Decentralized Information Flow Control Policies
Decentralized Information Flow control (DIFC) is a key innovation of traditional Information Flow Control (IFC). Compared with IFC, DIFC provides new features including decentralized declassification, taint-tracking, and privilege-transferring. These characteristics also make DIFC able to achieve more fine-grained security goals. However, the flexibility of DIFC also presents challenges to its policy verification which existing approaches have not been able to effectively solve. This paper formalizes the DIFC's policy verification problem, and uses Computational Tree Logic formulae to express fine-grained security goals. This paper also proves that the DIFC's policy verification problem is NP-complete, and discusses the main factors resulting in its high computational complexity.