Policy-based access control from numerical evidence

Increasingly, access to resources needs to be regulated or informed by considerations such as risk, cost, and reputation. We therefore propose a framework for policy languages, based on semi-rings, that aggregate quantitative evidence to support decision-making in access control systems. As aggregation operators \addition", \worst case", and \best case" over non- negative reals are both relevant in practice and amenable to analysis, we study an instance, Peal, of our framework in that setting. Peal is a stand-alone policy language but can also be integrated with existing policy languages. Peal policies can be synthesized into logical formulae that no longer make reference to quantities but capture all policy behavior. Satis ability checking of such formulae can be used to validate and analyze policies in this new evidence-based approach. We discuss a number of applications, including vacuity, redundancy, change-impact and safety analysis. The synthesis algorithm requires a form of subset enumeration, for which we develop bespoke algorithms and demonstrate experimentally that our algorithms work better than generic state exploration methods. We also sketch how our approach extends from non-negative reals to other semi-rings and even to rings such as the real numbers