The importance of security in computer and information systems is increasing as network-connected computer systems become more ubiquitous. The objective of security is to verify that the computing platform is secured and that data and information are properly accessed and handled by users and applications, ensuring data confidentiality and integrity. To develop a framework for modeling and verifying security as a data quality attribute, designers need to identify parameters and variables with the express power to capture and represent security models and determine the type of analysis to enable.
This post, which is excerpted from a recently published report, presents an approach for modeling and validating confidentiality based on the Bell–LaPadula security model using the Architecture Analysis and Design Language (AADL). It also presents 11 analysis rules that must be enforced over an AADL instance model to ensure the consistency of a security model. Mapping Bell-LaPadula to AADL allows the expression of key concepts within the AADL Model so they can be analyzed automatically.
The Bell–LaPadula Security Model
The Bell–LaPadula security model is a mathematical framework and model for designing secure computer system architectures. In particular, it regulates the dynamic behavior of a system as “subjects” with differing privileges to read from and write to “objects” with different access restrictions. Systems based on this model must enforce two properties:
the simple security property that prevents subjects from reading objects without authorization; andthe star property that prevents sensitive data from being written to insecure objects.
A system in conformance with the model never allows a subject to access an object that it is not permitted to and never allows the subject to manipulate an object in nonpermitted ways.
Our approach to mapping the concepts from the Bell–LaPadula security model to architectural models written in AADL is described in three steps:
our use of the AADL property mechanism to define security labelsour mapping of subjects and objects to AADL language featureshow this mapping affects Bell–LaPadula access modes
This article is purposely trimmed, please visit the source to read the full article.