Research On Data Security Of Propositional Satisfiability Problem In Formal Verification

Propositional satisfiability(abbreviated as SAT)is the problem that search for a satisfying assignment for a particular propositional formula in CNF format.It is an important problem in computer science and engineering,widely employed in software and hardware verification.Because of the quick increasing size of software and hardware system,the size of the formula to be solved by SAT is also growing very quickly.Thus,solving SAT problem with the flexible computing resource provided by cloud or grid in open computing environment is an efficient approach to overcome such challenge.However,unauthorized access to confidential information in such open environment is another serious challenge.Existing researches focus on protecting confidential information with fully homomorphic encryption.But the complex and expensive encrypting operations make this approach unrealistic.To resolve this problem,this dissertation studies how to protect the structure of the formula and the final result with acceptable performance for solving SAT formulas from software and hardware verification.These proposed approaches obfuscate the SAT formula by inserting noise data to hide the formula structure and the final result,while preserving the consistency of the solution space,such that the final result can be recovered from the obfuscated formula.In this way,the obfuscated SAT formulas can be solved directly by existing highly optimized SAT solvers.The proposed approaches are:1.Solving SAT problem in open environment with noise based obfuscation.Existing approaches in protecting CNF formula include those based on encryption and those based on data partition.These approaches all rely on enumerating satisfying assignment(ALLSAT),which make them very inefficient.By analyzing the CNF structure,this dissertation proposes noise based obfuscation.This approach seamlessly inserts noise formula into origin formula,to hide the original formula's structure,while preserving the CNF format and solution space,such that the obfuscated formula can be solved with existing SAT solvers.This approach achieves pretty good balance between efficiency and privacy protection.This dissertation proves its correctness with some theorems and shows its efficiency with experimental result.2.Structure-aware obfuscation.The difficulty of recognizing CNF formula's structure is an important metric in measuring the obfuscating algorithm's effectiveness.This dissertation studies the structure of CNF formulas from hardware designs,and proposes a structure-aware approach to insert noise.This approach maps the original formula's structure into new structure with noise,such that these is no explicit relation between the original and the new formula.In this way,it is much more complicated to recover the original structure.This dissertation prove the effectiveness of this approach,and show its efficiency with experimental result.3.CNF obfuscation based on solution space projection equivalence.The algorithm that enumerates a CNF formula's all solution is called ALLSAT.ALLSAT algorithm is an serious challenge to our obfuscation algorithms discussed above,because ALLSAT can find out all variables with the same assignment in all satisfying assignments,and take them as candidate noise variables,and then further identify the original formula.To overcome this problem,this dissertation proposes CNF obfuscation based on solution space projection equivalence,to relax the requirement that noise variables must have the same assignments in all satisfying assignments.In this way,our approach can resist the attack from ALLSAT solver.4.CNF obfuscation based on customization of solution.This dissertation further studies how to hide the result of SAT solving by proposing CNF obfuscation based on over-approximation of solution space.This approach expands the solution space of noise formula,such that the solution space of the resulted formula is an over-approximation of the original formula.This dissertation proves the correctness of this approach,and shows its efficiency and effectiveness with experimental result.Because the CNF obfuscation based on over-approximation may call the SAT solver for multiple times,and the possibility of such calling depends on the ratio of original solution to noise solution.So this dissertation further propose to combine projection equivalence and over-approximation approaches mentioned above.5.Iterative characterizing algorithm based on cofactoring and Craig interpolant.This dissertation proposes an iterative characterizing algorithm based on cofactoring and Craig interpolant.In inferring the encoder's internal structure and generating its decoder,one of the most critical algorithm is to characterize a Boolean function f that covers a Boolean relation R.State-of-the-art algorithms are satisfying assignment enumeration and quantifier elimination with SAT or BDD.But these algorithms are very inefficient because of irregular solution space.Thus we propose an iterative characterizing algorithm.In each iteration of this algorithm,for each satisfying assignment A not yet enumerated,R is simplified with A's cofactor,and used to generated a Craig interpolant,which can is an enlarged cube of A.This algorithm is a halting one and is much faster than naive satisfying assignment enumeration.This dissertation studies extensively many important problem in outsouring SAT solving,and proposes many solutions that are highly efficient and effective.This dissertation further show the efficiency and effectiveness of these approaches with theoretical analysis and experimental result.These research results are of very important in both theoretical and application fields.