Formal Modeling and Verification of Access-Control Policies

(eng) The construction of secure software is a notoriously difficult task. The abstract security requirements have to be turned into functional requirements and then implemented. However, only few techniques allow to verify that the implemented elements fulfill the originally expressed requirements. The potential gap between the specification and the implementation gets even wider with iterative development schemes where code (and sometimes specification) is updated numerous times. In this document we propose a methodology aimed at facilitating the co-evolution of the security requirements and the implemented code. Focusing on the access-control perspective, we provide models and algorithms to specify the expected requirements and to extract the implemented access-control rules directly from the executable source code. Then we verify the conformance of the implemented features towards the specified requirements and, if inconsistencies are found, we provide potential corrective measures that can be applied directly into the source code.