• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Book chapter

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

P. 309-313.
Khoroshilov A. V., Petrenko A. K., Девянин П. Н., Kuliamin V., Щепетков И. В.

The paper presents a work-in-progress on formal verification
of operating system security model, which integrates control of confi-
dentiality and integrity levels with role-based access control. The main
goal is to formalize completely the security model and to prove its con-
sistency and conformance to basic correctness requirements concerning
keeping levels of integrity and confidentiality. Additional goal is to per-
form 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.














In book

Edited by: Y. A. Ameur, K. Schewe. Heidelberg: Springer, 2014.