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

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