Outsourcing SAT-based Verification Computations in Network Security

TL;DR

This paper introduces novel methods for randomizing SAT instances to enable secure outsourcing of complex computations like circuit verification and network analysis in cloud environments, ensuring privacy and correctness.

Contribution

The paper presents new randomization techniques for SAT problems, including variable and instance randomization, applicable to real-world security-sensitive cloud computing tasks.

Findings

Methods are correct and feasible

Techniques are scalable and general

Applicable to real-world problems

Abstract

The emergence of cloud computing gives huge impact on large computations. Cloud computing platforms offer servers with large computation power to be available for customers. These servers can be used efficiently to solve problems that are complex by nature, for example, satisfiability (SAT) problems. Many practical problems can be converted to SAT, for example, circuit verification and network configuration analysis. However, outsourcing SAT instances to the servers may cause data leakage that can jeopardize system's security. Before outsourcing the SAT instance, one needs to hide the input information. One way to preserve privacy and hide information is to randomize the SAT instance before outsourcing. In this paper, we present multiple novel methods to randomize SAT instances. We present a novel method to randomize the SAT instance, a variable randomization method to randomize the solution set, and methods to randomize Mincost SAT and MAX3SAT instances. Our analysis and evaluation show the correctness and feasibility of these randomization methods. The scalability and generality of our methods make it applicable for real world problems.