Advertisement

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)

Abstract

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

References

  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).  https://doi.org/10.1007/11823230_4CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/11823230_15CrossRefGoogle 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).  https://doi.org/10.1007/11804192_6CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-17524-9_1CrossRefGoogle 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).  https://doi.org/10.1007/978-3-540-39910-0_11CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/3-540-45937-5_13CrossRefGoogle 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).  https://doi.org/10.1007/978-3-540-77505-8_23CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-18275-4_12CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/3-540-47764-0_12CrossRefzbMATHGoogle 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).  https://doi.org/10.1007/978-3-642-18070-5_2CrossRefGoogle 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).  https://doi.org/10.1007/978-3-319-66706-5_17CrossRefGoogle 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).  https://doi.org/10.1007/3-540-45719-4_25CrossRefGoogle 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).  https://doi.org/10.1007/978-3-642-19718-5_24CrossRefGoogle 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