Static verification and enforcement of authorization policies
Stefano Calzavara · ARCA (Università Ca' Foscari Venezia) · 2013
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.