Static verification and enforcement of authorization policies

The thesis addresses the problem of the verification and enforcement of authorization policies through static analysis techniques. The main contributions are threefold: a formal semantics for grsecurity, which allows us to effectively validate a number of desirable security properties for role-based access control systems; an extension of RCF based on affine logic, to guarantee the enforcement of expressive authorization policies predicating on resource usage bounds; a verification methodology for Android applications, targeted to the enforcement of an access control policy robust against privilege escalation attacks. All the proposed techniques are proved sound and the issues related to their practical implementation are discussed.