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