Policy-based access control is one of the most fundamental and widely used mechanisms for achieving privacy and security at both application and network levels. Given the high importance and delicacy of security policies, ensuring the correctness of these policies is important, and yet difficult. A tiny error in security policies could lead to irreparable, if not tragic, consequences. Therefore, identifying discrepancies between policy specifications and their intended function is a crucial task. To achieve this goal, this project pursues a new approach to testing and verification of security policies, including application-level security policies (such as XACML policies) and network-level security policies (such as firewall policies). To accomplish this, this project is defining two unified representations for security policies: program code representation and decision tree representation. Second, the project is developing a suite of rigorous and systematic security policy testing techniques. Third, this project is pursuing efficient and scalable verification and change-impact analysis techniques for security policies. Fourth, this project explores methods for testing and verifying stateful security policies. The project is developing frameworks and techniques for testing and verifying both application-level and network-level security policies. The project will also produce concepts and theories that fundamentally advance the knowledge and understanding of security policies. The concepts, theories, algorithms, and tools produced by this NSF-supported research are expected to promote rigorous security policy testing and verification practice, which will lead to better policy quality and higher security assurance in general. Furthermore, the results of this research will enable further innovations in related fields that depend on the correctness of security policy.
Access control is one of the most fundamental and widely used privacy and security mechanisms at both application and network levels. Access control mechanisms decide which principals, such as users or processes, have access to which resources in a system based on user-specified security policies. Given the high importance and delicacy of security policies, ensuring the correctness of security policies is important, and yet difficult. A tiny error in security policies could lead to irreparable, if not tragic, consequences. Therefore, identifying discrepanciesbetween policy specifications and their intended function is a crucial task. To achieve this goal, security policies must undergo rigorous testing and verification to ensure that they truly represent the intention of their policy authors. The main goal of this project is to develop foundations for testing access control policies and a set of techniques and tools for empirically investigating and evaluating the proposedfoundations. In this project, we have successfully achieved the five main objectives of this project: (1) to propose a fault model of access control policies and investigate its fault types' occurrence frequencies in policy development; (2) to develop structural coverage criteria fortesting access control policies; (3) to develop a mutation testing approach for access control policies and use it to assess a testsuite's fault-detection capability; (4) to develop test generation techniques for access control policies; and (5) to develop a setof practical tools for supporting the tasks described in the preceding objectives. The project results will not only deepen our understanding of testing access control policies, a special type of software artifacts under test, but also provide a practical set of techniques and tools to support systematic testing of access control policies. The fundamental concepts developed in this project are useful beyond this project. In particular, this project is defining two unified representations for security policies: program code representation and decision tree representation. Second, the project is developing a suite of rigorous and systematic security policy testing techniques. Third, this project is pursuing efficient and scalable verification and change-impact analysis techniques for security policies. Fourth, this project explores methods for testing and verifying stateful security policies. These techniques are useful beyond the testing and verification of security policies. For example, we have shown that the decision diagram representation is very useful in the efficient evaluation of XACML policies. Our research results have been successfully published in top tier computer science conferences (such as SIGMETRICS, USENIX LISA, INFOCOM, and SRDS), and computer science journals (such as TPDS, ToN, TAAS, TNSM, and COMNET). In particular, our paper titled "First Step Towards Automatic Correction of Firewall Policy Faults" won the Best Student Paper Award in the 24th USENIX Large Installation System Administration Conference (USENIX LISA), in San Jose, California, November 2010. This project has supported a number of Ph.D. students, some of them have successfully graduated with Ph.D. degrees. For example, Chad Meiners, whose Ph.D. studies were supported by this project, has graduated and joined MIT Lincoln Laboratory as a research scientist. As another example, Fei Chen, whose Ph.D. studies were supported by this project, has graduated and joined VMware. The results that we developed in this project has been incorporated into the graduate course CSE 825 "Computer and Network Security" at Michigan State University that the PI has been teaching. The PI designed course projects based on this project for students to work on. The course materials help to educate the next generation of computer engineers for the nation. In addition, Our project has provided new opportunities for Ph.D. students to develop their research skills as they pursue their doctoral degrees and eventual careers in academia and/or industry.
