# Secure and trusted partial grey-box verification

- 18 Downloads

## Abstract

A crucial aspect in the development of software-intensive systems is *verification*. This is the process of checking whether the system has been implemented in compliance with its specification. In many situations, the manufacture of one or more components of the system is outsourced. We study the case of how a third party (the *verifier*) can verify an outsourced component effectively, without access to all the details of the internal design of that component built by the *developer*. We limit the design detail that is made available to the verifier to a diagram of interconnections between the different design units within the component, but encrypt the design details within the units and also the intermediate values passed between the design units. We formalize this notion of limited information using tabular expressions to describe the functions in both the specifications and the design. The most common form of verification is testing, and it is known that black-box testing of the component is not effective enough in deriving test cases that will adequately determine the correctness of the implementation, and the safety of its behaviour. We have developed protocols that allow for the derivation of test cases that take advantage of the design details disclosed as described above. We can regard this as *partial grey-box testing* that does not compromise the developer’s secret information. Our protocols work with both trusted and untrusted developers, as well as trusted and untrusted verifiers, and allow for the checking of the correctness of the verification process itself by any third party, and at any time. Currently our results are derived under the simplifying assumption that the software design units are linked acyclically. We leave the lifting of this assumption as an open problem for future research.

## Keywords

Verification Secure testing Grey-box verification Tabular expressions## Notes

## Supplementary material

## References

- 1.Alspaugh, T.A., Faulk, S.R., Britton, K.H., Parker, R.A., Parnas, D.L.: Software requirements for the A-7E aircraft. Tech. Rep, DTIC Document (1992)Google Scholar
- 2.Hayhurst, K.J., Veerhusen, D.S., Chilenski, J.J., Rierson, L.K.: A practical tutorial on modified condition/decision coverage. Tech. Rep. TM-2001-210876, NASA (2001)Google Scholar
- 3.Gentry, C.: A fully homomorphic encryption scheme. Ph.D. thesis, Stanford University (2009)Google Scholar
- 4.Naor, M.: Bit commitment using pseudorandomness. J. Cryptol.
**4**(2), 151 (1991)CrossRefzbMATHGoogle Scholar - 5.Collberg, C., Thomborson, C., Low, D.: A taxonomy of obfuscating transformations. Department of Computer Science, The University of Auckland, New Zealand, Tech. Rep. (1997)Google Scholar
- 6.Wang, C., Hill, J., Knight, J., Davidson, J.: Software tamper resistance: obstructing static analysis of programs. Tech. Rep. CS-2000-12, University of Virginia (2000)Google Scholar
- 7.Barak, B., Goldreich, O., Impagliazzo, R., Rudich, S., Sahai, A., Vadhan, S., Yang, K.: On the (im)possibility of obfuscating programs. In: CRYPTO 2001, pp. 1–18. Springer (2001)Google Scholar
- 8.Chaki, S., Schallhart, C., Veith, H.: Verification across intellectual property boundaries. ACM Trans. Softw. Eng. Methodol. (TOSEM)
**22**, 15 (2013)CrossRefGoogle Scholar - 9.Lynn, B., Prabhakaran, M., Sahai, A.: Positive results and techniques for obfuscation. In: EUROCRYPT 2004, pp. 20–39. Springer (2004)Google Scholar
- 10.Yao, A.C.: Protocols for secure computations. In: Proceedings of the 54th IEEE Annual Symposium on Foundations of Computer Science (FOCS)Google Scholar
- 11.Goldwasser, S., Kalai, Y.T., Rothblum, G.N.: One-time programs. In: CRYPTO 2008, pp. 39–56. Springer (2008)Google Scholar
- 12.Goldwasser, S., Kalai, Y., Popa, R.A., Vaikuntanathan, V., Zeldovich, N.: Reusable garbled circuits and succinct functional encryption. In: Proceedings of the 45th ACM Symposium on Theory of Computing (STOC), pp. 555–564. ACM (2013)Google Scholar
- 13.Cormode, G., Mitzenmacher, M., Thaler, J.: Practical verified computation with streaming interactive proofs. In: Proceedings of the 3rd Innovations in Theoretical Computer Science Conference, pp. 90–112. ACM (2012)Google Scholar
- 14.Thaler, J., Roberts, M., Mitzenmacher, M., Pfister, H.: Verifiable computation with massively parallel interactive proofs. In: Proceedings of the 4th USENIX Conference on Hot Topics in Cloud Computing, HotCloud’12 (2012)Google Scholar
- 15.Vu, V., Setty, S., Blumberg, A.J., Walfish, M.: A hybrid architecture for interactive verifiable computation. In: Proceeding of the 2013 IEEE Symposium on Security and Privacy, SP’13, pp. 223–237. IEEE (2013)Google Scholar
- 16.Setty, S., McPherson, R., Blumberg, A.J., Walfish, M.: Making argument systems for outsourced computation practical (sometimes). In: Proceedings of the 19th Annual Network & Distributed System Security Symposium (2012)Google Scholar
- 17.Setty, S., Vu, V., Panpalia, N., Braun, B., Blumberg, A.J., Walfish, M.: Taking proof-based verified computation a few steps closer to practicality. In: Proceedings of the 21st USENIX Conference on Security Symposium, Security’12, pp. 253–268 (2012)Google Scholar
- 18.Parno, B., Howell, J., Gentry, C., Raykova, M.: Pinocchio: Nearly practical verifiable computation. In: Proceedings of the 2013 IEEE Symposium on Security and Privacy (SP), pp. 238–252. IEEE (2013)Google Scholar
- 19.Ben-Sasson, E., Chiesa, A., Genkin, D., Tromer, E., Virza, M.: SNARKs for C: Verifying program executions succinctly and in zero knowledge. In: Proceedings of CRYPTO 2013, pp. 90–108. Springer (2013)Google Scholar
- 20.Arora, S., Safra, S.: Probabilistic checking of proofs: a new characterization of NP. J. ACM (JACM)
**45**(1), 70 (1998)MathSciNetCrossRefzbMATHGoogle Scholar - 21.Wassyng, A., Janicki, R.: Tabular expressions in software engineering. Fundam. Inf.
**67**, 343 (2005)zbMATHGoogle Scholar - 22.Malkhi, D., Nisan, N., Pinkas, B., Sella, Y.: Fairplay—a secure two-party computation system. In: Proceedings of the 13th Conference on USENIX Security Symposium SSYM’04, vol. 13, pp. 20–20 (2004)Google Scholar
- 23.Huang, Y., Evans, D., Katz, J., Malka, L.: Faster secure two-party computation using garbled circuits. In: Proceedings of the 20th USENIX Conference on Security SEC’11, pp. 35–35 (2011)Google Scholar
- 24.Katz, J., Lindell, Y.: Introduction to Modern Cryptography. CRC Press, Boca Raton (2014)zbMATHGoogle Scholar
- 25.FIPS: Data Encryption Standard. NBS 46 (1977)Google Scholar
- 26.Vaikuntanathan, V.: Computing blindfolded: new developments in fully homomorphic encryption. In: Proceedings of the 52nd IEEE Annual Symposium on Foundations of Computer Science (FOCS), pp. 5–16. IEEE (2011)Google Scholar
- 27.Gentry, C., Halevi, S., Vaikuntanathan, V.: \(i\)-hop homomorphic encryption and rerandomizable Yao circuits. In: Proceedings of CRYPTO 2010, pp. 155–172. Springer (2010)Google Scholar
- 28.Valiant, L.G.: Universal circuits (preliminary report). In: Proceedings of the 8th Annual ACM Symposium on Theory of Computing (STOC), pp. 196–203. ACM (1976)Google Scholar
- 29.Sander, T., Young, A., Yung, M.: Non-interactive cryptocomputing for NC1. In: Proceedings of the 40th Annual Symposium on Foundations of Computer Science (FOCS), pp. 554–566. IEEE (1999)Google Scholar
- 30.Acar, A., Aksu, H., Uluagac, A.S.: C. M.: A survey on homomorphic encryption schemes: theory and implementation (2017). arxiv: 1704.03578
- 31.Zhou, B., Pei, J.: Preserving privacy in social networks against neighborhood attacks. In: Proceedings of the 24th IEEE International Conference on Data Engineering, ICDE’08, pp. 506–515. IEEE (2008)Google Scholar
- 32.Cheng, J., Fu, A.W., Liu, J.: K-isomorphism: privacy preserving network publication against structural attacks. In: Proceedings of the 2010 ACM SIGMOD International Conference on Management of data, pp. 459–470. ACM (2010)Google Scholar