Formal Modeling of Adaptive Security Requirements in Dynamic Systems with Uncertainty
MetadataShow full item record
Modern software systems often operate in highly dynamic environments and are subject to various forms of changes, including: changes in the structure of their operating environments and changes in security requirements. Protecting valuable assets in such changing and uncertain circumstances not only requires specifying adaptive security requirements, but also requires detecting the changes in the operating environment, reasoning about the consequence of changes and readjusting security controls in response to the changes. One step towards ensuring continuous protection of valuable assets is to define the right adaptive security requirements. Formal models of security requirements and policies allow unambiguous and precise definition of security requirements as well as reasoning about correctness and satisfaction of the requirements. Although there is a large body of research in dynamic access control models and mechanisms, security engineers still do not have access to methodological mechanisms to ensure the correctness of the specified requirements and policies. For this purpose, the research problem of this dissertation is how to systematically engineer adaptive security systems and ensure that software-intensive systems continue protecting their valuable assets in the face of run-time changes Standard policy languages such as eXtensible Access Control Markup Language (XACML) do not have formal semantics and do not allow reasoning about policies. Logic-based approachesd have been introduced to allow precise modeling and allow provide verification services. OHowever, ne of the problems with many of the existing logic-based approaches is that they are often expressed in classical logics, also called as monotonic logics. A major issue with monotonic logics is that they are not devised to invalidate initial believes in the light of further observations. For this reason, the research problem of this dissertation is formal modeling of security requirements for dynamic systems with uncertainties. The formal models should be capable of invalidating initial assumptions when changes are detected in the operating environment. They should also be supported by reasoning engines that are capable of reasoning in the absence of context data, which is common in changing environments. The issue of dealing with imperfect context data and incomplete security requirements in overlooked in traditional logic-based formal models. cies are added incrementally. Furthermore, the formalism is used to detect and resolve policy conflicts and identify possible attribute hiding attacks _ This PhD dissertation focuses on developing three types of formal models to support engineering adaptive security: 1) A formal model for context-aware access control policies. This model enables reasoning with unavailable context data and incomplete access control policy sets that are inevitable in dynamic environments, 2) A formal model for structure of operating environments. This model allows keeping track of structural changes of operating environments and verifying the satisfaction of security requirements at runtime when operating environment changes, and 3) A formal model for security violation scenarios, this model allows identifying action-plans in order to readjust security controls. Regarding to these three aspects, first, this thesis introduces a non-monotonic reasoning scheme for specifying context-aware access control policies. In the introduced formalism, unavailable context data and incomplete access control policies can be explicitly expressed. The formalism is based on Answer Set Programming (ASP), a non-monotonic logic programming language that allows invalidation of initial security decisions when policies are added over time. Second, this thesis introduces a formalism based on theory of action and changes that supports keeping track of structural changes, identifying security violations and recommending corrective actions to fix the violations.