Verifying access control properties with design by contract: Framework and lessons learned

Ensuring the correctness of high-level security properties including access control policies in mission-critical applications is indispensable. Recent literature has shown how immaturity of such properties has caused serious security vulnerabilities, which are likely to be exploited by malicious parties for compromising a given application. This situation gets aggravated by the fact that modern applications are mostly built on previously developed reusable software modules and any failures in security properties in these reusable modules may lead to vulnerabilities across associated applications. In this paper, we propose a framework to address this issue by adopting Design by Contract (DBC) features. Our framework accommodates security properties in each application focusing on access control requirements. We demonstrate how access control requirements based on ANSI RBAC standard model can be specified and verified at the source code level.