Categories
Honors and Awards News

Best Artifact Award for security verification

The paper “Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies using mCRL2”, coauthored with Hamed Arshad, Ross Horne, Olaf Owe, and Tim Willemse, wins the Best Artifact Award at the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems

The paper “Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies using mCRL2”, coauthored with Hamed Arshad, Ross Horne, Olaf Owe, and Tim Willemse, wins the Best Artifact Award at the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems

This work was part of the PhD thesis of Hamed, and the paper is coauthored by five people (from Luxembourg, Netherlands, University of Oslo, and NTNU). The paper was presented at FORTE during the confederated conferences called DisCoTec 2022 and the new tool called XACML2mCRL2 was demoed to the whole community during the plenary demos session. The tool was given the Best Artifact Award (https://www.discotec.org/2022/programme#discotec-best-artefacts) and was also invited for a special issue of the prestigious Elsevier journal Science of Computer Programming appearing in 2023.

Image showing an overview of the verification tool chain, with our tool in green.

The tool is meant to help verify correctness of access control policies, especially applicable to the health domain where our usecase is taken from (hence the playful title of the paper, “Process Algebra Can Save Lives: Static Analysis of XACML Access Control Policies using mCRL2”).

In academia one can use this tool in teaching (it is already used in the MSc course IMT4123 Systems Security at NTNU) or one can build MSc theses topics using the tool for various applications or extensions. More widely, one can use this tool in projects and help industry with their verification tasks.