Biblio

While the standard language XACML is very expressive for specifying fine-grained access control policies, defects can get into XACML policies for various reasons, such as misunderstanding of access control requirements, omissions, and coding errors. These defects may result in unauthorized accesses, escalation of privileges, and denial of service. Therefore, quality assurance of XACML policies for real-world information systems has become an important issue. To address this issue, this paper presents a family of coverage criteria for XACML policies, such as rule coverage, rule pair coverage, decision coverage, and Modified Condition/Decision Coverage (MC/DC). To demonstrate the assurance levels of these coverage criteria, we have developed methods for automatically generating tests, i.e., access requests, to satisfy the coverage criteria using a constraint solver. We have evaluated these methods through mutation analysis of various policies with different levels of complexity. The experiment results have shown that the rule coverage is far from adequate for revealing the majority of defects in XACML policies, and that both MC/DC and decision coverage tests have outperformed the existing methods for testing XACML policies. In particular, MC/DC tests achieve a very high level of quality assurance of XACML policies.

With the increasing inter-connection of operation technology to the IT network, the security threat to the Industrial Control System (ICS) is increasing daily. Therefore, it is critical to utilize formal verification technique such as model checking to mathematically prove the correctness of security and safety requirements in the controller logic before it is deployed on the field. However, model checking requires considerable effort for regular ICS users and control technician to verify properties. This paper, provides a simpler approach to the model checking of temperature process control system by first starting with the control module design without formal verification. Second, identifying possible vulnerabilities in such design. Third, verifying the safety and security properties with a formal method.