lengths compared to the manually constructed one in the work of Ghalaty et al. 9

Conclusion

Search-based program synthesis promises to be a useful tool for future program development environments. Programming by examples in domain-specific applications and semantics-preserving optimization of program fragments to satisfy performance goals expressed via syntactic criteria are already proving to be its interesting applications. Our experience shows that investing in the infrastructure—standardized input formats, collection of benchmarks, open-source prototype solvers, and a competition of solvers—has been vital in advancing the state of the of art. Finally, improving the scalability of SyGuS solvers is an active area of current research, and in particular, a promising research direction is to explore how these solvers can benefit from modern machine learning technology (see, for example, Devlin et al. 6 for the use of neural networks for learning programs from input-to-output examples).

 

References

1. Akiba, T., Imajo, K., Iwami, H., Iwata, Y., Kataoka, T., Takahashi, N., Mmoskal, M., Swamy, N. Calibrating research in program synthesis using 72,000 hours of programmer time. Technical Report, MSR, 2013.

2. Alur, R., Bodík, R., Juniwal, G., Martin, M. M. K., Raghothaman, M., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.

Syntax-guided synthesis. In Proc. FMCAD,

2013, 1–17.

3. Alur, R., Radhakrishna, A., Udupa, A. Scaling enumerative program synthesis via divide and conquer. In Proc. TACAS, LNCS 10205, 2017,

319–336.

4. Clarke, E., Grumberg, O., Peled, D. Model Checking.

MIT Press, 2000.

5. de Moura, L., Bjørner, N. Satisfiability Modulo Theories: Introduction and applications. Commun. ACM 54, 9

(2011), 69–77.

6. Devlin, J., Uesato, J., Bhupatiraju, S., Singh, R., Mohamed, A., Kohli, P. Robustfill: Neural program learning under noisy I/O. In Proc. ICML, 2017, 990–998.

7. Eldib, H., Wu, M., Wang, C. Synthesis of fault-attack countermeasures for cryptographic circuits. In Proc.

CAV, LNCS 9780, 2016, 343–363.

8. Garg, P., Löding, C., Madhusudan, P., Neider, D. ICE: A robust framework for learning invariants. In Proc.

CAV, LNCS 8559, 2014, 69–87.

9. Ghalaty, N., Aysu, A., Schaumont, P. Analyzing and eliminating the causes of fault sensitivity analysis.

In Proc. DATE, 2014, 1–6.

10. Gulwani, S. Automating string processing in spreadsheets using input–output examples. In Proc.

POPL, 2011, 317–330.

11. Gulwani, S., Harris, W.R., Singh, R. Spreadsheet data manipulation using examples. Commun. ACM, 55, 8

(2012), 97–105.

12. Gulwani, S., Jha, S., Ti wari, A., Venkatesan, R. Synthesis of loop-free programs. In Proc. PLDI, 2011, 62–73.

13. Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.

Oracle-guided component-based program synthesis.

In Proc. ICSE, 2010, 215–224.

14. Kuncak, V., Mayer, M., Piskac, R., Suter, P. Software synthesis procedures. Commun. ACM, 55, 2.

15. Le, X. D., Chu, D., Lo, D., Le Goues, C., Visser, W. S3: Syntax- and semantic-guided repair synthesis via programming by examples. In Proc. FSE, 2017,

593–604.

16. Malik, S., Zhang, L. Boolean satisfiability: From theoretical hardness to practical success. Commun.

ACM, 52, 8 (2009), 76–82.

17. Manna, Z., Waldinger, R. Fundamentals of deductive program synthesis. IEEE Trans. Softw. Eng. 18, 8

(1992), 674–704.

18. Massalin, H. Superoptimizer – A look at the smallest program. In Proc. ASPLOS, 1987, 122–126.

19. Mechtaev, S., Yi, J., Roychoudhury, A. Angelix: Scalable multiline program patch synthesis via symbolic analysis. In Proc. ICSE, 2016, 691–701.

20. Mitchell, T. Machine Learning. McGraw-Hill, 1997.

21. Osera, P., Zdancewic, S. Type-and-example-directed program synthesis. In Proc. PLDI, 2015, 619–630.

22. Polikarpova, N., Kuraj, I., Solar-Lezama, A. Program synthesis from polymorphic refinement types. In

Proc. PLDI, 2016, 522–538.

23. Quinlan, J. Introduction to decision trees. Mach.

Learn. 1, 1 (1986), 81–106.

24. Raychev, V., Vechev, M. T., Yahav, E. Code completion with statistical language models. In Proc. PLDI, 2014,

419–428.

25. Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C. W. Counterexample-guided quantifier instantiation for synthesis in SMT. In Proc. CAV, 2015, 198–216.

26. Schkufza, E., Sharma, R., Aiken, A. Stochastic program optimization. Commun. ACM 59, 2 (2016), 114–122.

27. Seshia, S.A. Combining induction, deduction, and structure for verification and synthesis. Proc. IEEE

103, 11 (2015), 2036–2051.

28. Solar-Lezama, A. Program sketching. S TTT 15, 5–6

(2013), 475–495.

29. Solar-Lezama, A., Rabbah, R., Bodík, R., Ebcioglu, K.

Programming by sketching for bit-streaming programs. In Proc. PLDI, 2005, 281–294.

30. Srivastava, S., Gulwani, S., Foster, J. S. Template-based program verification and program synthesis.

STTT 15, 5–6 (2013), 497–518.

31. Stump, A., Sutcliffe, G., Tinelli, C. Starexec: A cross-community infrastructure for logic solving. In

Proc. IJCAR, 2014, 367–373.

32. Udupa, A., Raghavan, A., Deshmukh, J., Mador-Haim, S., Martin, M., Alur, R. TRANSIT: Specifying protocols with concolic snippets. In Proc. PLDI, 2013, 287–296.

33. Warren, H. S. Hacker’s Delight. Addison-Wesley, 2002.

 

Rajeev Alur is the Zisman Family Professor in the Department of Computer and Information Sciences at the University of Pennsylvania, Philadelpha, PA, USA.

Rishabh Singh is a research scientist at Google Brain, Mountain View, CA, USA.

Dana Fisman is a senior lecturerat Ben Gurion University, Be’er Shera, Israel.

Armando Solar-Lezama is an associate professor and leader of the Computer Assisted Programming Group at MI T, Cambridge, MA, USA.

©2018 ACM 0001-0782/18/12 $15.00.

secret key, the public inputs can correspond to a message, and the output can be the encryption of the message using the secret key. Such cryptographic circuits are commonplace in encryption systems used in practice. One possible attack, that is, a strategy for the attacker to gain information about the private inputs despite the established logical correctness of the circuit, is based on measuring the time it takes for the circuit to compute. For instance, when a public input bit changes from 1 to 0, a specific output bit is guaranteed to change from 1 to 0 independent of whether a particular private input bit is 0 or 1, but may change faster when this private input is 0, thus leaking information. Such vulnerabilities do occur in practice, and in fact, Ghalaty et al. 9 reports such an attack on a circuit used in the AES encryption standard. The timing attack is not possible if the circuit meets the so-called structural property of being constant time: A constant-time circuit is the one in which the length of all input-to-output paths measured in terms of number of gates are the same. After identifying the attack, Ghalaty et al. 9 shows how to convert the given circuit to an equivalent constant-time circuit by introducing delay elements on shorter paths.

As noted in the work of Eldib et al., 7 being constant-time is a syntactic constraint on the logical representation of a circuit, that is, it depends on the structure of the expression and not on the operators used in the construction. As a result, given a circuit C, synthesizing another circuit C′ such that C′ is a constant-time circuit and is functionally equivalent to C can be formalized as a SyGuS problem. The set of all constant-time circuits with all input-to-output path lengths within a given bound can be expressed using a context-free grammar and being logically equivalent to the original circuit can be expressed as a Boolean formula involving the unkno wn circuit. Eldib et al. 7 then use the EUSolver to automatically synthesize constant-time circuits that are logically equivalent to given cryptographic circuits, and in particular, report a solution that is smaller in terms of overall size as well as path