Author’s Web Page: www.dais.unive.it/~calzavara

To my father Angelo (Tito) This thesis addresses the problem of statically verifying and enforcing authorization policies in a range of different settings. The problem of policy verification consists in trying to fill in the gap between a high-level policy specification and its low-level expected security requirements: this problem can be effectively addressed through static model-checking techniques, which allow to assess the robustness of a given authorization policy way before its actual enforcement. The thesis introduces the formal machinery to perform such analysis on role-based access control policies for grsecurity, an extension for the Linux kernel aimed at enhancing the operating system security. An implementation of the analysis is discussed, along with a preliminary investigation about the security of existing grsecurity access control policies. Policy enforcement is an orthogonal issue to policy verification: namely, given a policy specification, the challenge is understanding if a specific system implementa