PEALT: An automated reasoning tool for numerical aggregation of trust evidence

Abstract

We present a tool PEALT that supports the understanding and validation of mechanisms that numerically aggregate trust evidence of potentially heterogenous sources. Such mechanisms are expressed in the policy composition language Peal and subjected to vacuity checking, sensitivity analysis of thresholds, and policy refinement. Verification code is generated by either compiling away numerical references prior to constraint solving or by delegating numerical reasoning to Z3, the common back-end constraint solver of PEALT. The former gives compact diagnostics but restricts value ranges and may be space intensive. The latter generates compact verification code, but gives verbose diagnostics, and may struggle with multiplicative reasoning. We experimentally compare code generation and verification running times of these methods on randomly generated analyses and on a non-random benchmark modeling majority voting. Our findings suggest both methods have complementary value and may scale up well for the analysis of most realistic case studies. © 2014 Springer-Verlag.