Modeling and checking the security of DIFC system configurations

Decentralized information flow control (DIFC) systems provide strong protection for data secrecy and integrity. However, the complicated configuration of information flow between system objects increases the chance of misconfiguration, making the system vulnerable to attackers. In this paper we first present a systematic analysis of misconfigurations and their security threats for DIFC systems. Then we define the security analysis problem for DIFC configurations based on a formal state-transition model, which allows model checkers to prove a configuration is secure or detect misconfigurations that violate the desired security goal. The experiment shows that bounded model checking techniques plus a novel preprocessing algorithm are effective in solving this problem.