Cybersecurity policy verification with declarative programming

摘要

Cybersecurity is a growing concern in today’s society. Security policies have been developed to ensure that data and assets remain protected for legitimate users, but there must be a mechanism to verify that these policies can be enforced. This paper addresses the verification problem of security policies in role-based access control of enterprise software. Most existing approaches employ traditional logic or procedural programming that tends to involve complex expressions or search with backtrack. These can be time-consuming, and hard to understand, and update, especially for large-scale security verification problems. Declarative programming paradigms such as “Answer Set” programming have been widely used to alleviate these issues by ways of elegant and flexible modeling for complex search problems. However, solving problems using these paradigms can be challenging due to the nature and limitation of the declarative problem solver. This paper presents an approach to automated security policy verification using Answer Set programming. In particular, we investigate how the separation of duty security policy in role-based access control can be verified. Our contribution is a modeling approach that maps this verification problem into a graph-coloring problem to facilitate the use of generate-and-test in a declarative problem-solving paradigm. The paper describes a representation model and rules that drive the Answer Set Solver and illustrates the proposed approach to securing web application software to assist the hiring process in a company.