Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Outsourcing SAT-based Verification Computations in Network Security

Qi Duan, Ehab Al-Shaer

TL;DR

This work addresses privacy concerns in outsourcing SAT-based verification to cloud services by introducing a suite of randomization and derandomization techniques that preserve satisfiability while obscuring the original problem. It presents methods such as permutation/negation, matrix multiplication with a full-rank random matrix, and solution-set randomization, along with extensions to Mincost SAT and MAX3SAT, plus verification strategies. A firewall equivalence checking case study grounds the approach in a practical network security problem, and empirical evaluation demonstrates feasible overhead for real-world use. The results suggest that privacy-preserving SAT outsourcing can be realistically deployed, with future work aimed at broader applications and interactive platforms.

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.

Outsourcing SAT-based Verification Computations in Network Security

TL;DR

This work addresses privacy concerns in outsourcing SAT-based verification to cloud services by introducing a suite of randomization and derandomization techniques that preserve satisfiability while obscuring the original problem. It presents methods such as permutation/negation, matrix multiplication with a full-rank random matrix, and solution-set randomization, along with extensions to Mincost SAT and MAX3SAT, plus verification strategies. A firewall equivalence checking case study grounds the approach in a practical network security problem, and empirical evaluation demonstrates feasible overhead for real-world use. The results suggest that privacy-preserving SAT outsourcing can be realistically deployed, with future work aimed at broader applications and interactive platforms.

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.

Paper Structure

This paper contains 19 sections, 4 theorems, 23 equations, 4 tables.

Table of Contents

  1. Introduction
  2. Motivation
  3. Computational Model, Adversary Model and Requirements for SAT Outsourcing
  4. Computational Model
  5. Adversary Model
  6. Classification of Outsourcing Security
  7. Randomizing SAT Instances
  8. Permutation of Variables and Negation Flipping
  9. Matrix Multiplication Randomization
  10. Solution Set Randomization
  11. Randomizing Mincost SAT
  12. Randomizing MAX3SAT
  13. Verification of the Correctness of the Result
  14. Outsourcing Multi-party SAT-based Computation
  15. Case Study: Firewall Equivalence Checking
  16. ...and 4 more sections

Key Result

Theorem 1

Full Outsourcing-Security Let $Alg$ be an algorithm with outsource input/output. A pair of algorithms $(C,S)$ is said to be an outsource-secure implementation of $Alg$ if: 1. Correctness: $C^S$ is a correct implementation of $Alg$. 2. Security: For all probabilistic polynomial-time adversaries $A =

Theorems & Definitions (6)

  • Theorem 1
  • Theorem 2
  • Theorem 1
  • proof
  • Theorem 2
  • proof