Modeling and checking the security of DIFC system configurations

Mingyi Zhao, Peng Liu

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

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
Pages21-38
Number of pages18
ISBN (Electronic)9783319014333
ISBN (Print)9783319014326
DOIs
StatePublished - Jan 1 2013

Fingerprint

Flow control
Control systems
Model checking
Experiments

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Cite this

Zhao, M., & Liu, P. (2013). Modeling and checking the security of DIFC system configurations. In Automated Security Management (pp. 21-38). Springer International Publishing. https://doi.org/10.1007/978-3-319-01433-3_2
Zhao, Mingyi ; Liu, Peng. / Modeling and checking the security of DIFC system configurations. Automated Security Management. Springer International Publishing, 2013. pp. 21-38
@inbook{741d8738345a471589ccd2939d1b57b4,
title = "Modeling and checking the security of DIFC system configurations",
abstract = "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.",
author = "Mingyi Zhao and Peng Liu",
year = "2013",
month = "1",
day = "1",
doi = "10.1007/978-3-319-01433-3_2",
language = "English (US)",
isbn = "9783319014326",
pages = "21--38",
booktitle = "Automated Security Management",
publisher = "Springer International Publishing",

}

Zhao, M & Liu, P 2013, Modeling and checking the security of DIFC system configurations. in Automated Security Management. Springer International Publishing, pp. 21-38. https://doi.org/10.1007/978-3-319-01433-3_2

Modeling and checking the security of DIFC system configurations. / Zhao, Mingyi; Liu, Peng.

Automated Security Management. Springer International Publishing, 2013. p. 21-38.

Research output: Chapter in Book/Report/Conference proceedingChapter

TY - CHAP

T1 - Modeling and checking the security of DIFC system configurations

AU - Zhao, Mingyi

AU - Liu, Peng

PY - 2013/1/1

Y1 - 2013/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84948103019&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84948103019&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-01433-3_2

DO - 10.1007/978-3-319-01433-3_2

M3 - Chapter

SN - 9783319014326

SP - 21

EP - 38

BT - Automated Security Management

PB - Springer International Publishing

ER -

Zhao M, Liu P. Modeling and checking the security of DIFC system configurations. In Automated Security Management. Springer International Publishing. 2013. p. 21-38 https://doi.org/10.1007/978-3-319-01433-3_2