Abstract

Lattice-based access control models (LBAC) initiated by Bell-LaPadula (BLP)/Biba models, and consolidated by Denning have played a vital role in building secure systems via Information Flow Control (IFC). IFC systems typically label data and track labels, while allowing users to exercise appropriate access privileges. This is defined through a finite set of security classes over a lattice. Recently, IFC has also been playing a crucial role in formally establishing the security of operating systems/programs. Towards such a goal, researchers often use assertions to keep track of the flow of information from one subject/object to another object/subject. Specifying and realizing these assertions will be greatly benefitted, if the underlying labels of objects/subjects can be interpreted in terms of access permissions/rights of subjects/objects as well as subjects/objects that have influenced them; these would lead to automatic generation of proof obligations/assertions. Thus, if one can arrive at a label model for LBAC that satisfies properties like (i) intuitive and expressive labels, (ii) completeness w.r.t. Denning’s lattice model, and (iii) efficient computations on labels, then building/certifying secure systems using LBAC will be greatly benefitted.

In this paper, we arrive at such a semantic generative model (that tracks readers/writers of objects/subjects) for the Denning’s lattice model, and establish a strong correspondence between syntactic label policies and semantically labelled policies. Such a correspondence leads to the derivation of the recently proposed Readers-Writers Flow Model (RWFM). It may be noted that RWFM [11] also deals with declassification rules which is not discussed here as it is not relevant here. The relationship, further establishes that the RWFM  label model provides an application-independent concrete generative label model that is sound and complete wrt Denning’s Model. We define the semantics of information flow in this label model, and argue that reading and writing induce possibly different pre-orders on the set of subjects. Hence, the subject relations become explicit, making it possible to derive relations from the labels. We further define a notion of information dominance on subjects and show that the notion of principal hierarchy can be naturally defined that is consistent with the IFC model; this perhaps overcomes the adverse impact on the flow policy that is often experienced during the classical approach of defining the hierarchy orthogonally. This enables us to realize Role-Based Access Control (RBAC) structurally and enforce information flow security. Further, we demonstrate how the underlying label model succinctly subsumes various lattice-based control models like BLP, Biba, RBAC, Chinese wall model, etc.

Links

• Springer

Citation

Kumar, N.V.N., Shyamasundar, R.K., 2017. A Complete Generative Label Model for Lattice-Based Access Control Models, in: Cimatti, A., Sirjani, M. (Eds.), Software Engineering and Formal Methods, Lecture Notes in Computer Science. Springer International Publishing, Cham, pp. 35–53. https://doi.org/10.1007/978-3-319-66197-1_3