1-Feb-2019: The book about modeling and verification of access control policies in operating systems is published

We are happy to announce availability of "Modeling and verification of access control policies in operating systems" book issued by publishing house "Goryachaya Liniya - Telekom". The book is written by P.N. Devyanin (RusBiTech) and members of Linux Verification Center team within AstraVer project.

The book describes the process of implementing Security Policy Model (ADV_SPM) and Functional Specification (ADV_FSP) families of requirements defined by Common Criteria and refined by FSTEC Russia order #131, dated from July 30, 2018.

"The book considers various aspects of modeling of security policies implemented in access control modules of operating system, starting from requirements formalization and ending with proving correctness of its implementation in the source code. It is worth to note that historically the term modeling of security policy comes from modeling access control policies, but Common Criteria and our book actually covers the tasks of formalization and verification of arbitrary functional requirements. We hope that our experience will help to cultivate advanced practices for achieving the high levels of assurance in critical systems across different domains and industries" - says Alexey Khoroshilov, leading researcher of ISPRAS and director of Linux Verification Center.

The book is recommended to security engineers, teachers and students interested in "Information security" and "Formal methods" domains.