A scalable Shannon entropy estimator

摘要: Quantified information flow (QIF) has emerged as a rigorous approach to quantitatively measure confidentiality; the information-theoretic underpinning of QIF allows the end-users to link the computed quantities with the computational effort required on the part of the adversary to gain access to desired confidential information. In this work, we focus on the estimation of Shannon entropy for a given program . As a first step, we focus on the case wherein a Boolean formula captures the relationship between inputs X and output Y of . Such formulas have the property that for every valuation to X, there exists exactly one valuation to Y such that is satisfied. The existing techniques require model counting queries, where .We propose the first efficient algorithmic technique, called to estimate the Shannon entropy of with PAC-style guarantees, i.e., the computed estimate is guaranteed to lie within a …