Modular Static Analysis of String Manipulations in C Programs

  • Matthieu JournaultEmail author
  • Antoine Miné
  • Abdelraouf Ouadjaout
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)


We present a modular analysis able to tackle out-of-bounds accesses in C strings. This analyzer is modular in the sense that it infers and tabulates (for reuse) input/output relations, automatically partitioned according to the shape of the input state. We show how the inter-procedural iterator discovers and generalizes contracts in order to improve their reusability for further analysis. This analyzer was implemented and was able to successfully analyze and infer relational contracts for functions such as strcpy, strcat.

Supplementary material


  1. 1.
    Allamigeon, X., Godard, W., Hymans, C.: Static analysis of string manipulations in critical embedded C programs. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 35–51. Springer, Heidelberg (2006). Scholar
  2. 2.
    Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 221–239. Springer, Heidelberg (2006). Scholar
  3. 3.
    Berdine, J., Calcagno, C., O’Hearn, P.W.: Smallfoot: modular automatic assertion checking with separation logic. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 115–137. Springer, Heidelberg (2006). Scholar
  4. 4.
    Bourdoncle, F.: Abstract interpretation by dynamic partitioning. J. Funct. Prog. 2(4), 407–423 (1992)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Calcagno, C., et al.: Moving fast with software verification. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 3–11. Springer, Cham (2015). Scholar
  6. 6.
    Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the Second International Symposium on Programming, pp. 106–130. Dunod, Paris (1976)Google Scholar
  7. 7.
    Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E.J. (ed.) IFIP Conference on Formal Description of Programming Concepts, St-Andrews, N.B., CA, pp. 237–277, North-Holland (1977)Google Scholar
  8. 8.
    Cousot, P.: Verification by abstract interpretation. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 243–268. Springer, Heidelberg (2003). Scholar
  9. 9.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, pp. 238–252. ACM (1977)Google Scholar
  10. 10.
    Cousot, P., Cousot, R.: Static determination of dynamic properties of generalized type unions. In: Language Design for Reliable Software, pp. 77–94 (1977)Google Scholar
  11. 11.
    Cousot, P., Cousot, R.: Modular static program analysis. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 159–179. Springer, Heidelberg (2002). Scholar
  12. 12.
    Cousot, P., et al.: Combination of abstractions in the ASTRÉE static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 272–300. Springer, Heidelberg (2007). Scholar
  13. 13.
    Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: Ball, T., Sagiv, M. (eds.) Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, 26–28 January 2011, pp. 105–118. ACM (2011)Google Scholar
  14. 14.
    Cousot, P., Cousot, R., Logozzo, F.: Precondition inference from intermittent assertions and application to contracts on collections. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 150–168. Springer, Heidelberg (2011). Scholar
  15. 15.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, pp. 84–96. ACM Press (1978)Google Scholar
  16. 16.
    Dor, N., Rodeh, M., Sagiv, M.: Cleanness checking of string manipulations in C programs via integer analysis. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 194–212. Springer, Heidelberg (2001). Scholar
  17. 17.
    Fähndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10–30. Springer, Heidelberg (2011). Scholar
  18. 18.
    Miné, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Irwin, M.J., De Bosschere, K. (eds.) Proceedings of the 2006 ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2006), Ottawa, Ontario, Canada, 14–16 June 2006, pp. 54–63. ACM (2006)Google Scholar
  19. 19.
    Müller-Olm, M., Seidl, H.: Analysis of modular arithmetic. ACM Trans. Program. Lang. Syst. 29(5), 29 (2007)CrossRefGoogle Scholar
  20. 20.
    Sharma, T., Reps, T.: A new abstraction framework for affine transformers. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 342–363. Springer, Cham (2017). Scholar
  21. 21.
    Simon, A.: Value-Range Analysis of C Programs: Towards Proving the Absence of Buffer Overflow Vulnerabilities. Springer, London (2008)Google Scholar
  22. 22.
    Simon, A., King, A.: Analyzing string buffers in C. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 365–380. Springer, Heidelberg (2002). Scholar
  23. 23.
    Sotin, P., Jeannet, B.: Precise interprocedural analysis in the presence of pointers to the stack. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 459–479. Springer, Heidelberg (2011). Scholar
  24. 24.
    Wagner, D.A., Foster, J.S., Brewer, E.A., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Proceedings of the Network and Distributed System Security Symposium, NDSS 2000, San Diego, California, USA. The Internet Society (2000)Google Scholar
  25. 25.
    Wilander, J., Kamkar, M.: A comparison of publicly available tools for dynamic buffer overflow prevention. In: Proceedings of the Network and Distributed System Security Symposium, NDSS 2003, San Diego, California, USA. The Internet Society (2003)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Matthieu Journault
    • 1
    Email author
  • Antoine Miné
    • 1
  • Abdelraouf Ouadjaout
    • 1
  1. 1.Sorbonne Université, CNRS, Laboratoire d’Informatique de Paris 6, LIP6ParisFrance

Personalised recommendations