Static Analysis with Set-Closure in Secrecy

Abstract. We report that the homomorphic encryption scheme can unleash the possibility of static analysis of encrypted programs. Static analysis in cipher-world is desirable in the static-analysis-as-a-service setting, because it allows the program owners to encrypt and upload their programs to the static analysis service while the service provider can still analyze the encrypted programs without decrypting them. Only the owner of the decryption key (the program owner) is able to decrypt the analysis result. As a concrete example, we describe how to perform a pointer analysis in secrecy. In our method, a somewhat homomorphic encryption scheme of depth O(log m) is able to evaluate a simple pointer analysis with O(log m) homomorphic matrix multiplications, for the number m of pointer variables when the maximal pointer level is bounded. We also demonstrate the viability of our method by implementing the pointer analysis in secrecy.

• Type: Journal
• Year: 2015
• Where: SAS
• Authors: Woosuk Lee, Hyunsook Hong, Kwangkeun Yi, Jung Hee Cheon
• Keywords: Formal Methods, SAS 2015