Advertisement

Optimal Guard Synthesis for Memory Safety

  • Thomas Dillig
  • Isil Dillig
  • Swarat Chaudhuri
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

Abstract

This paper presents a new synthesis-based approach for writing low-level memory-safe code. Given a partial program with missing guards, our algorithm synthesizes concrete predicates to plug in for the missing guards such that all buffer accesses in the program are memory safe. Furthermore, guards synthesized by our technique are the simplest and weakest among guards that guarantee memory safety, relative to the inferred loop invariants. Our approach is fully automatic and does not require any hints from the user. We have implemented our algorithm in a prototype synthesis tool for C programs, and we show that the proposed approach is able to successfully synthesize guards that closely match hand-written programmer code in a set of real-world C programs.

Keywords

Memory Access Synthesis Problem Pointer Arithmetic Loop Body Program Synthesis 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. 1.
    Berdine, J., Cook, B., Ishtiaq, S.: sLAyer: Memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178–183. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  2. 2.
    Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: Checking memory safety with blast. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 2–18. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  3. 3.
    Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamarić, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 19–33. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  4. 4.
    Dillig, I., Dillig, T., Aiken, A.: Fluid updates: Beyond strong vs. Weak updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 246–266. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  5. 5.
    Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL, pp. 289–300 (2009)Google Scholar
  6. 6.
    Dillig, I., Dillig, T., Li, B., McMillan, K.: Inductive invariant generation via abductive inference. In: OOPSLA, pp. 443–456. ACM (2013)Google Scholar
  7. 7.
    Li, B., Dillig, I., Dillig, T., McMillan, K., Sagiv, M.: Synthesis of circular compositional program proofs via abduction. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 370–384. Springer, Heidelberg (2013)Google Scholar
  8. 8.
    Alur, R., Bodik, R., Juniwal, G., Martin, M.M., Raghothaman, M., Seshia, S., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: FMCAD (2013)Google Scholar
  9. 9.
    Solar-Lezama, A.: The sketching approach to program synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 4–13. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  10. 10.
    Srivastava, S., Gulwani, S., Foster, J.S.: Template-based program verification and program synthesis. STTT 15(5-6), 497–518 (2013)CrossRefGoogle Scholar
  11. 11.
    Srivastava, S., Gulwani, S., Chaudhuri, S., Foster, J.: Path-based inductive synthesis for program inversion. In: PLDI, pp. 492–503 (2011)Google Scholar
  12. 12.
    Dillig, I., Dillig, T.: explain: A tool for performing abductive inference. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 684–689. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  13. 13.
    Dillig, I., Dillig, T., Aiken, A.: SAIL: Static Analysis Intermediate Language. Stanford University Technical ReportGoogle Scholar
  14. 14.
  15. 15.
    Openssh 5.3p1, http://www.openssh.com/:
  16. 16.
    Vechev, M., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: POPL, pp. 327–338 (2010)Google Scholar
  17. 17.
    Seshia, S.: Sciduction: combining induction, deduction, and structure for verification and synthesis. In: DAC, pp. 356–365 (2012)Google Scholar
  18. 18.
    Srivastava, S., Gulwani, S., Foster, J.: From program verification to program synthesis. In: POPL, pp. 313–326 (2010)Google Scholar
  19. 19.
    Beyene, T., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: POPL (2014)Google Scholar
  20. 20.
    Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  21. 21.
    Jha, S., Seshia, S., Tiwari, A.: Synthesis of optimal switching logic for hybrid systems. In: 2011 Proceedings of the International Conference on Embedded Software (EMSOFT), pp. 107–116 (2011)Google Scholar
  22. 22.
    Chaudhuri, S., Solar-Lezama, A.: Smooth interpretation. In: PLDI (2010)Google Scholar
  23. 23.
    Chaudhuri, S., Clochard, M., Solar-Lezama, A.: Bridging boolean and quantitative synthesis using smoothed proof search. In: POPL (2014)Google Scholar
  24. 24.
    Younan, Y., Joosen, W., Piessens, F.: Runtime countermeasures for code injection attacks against c and c++ programs. ACM Comput. Surv. 44(3), 17 (2012)CrossRefGoogle Scholar
  25. 25.
    Dhurjati, D., Kowshik, S., Adve, V., Lattner, C.: Memory safety without runtime checks or garbage collection. In: LCTES 2003, pp. 69–80 (2003)Google Scholar
  26. 26.
    Balakrishnan, G., Reps, T.: Analyzing memory accesses in x86 executables. In: Duesterwald, E. (ed.) CC 2004. LNCS, vol. 2985, pp. 5–23. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  27. 27.
    Condit, J., Harren, M., Anderson, Z., Gay, D.M., Necula, G.C.: Dependent types for low-level programming. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 520–535. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  28. 28.
    Beyer, D., Henzinger, T.A., Jhala, R., Majumdar, R.: Checking memory safety with blast. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 2–18. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  29. 29.
    Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385–398. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  30. 30.
    Berdine, J., Cook, B., Ishtiaq, S.: sLAyer: Memory safety for systems-level code. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 178–183. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  31. 31.
    Wagner, D., Foster, J.S., Brewer, E.A., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Network and Distributed System Security Symposium, pp. 3–17 (2000)Google Scholar
  32. 32.
    Necula, G.C., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy code. In: POPL, pp. 128–139 (2002)Google Scholar
  33. 33.
    Jim, T., Morrisett, J.G., Grossman, D., Hicks, M.W., Cheney, J., Wang, Y.: Cyclone: A safe dialect of c. In: USENIX Annual Technical Conference, General Track, pp. 275–288 (2002)Google Scholar
  34. 34.
    Distefano, D., Filipović, I.: Memory leaks detection in java by bi-abductive inference. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol. 6013, pp. 278–292. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  35. 35.
    Botinčan, M., Distefano, D., Dodds, M., Grigore, R., Parkinson, M.J.: corestar: The core of jstar. In. In: Boogie. Citeseer (2011)Google Scholar
  36. 36.
    Dillig, I., Dillig, T., Aiken, A.: Automated error diagnosis using abductive inference. In: PLDI, pp. 181–192. ACMGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Thomas Dillig
    • 1
  • Isil Dillig
    • 1
  • Swarat Chaudhuri
    • 2
  1. 1.UT AustinUSA
  2. 2.Rice UniversityUSA

Personalised recommendations