发表机构
Darwin Deason Institute for Cyber Security; Southern Methodist University（达尔文·迪森网络安全研究所; 南方卫理公会大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一种版本空间方法，解决了概率组合等价性检查的指数级枚举问题，还将其应用于逻辑锁定网表的密钥计数，在70个TrustHub实例中验证了存活熵低于声明密钥长度的结论。
AI 中文摘要
关于数字电路的许多问题具有相同的形式：存在一个隐藏对象，它与一组观测值一致，研究者希望知道仍保持一致的候选对象数量，以及下一步应进行何种观测。存活候选对象的集合即为版本空间，其大小（取对数后）可衡量观测值的收敛程度。本文将版本空间视角作为一种方法，并将其应用于两个通常被视为不相关的电路分析问题。第一个问题是概率组合等价性检查，其中候选对象是布尔函数，观测值是改进的Haar谱系数。2002年提出的一种方法提出了该计数问题，但仅解决了两个特殊情况，使得一般情况成为观测值数量的指数级枚举问题，本文解决了该问题：通过对块和进行重新参数化，将嵌套系数间的依赖关系转化为局部性；采用求和-乘积递归以真值表大小的多项式时间精确计数存活函数；针对单个系数、系数对及所有祖先闭集，推导得到了闭式表达式；2002年工作所采用的独立性近似的误差等于可计算的格索引，所有公式均通过穷举枚举验证，且复现了2002年的表格。第二个应用是逻辑锁定网表的密钥计数，其中候选对象是密钥，观测值是预言机响应。在门级因子图上运行相同的递归，可计算与一组查询保持一致的密钥数量；在TrustHub混淆版本的70个实例中，存活熵每次都低于所声明的密钥长度。这两个应用是同一方法的体现：一个见证提供观测值，每次观测都会移除候选对象，且版本空间被精确计数。
英文摘要
Many questions about a digital circuit take the same form. A hidden object is consistent with a set of observations, and one wants to know how many remain consistent and which observation to make next. The set of surviving candidates is the version space, and its size, on a logarithmic scale, measures how much the observations have settled. This paper develops the version-space view as one method and applies it to two circuit-analysis problems usually treated as unrelated. The first is probabilistic combinational equivalence checking, where the candidates are Boolean functions and the observations are modified-Haar spectral coefficients. A method proposed in 2002 posed this counting problem and solved only two special cases, leaving the general case an enumeration exponential in the number of observations. We close it. A reparameterization onto block sums turns the dependence among nested coefficients into locality, a sum--product recursion counts the surviving functions exactly in time polynomial in the truth-table size, closed forms follow for a single coefficient, a coefficient pair, and every ancestor-closed set, and the error of the independence approximation the 2002 work resorted to equals a computable lattice index. Every formula is checked against exhaustive enumeration and reproduces the 2002 tables. The second application is key counting for logic-locked netlists, where the candidates are keys and the observations are oracle responses. The same recursion, run over the gate-level factor graph, computes the number of keys still consistent with a set of queries; across seventy instances of the TrustHub obfuscation release the surviving entropy falls below the advertised key length every time. The two applications are one method: a witness supplies observations, each removes candidates, and the version space is counted exactly.
Comments23 pages, 3 figures. Code: https://github.com/mitch-thornton/locked-logic-key-counting, archived at https://doi.org/10.5281/zenodo.22218068
