Modeling and checking the security of DIFC system configurations

Mingyi Zhao, Peng Liu

Research output: Chapter in Book/Report/Conference proceedingChapter

1 Scopus citations


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.

Original languageEnglish (US)
Title of host publicationAutomated Security Management
PublisherSpringer International Publishing
Number of pages18
ISBN (Electronic)9783319014333
ISBN (Print)9783319014326
StatePublished - Jan 1 2013

All Science Journal Classification (ASJC) codes

  • General Computer Science


Dive into the research topics of 'Modeling and checking the security of DIFC system configurations'. Together they form a unique fingerprint.

Cite this