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.