Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397
Issue N1 2020 year
Computer systems with high level of security require a formal proof of security in the framework of some mathematical models. There exists a sufficiently large number of such models; most of them have either a graph nature or an automata nature. In some models security is decidable in all cases, however there exist examples in which security is undecidable, so there emerges a need in additional constraints. Another problem consists in mutual expressibility of different security models (e.g. in case of a merge of two systems into one). A possible way of such unification is embedding one system into another. Embedding is a mapping that satisfies three properties: injectivity, preserving security/insecurity and preserving functionality. Our research is focused on Concept-Based Access Control (CBAC) model introduced by Afonin and Bonushkina in 2019. This is a graph model with undecidable security. We constructively show that two classical security models, namely take-grant and noninterference models, can be embedded in CBAC, and complexity of security validation in original systems and in CBAC images has the same order. Thus, CBAC is rich enough to naturally reflect properties of both graph-based models and automata-based models. Since security is decidable in take-grant and noninterference, embeddings produce two new subclasses of CBAC systems with decidable security.