PV1 ⊧ EntropyEstimationcomputes the Shannon entropy for a given program

Application domain/field

• Quantified information flow
• Confidentiality measurements
• Information leakage

Expected input

Boolean formula

Format:

CNF file

Expected output

Shannon entropy estimation

Internals

Estimates the Shannon entropy of a formula $\phi$ such that the computed estimate is guaranteed to lie with ($1+-ϵ$)-factor of the ground truth with confidence at least $1-\delta$. They focus on Boolean formulas that capture the relationship between input X and output Y of a given program. They estimate the Shannon entropy for this Boolean formula. Uses GANAK for model counting queries and SPUR for sampling queries.