Scalable Precise Computation of Shannon Entropy

Quantitative information flow (QIF) is an important approach to measuring the amount of information leaked about a secret by observing the running of a program [11, 16]. In QIF, we often quantify the leakage using entropy-theoretic notions, such as Shannon entropy [2, 5, 30, 33] or min-entropy [2, 29, 30, 33]. Roughly speaking, a program in QIF can be seen as a function from a set of secret inputs $X$ to outputs $Y$ observable to an attacker who may try to infer $X$ based on the output $Y$. Boolean formulas are a basic representation to model programs [14, 15]. In this paper, we focus on precisely computing the Shannon entropy of a program expressed in Boolean formulas.

Let $\phi (X,Y)$ be a (Boolean) formula that models the relationship between the input variable set $X$ and the output variable set $Y$ in a given program, such that for any assignment of $X$, at most one assignment of $Y$ satisfies the formula $\phi (X,Y)$. Let $p$ represent a probability distribution defined over the set ${\{\mathrm{𝑓𝑎𝑙𝑠𝑒},\mathrm{𝑡𝑟𝑢𝑒}\}}^Y$. For each assignment $\sigma$ to $Y$, the probability is defined as $p_{\sigma }=\frac{\left|\mathrm{𝑆𝑜𝑙}(\phi (Y\mapsto \sigma ))\right|}{\left|\mathrm{𝑆𝑜𝑙}{(\phi )}_{\downarrow X}\right|}$, where $\mathrm{𝑆𝑜𝑙}(\phi (Y\mapsto \sigma ))$ denotes the set of solutions of $\phi (Y\mapsto \sigma )$ and $\mathrm{𝑆𝑜𝑙}{(\phi )}_{\downarrow X}$ denotes the set of solutions of $\phi$ projected to $X$. The Shannon entropy of $\phi$ is $H(\phi )={\sum }_{\sigma \in 2^Y}-p_{\sigma }\log p_{\sigma }$. Then we can immediately obtain a measure of leaked information with the computed entropy and the assumption that $X$ follows a uniform distribution ¹¹1If $X$ does not follow a uniform distribution, techniques exist for reducing the analysis to a uniform case [1]. [19].

The workflow of existing precise methods for computing entropy can often be divided into two stages. In the first stage, we enumerate possible outputs, i.e., the satisfying assignments over $Y$, while in the second stage, we compute the probability of the current output based on the number of inputs mapped to the output [15]. The computation in the second stage often invokes model counting (#SAT), which refers to computing the number of solutions $\mathrm{𝑆𝑜𝑙}(\phi )$ for a given formula $\phi$. Due to the exponential number of possible outputs, the current precise methods are often difficult to scale to programs with a large size of $Y$. Therefore, researchers have increasingly focused on approximate estimation of Shannon entropy. We remark that Golia et al. [15] proposed the first Shannon entropy estimation tool, EntropyEstimation, which guarantees that the estimate lies within $(1\pm ϵ)$-factor of $H(\phi )$ with confidence at least $1-\delta$. EntropyEstimation employs uniform sampling to avoid generating all outputs, and indeed scales much better than the precise methods.

As previously discussed, existing methods for precisely computing Shannon entropy struggle to scale when applied to formulas with a large set of outputs. Theoretically, this requires performing up to $2^{|Y|}$ model counting queries. The primary contribution of this paper is to enhance the scalability of precise Shannon entropy computation by improving both stages of the computation process. For the first stage, we design a knowledge compilation language to guide the search and avoid exhaustive enumeration of possible outputs. This language augments Algebraic Decision Diagrams (ADDs), an influential representation, with conjunctive decomposition. For the second stage, instead of performing model counting queries individually, we leverage shared component caching across successive queries. Moreover, we exploit literal equivalence to pre-process the formula corresponding to a given program. By integrating these techniques, we develop a Precise Shannon Entropy tool PSE. We conducted an extensive experimental evaluation over a comprehensive set of benchmarks (459 in total) and compared PSE with the existing precise Shannon entropy computing methods and the current state-of-the-art Shannon entropy estimation tool, EntropyEstimation. Our experiments indicate that EntropyEstimation is able to solve 276 instances, whereas PSE surpasses this by solving an additional 56 instances. Among the benchmarks that were solved by both PSE and EntropyEstimation, PSE is at least $10\times$ as efficient as EntropyEstimation in 98% of these benchmarks.

The remainder of this paper is organized as follows. Section 2 introduces the notation and provides essential background information. Section 3 introduces Algebraic Decision Diagrams with conjunctive decomposition ($\text{ADD}[\wedge ]$). Section 4 discusses the application of $\text{ADD}[\wedge ]$ to QIF and introduces our precise entropy tool, PSE. Section 5 details the experimental setup, results, and analysis. Section 6 reviews related work. Finally, Section 7 concludes the paper.

In this paper, we focus on the programs modeled by (Boolean) formulas. In the formulas discussed, the symbols $x$ and $y$ denote variables, and literal $l$ refers to either the variable $x$ or its negation $\neg x$, where $var(l)$ represents the variable underlying the literal $l$. A formula $\phi$ is constructed from the constants $\mathrm{𝑡𝑟𝑢𝑒}$, $\mathrm{𝑓𝑎𝑙𝑠𝑒}$ and variables using negation operator $\neg$, conjunction operator $\wedge$, disjunction operator $\vee$, implication operator $\to$, and equality operator $\leftrightarrow$, where $\mathrm{𝑉𝑎𝑟𝑠}(\phi )$ denotes the set of variables appearing in $\phi$. A clause $C$ (resp. term $T$) is a set of literals representing their disjunction (resp. conjunction). A formula in conjunctive normal form (CNF) is a set of clauses representing their conjunction. Given a formula $\phi$, a variable $x$, and a constant $b$, the substitution $\phi [x\mapsto b]$ refers to the transformed formula obtained by substituting the occurrence of $x$ with $b$ throughout $\phi$.

An assignment $\sigma$ over variable set $V$ is a mapping from $V$ to $\{\mathrm{𝑓𝑎𝑙𝑠𝑒},\mathrm{𝑡𝑟𝑢𝑒}\}$. The set of all assignments over $V$ is denoted by $2^V$. Given a subset $V^{\prime }\subseteq V$, ${\sigma }_{\downarrow V^{\prime }}=\{x\mapsto b\in \sigma \mid x\in V^{\prime }\}$. Given a formula $\phi$, an assignment over $\mathrm{𝑉𝑎𝑟𝑠}(\phi )$ satisfies $\phi$ ($\sigma \vDash \phi$) if the substitution $\phi [\sigma ]$ is equivalent to $\mathrm{𝑡𝑟𝑢𝑒}$. Given an assignment $\sigma$, if all variables are assigned a value in $\{\mathrm{𝑓𝑎𝑙𝑠𝑒},\mathrm{𝑡𝑟𝑢𝑒}\}$, then $\sigma$ is referred to as a complete assignment. Otherwise it is a partial assignment. A satisfying complete assignment is also called solution or model. We use $\mathrm{𝑆𝑜𝑙}(\phi )$ to the set of solutions of $\phi$, and model counting is the problem of computing $|\mathrm{𝑆𝑜𝑙}(\phi )|$. Given two formulas $\phi$ and $\psi$ over $V$, $\phi \vDash \psi$ iff $\mathrm{𝑆𝑜𝑙}(\phi \wedge \neg \psi )=\mathrm{\varnothing }$.

In order to compute the Shannon entropy of a circuit formula $\phi (X,Y)$, we need to use the probability distribution over the outputs. Algebraic Decision Diagrams (ADDs) are an influential compact probability representation that can be exponentially smaller than the explicit representation. Macii and Poncino [28] showed that ADD supports efficient exact computation of entropy. However, we observed in the experiments that the sizes of ADDs often exponentially explode with large circuit formulas. We draw inspiration from a Boolean representation known as the Ordered Binary Decision Diagram with conjunctive decomposition ($\text{OBDD}[\wedge ]$) [24], which reduces its size through recursive component decomposition and divide-and-conquer strategies. This approach enables the representation to be exponentially smaller than the original OBDD. Accordingly, we propose a probabilistic representation called Algebraic Decision Diagrams with conjunctive decomposition ($\text{ADD}[\wedge ]$) and demonstrate it supports tractable entropy computation. $\text{ADD}[\wedge ]$ is a general form of ADD and is defined as follows:

Hereafter, we denote the set of variables that appear in the graph rooted at $u$ as $\mathrm{𝑉𝑎𝑟𝑠}(u)$ and the set of child nodes of $u$ as $Ch(u)$. We now turn to show how an $\text{ADD}[\wedge ]$ defines a probability distribution:

Figure 1 depicts an $\text{ADD}[\wedge ]$ representing the probability distribution of ${\phi }_n^{sep}$ in Example 1 over its outputs with respect to $y_1\prec y_2\prec \mathrm{\cdots }\prec y_{2n}$. The reader can verify that each equivalent ADD with respect to $\prec$ has an exponential number of nodes. In the field of knowledge compilation [10, 13], the concept of succinctness is often used to describe the space efficiency of a representation. Based on the following observations, we can conclude that $\text{ADD}[\wedge ]$ is strictly more succinct than ADD. First, OBDD and $\text{OBDD}[\wedge ]$ are subsets of ADD and $\text{ADD}[\wedge ]$, respectively. Second, $\text{OBDD}[\wedge ]$ is strictly more succinct than OBDD [24]. Finally, each $\text{OBDD}[\wedge ]$ cannot be transformed into a non-OBDD ADD.

In this section, we introduce our tool PSE, designed to compute the Shannon entropy of a given circuit CNF formula with respect to its output variables. PSE, as presented in Algorithm 1, takes as input a CNF formula $\phi$, an input set $X$, and an output set $Y$, and returns the Shannon entropy $H(\phi )$ of the formula. Like other tools for computing Shannon entropy, PSE follows a two-stage process: the $Y$-stage (corresponding to outputs) and the $X$-stage (corresponding to inputs). In the $X$-stage (lines 3–4), we perform multiple optimized model counting operations on sub-formulas over variables in $X$, where the leaves of $\text{ADD}[\wedge ]$ are implicitly generated. The optimization technique is discussed in Section 4.1. In the $Y$-stage (the remaining lines), we conduct a search within the $\text{ADD}[\wedge ]$ framework to precisely compute the Shannon entropy, where the internal nodes of $\text{ADD}[\wedge ]$ are implicitly generated. The following observation states the input of each recursive call is still a circuit formula and the two input formulas of a call corresponding to a decision node in $\text{ADD}[\wedge ]$ have the same output variables.

We implemented a prototype of PSE in C++ and performed evaluations in order to understand its performance. We experimented on benchmarks from the same domains as the state-of-the-art Shannon entropy tool EntropyEstimation [15], that is, QIF benchmarks, plan recognition, bit-blasted versions of SMTLIB benchmarks, QBFEval competitions, program synthesis, and combinatorial circuits [27] ²²2The paper of EntropyEstimation [15] does not mention the domains of program synthesis and combinatorial circuits but actually presents benchmarks in these two domains.. EntropyEstimation reported results only for 96 successfully solved benchmarks (denoted ${\mathrm{Suite}}_1$), which we found insufficient for scalability testing. To ensure a rigorous evaluation, we extended ${\mathrm{Suite}}_1$ as follows:

• $\mathrm{■}$

  ${\mathrm{Suite}}_2$ (399 benchmarks): ${\mathrm{Suite}}_1$ is from the benchmarks that were used to test a well-known model counter called Ganak ³³3The benchmarks are available at https://github.com/meelgroup/ganak; thereby, we added each circuit formula in the aforementioned domain but not in ${\mathrm{Suite}}_1$ from the Ganak benchmarks.

• $\mathrm{■}$

  ${\mathrm{Suite}}_3$ (459 benchmarks): Incorporated 60 additional combinatorial circuits ⁴⁴4The additional benchmarks are available at https://github.com/nianzelee/PhD-Dissertation from [27] on the basis of ${\mathrm{Suite}}_2$.

All experiments were run on a computer with Intel(R) Core(TM) i9-10920X CPU @ 3.50GHz and 32GB RAM. Each instance was run on a single core with a timeout of 3000 seconds and 4GB memory, the same setup adopted in the evaluation of EntropyEstimation.

Through our experiments, we sought to answer the following research questions:

1. RQ1:

   How does the runtime performance of PSE compare to the state-of-the-art Shannon entropy tools with (probabilistic) accuracy guarantee?

2. RQ2:

   How do the utilized methods impact the runtime performance of PSE?

Our work is based on the close relationship between QIF, model counting, and knowledge compilation. We introduce relevant work from three perspectives: (1) quantitative information flow analysis, (2) model counting, and (3) knowledge compilation.

In this paper, we propose a new compilation language, $\text{ADD}[\wedge ]$, which combines ADD and conjunctive decomposition to optimize the search process in the first stage of precise Shannon entropy computation. In the second stage of precise Shannon entropy computation, we optimize model counting queries by utilizing the shared component cache. We integrated preprocessing, heuristics, and other methods into the precise Shannon computation tool PSE, with its trace corresponding to $\text{ADD}[\wedge ]$. Experimental results demonstrate that PSE significantly enhances the scalability of precise Shannon entropy computation, even outperforming the state-of-the-art entropy estimator EntropyEstimation in overall performance. We believe that PSE has opened up new research directions for entropy computing in Boolean formula modeling.