Secure and trusted partial grey-box verification

  • Yixian Cai
  • George KarakostasEmail author
  • Alan Wassyng
Regular Contribution


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.


Verification Secure testing Grey-box verification Tabular expressions 


Supplementary material


  1. 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. 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. 3.
    Gentry, C.: A fully homomorphic encryption scheme. Ph.D. thesis, Stanford University (2009)Google Scholar
  4. 4.
    Naor, M.: Bit commitment using pseudorandomness. J. Cryptol. 4(2), 151 (1991)CrossRefzbMATHGoogle Scholar
  5. 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. 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. 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. 8.
    Chaki, S., Schallhart, C., Veith, H.: Verification across intellectual property boundaries. ACM Trans. Softw. Eng. Methodol. (TOSEM) 22, 15 (2013)CrossRefGoogle Scholar
  9. 9.
    Lynn, B., Prabhakaran, M., Sahai, A.: Positive results and techniques for obfuscation. In: EUROCRYPT 2004, pp. 20–39. Springer (2004)Google Scholar
  10. 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. 11.
    Goldwasser, S., Kalai, Y.T., Rothblum, G.N.: One-time programs. In: CRYPTO 2008, pp. 39–56. Springer (2008)Google Scholar
  12. 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. 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. 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. 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. 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. 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. 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. 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. 20.
    Arora, S., Safra, S.: Probabilistic checking of proofs: a new characterization of NP. J. ACM (JACM) 45(1), 70 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Wassyng, A., Janicki, R.: Tabular expressions in software engineering. Fundam. Inf. 67, 343 (2005)zbMATHGoogle Scholar
  22. 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. 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. 24.
    Katz, J., Lindell, Y.: Introduction to Modern Cryptography. CRC Press, Boca Raton (2014)zbMATHGoogle Scholar
  25. 25.
    FIPS: Data Encryption Standard. NBS 46 (1977)Google Scholar
  26. 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. 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. 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. 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. 30.
    Acar, A., Aksu, H., Uluagac, A.S.: C. M.: A survey on homomorphic encryption schemes: theory and implementation (2017). arxiv: 1704.03578
  31. 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. 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

Copyright information

© Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  1. 1.Department of Computing and SoftwareMcMaster UniversityHamiltonCanada

Personalised recommendations