Quantitative Multirun Security under Active Adversaries

We study the security of probabilistic programsunder the assumption that an active adversary controls part ofthe program´s inputs, and the program can be run several times. The adversary´s target are the high, confidential inputs to theprogram. We model the program behaviour as an information-theoretic channel and define a notion of quantitative multi-runleakage. We characterize in a simple way both the asymptoticmulti-run leakage and its exponential growth rate, depending onthe number of runs, the characterization is given in terms ofthe program´s channel matrix. We then study the case where adeclassification policy is specified: we define a measure of thedegree of violation of the policy and characterize its asymptoticmulti-run behaviour, thus allowing for a combined analysis ofwhat and how much information is leaked. We finally study thecase where a user is faced with the task of assessing the undueinfluence of an active adversary on a deployed program or system, of which only a (black-box) specification is available.