Formal Verification of OS Security Model with Alloy and Event-B

Petr N. Devyanin, Alexey V. Khoroshilov, Victor V. Kuliamin, Alexander K. Petrenko, Ilya V. Shchepetkov
Digital Printed Abstract View Cite
Type
Short Paper
Publication
4th International Conference on ASM, Alloy, B, TLA, VDM, and Z (ABZ'14)

Abstract

The paper presents a work-in-progress on formal verification of operating system security model, which integrates control of confidentiality and integrity levels with role-based access control. The main goal is to formalize completely the security model and to prove its consistency and conformance to basic correctness requirements concerning keeping levels of integrity and confidentiality. Additional goal is to perform data flow analysis of the model to check whether it can preserve security in the face of certain attacks. Alloy and Event-B were used for formalization and verification of the model. Alloy was applied to provide quick constraint-based checking and uncover various issues concerning inconsistency or incompleteness of the model. Event-B was applied for full-scale deductive verification. Both tools worked well on first steps of model development, while after certain complexity was reached Alloy began to demonstrate some scalability issues.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{DevyaninKKPS14,
  author       = {Petr N. Devyanin and
                  Alexey V. Khoroshilov and
                  Victor V. Kuliamin and
                  Alexander K. Petrenko and
                  Ilya V. Shchepetkov},
  editor       = {Yamine A{\"{\i}}t Ameur and
                  Klaus{-}Dieter Schewe},
  title        = {Formal Verification of {OS} Security Model with Alloy and Event-B},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 4th International
                  Conference, {ABZ} 2014, Toulouse, France, June 2-6, 2014. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {8477},
  pages        = {309--313},
  publisher    = {Springer},
  year         = {2014},
  url          = {https://doi.org/10.1007/978-3-662-43652-3\_30},
  doi          = {10.1007/978-3-662-43652-3\_30},
  timestamp    = {Sun, 02 Jun 2019 21:23:59 +0200},
  biburl       = {https://dblp.org/rec/conf/asm/DevyaninKKPS14.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'14

Related