Biblio

Access control is a widely used technology to protect information security. The implementation of access control depends on the response generated by access control policies to users’ access requests. Therefore, ensuring the correctness of access control policies is an important step to ensure the smooth implementation of access control mechanisms. To solve this problem, this paper proposes a constraint based access control policy security analysis framework (CACPSAF) to perform security analysis on access control policies. The framework transforms the problem of security analysis of access control policy into the satisfiability of security principle constraints. The analysis and calculation of access control policy can be divided into formal transformation of access control policy, SMT coding of policy model, generation of security principle constraints, policy detection and evaluation. The security analysis of policies is divided into mandatory security principle constraints, optional security principle constraints and user-defined security principle constraints. The multi-dimensional security analysis of access control policies is realized and the semantic expression of policy analysis is stronger. Finally, the effectiveness of this framework is analyzed by performance evaluation, which proves that this framework can provide strong support for fine-grained security analysis of policies, and help to correctly model and conFigure policies during policy modeling, implementation and verification.

As the technology reliance increases, computer networks are getting bigger and larger and so are threats and attacks. Therefore Network security becomes a major concern during this last decade. Network Security requires a combination of hardware devices and software applications. Namely, Firewalls and IPsec gateways are two technologies that provide network security protection and repose on security policies which are maintained to ensure traffic control and network safety. Nevertheless, security policy misconfigurations and inconsistency between the policy's rules produce errors and conflicts, which are often very hard to detect and consequently cause security holes and compromise the entire system functionality. In This paper, we review the related approaches which have been proposed for security policy management along with surveying the literature for conflicts detection and resolution techniques. This work highlights the advantages and limitations of the proposed solutions for security policy verification in IPsec and Firewalls and gives an overall comparison and classification of the existing approaches.

Smart industrial control systems (e.g., smart grid, oil and gas systems, transportation systems) are connected to the internet, and have the capability to collect and transmit data; as such, they are part of the IoT. The data collected can be used to improve services; however, there are serious privacy risks. This concern is usually addressed by means of privacy policies, but it is often difficult to understand the scope and consequences of such policies. Better tools to visualise and analyse data collection policies are needed. Graph-based modelling tools have been used to analyse complex systems in other domains. In this paper, we apply this technique to IoT data-collection policy analysis and visualisation. We describe graphical representations of category-based data collection policies and show that a graph-based policy language is a powerful tool not only to specify and visualise the policy, but also to analyse policy properties. We illustrate the approach with a simple example in the context of a chemical plant with a truck monitoring system. We also consider policy administration: we propose a classification of queries to help administrators analyse policies, and we show how the queries can be answered using our technique.

We describe the formalization of a correctness proof for a conflict detection algorithm for XACML (eXtensible Access Control Markup Language). XACML is a standardized declarative access control policy language that is increasingly used in industry. In practice it is common for rule sets to grow large, and contain unintended errors, often due to conflicting rules. A conflict occurs in a policy when one rule permits a request and another denies that same request. Such errors can lead to serious risks involving both allowing access to an unauthorized user as well as denying access to someone who needs it. Removing conflicts is thus an important aspect of debugging policies, and the use of a verified algorithm provides the highest assurance in a domain where security is important. In this paper, we focus on several complex XACML constructs, including time ranges and integer intervals, as well as ways to combine any number of functions using the boolean operators and, or, and not. The latter are the most complex, and add significant expressive power to the language. We propose an algorithm to find conflicts and then use the Coq Proof Assistant to prove the algorithm correct. We develop a library of tactics to help automate the proof.