BlindMarket: Enabling Verifiable, Confidential, and Traceable IP Core Distribution in Zero-Trust Settings

Abstract

We present BlindMarket, an end-to-end zero-trust distribution framework for hardware IP cores. BlindMarket allows two parties, the IP user and the IP vendor, to complete an IP trading process with strong guarantees of verifiability and confidentiality before the transaction, and then traceability after. We propose verification heuristics and adapt the cone of influence-based design pruning to overcome the limited scalability common to cryptographic protocols and the hardness of the underlying hardware verification. We systematically evaluate our framework on a diverse set of real-world hardware benchmarks, and the results demonstrate that BlindMarket effectively completes across a diverse set of real-world hardware IP cores, demonstrating successful verification on 12 out of 13 designs and substantial performance improvements enabled by design pruning and control-flow guided heuristics.

Figures (8)

• Figure 1: End-to-end workflow of secure IP verification and licensing in BlindMarket, organized into four phases. (1) In the preprocessing phase, the vendor encodes each IP core into CNF and masks it using randomness, while the user encodes the verification property. (2) During oblivious design selection, the user retrieves the masked CNF of the selected design via 1-out-of-$N$ OT, without revealing the selection to the vendor. (3) In the secure design verification phase, the vendor and user engage in a 2PC protocol to reconstruct the selected design and jointly verify it against the property using hw-ppSAT. (4) Finally, if verification succeeds, the vendor issues a certificate bound to the authorized user and selected IP, publishing it to the ledger for traceability.
• Figure 2: Secure hardware design verification workflow in BlindMarket. The vendor masks each CNF-encoded design using random matrices, and the user selects a target design via oblivious transfer (OT), receiving only the masked version. The vendor and user then run a 2PC protocol to reconstruct the selected design and combine it with the user’s property to form $\psi = \phi_i \land \neg\varphi$. The satisfiability of $\psi$ is evaluated using hw-ppSAT under 2PC, revealing only the final result to both parties while preserving mutual confidentiality.
• Figure 3: Illustration of two signal prioritization principles. In (a), the control signal ctrl is prioritized during branching, since assigning ctrl to false renders the values of a and $\texttt{c}$ irrelevant to the satisfiability of the encoded design. In (b), for two control signals ctrl1 and ctrl2, ctrl2 is prioritized, because once ctrl2 is assigned false, ctrl1 no longer influences the evaluation.
• Figure 4: When the circuit is unrolled, later-stage control signals dominate earlier-stage ones. Thus $\texttt{enable}_2$ dominates $\texttt{reset}_1$. Based on Principle 2, $\texttt{reset}_1$ dominates $\texttt{enable}_1$. Consequently, the priority chain becomes $\texttt{enable}_2 \succ \texttt{reset}_1 \succ \texttt{enable}_1$.
• Figure 5: Illustrates the performance ratio between (generic)ppSAT and (our) hw-ppSAT across various (pruned) benchmarks. Each segment represents a specific design, with the outer boundary (ratio = 1.0) indicating the baseline solving time of ppSAT. The shaded region corresponds to hw-ppSAT; a smaller area indicates a greater speedup. As shown, most designs experience a substantial reduction in solving time, with normalized ratios significantly below 1.0. In the best-case scenario, our method achieves a remarkable speedup with a ratio as low as 0.0098.