Modular Static Analysis of String Manipulations in C Programs

Matthieu Journault¹⁴,
Antoine Miné¹⁴ &
Abdelraouf Ouadjaout¹⁴

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11002))

Included in the following conference series:

International Static Analysis Symposium

1086 Accesses
11 Citations

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.

This work is supported by the European Research Council under Consolidator Grant Agreement 681393 – MOPSA.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic

$34.99 /Month

Get 10 units per month
Download Article/Chapter or eBook
1 Unit = 1 Article or 1 Chapter
Cancel anytime

Buy Now

Chapter: USD 29.95; Price excludes VAT (USA)

eBook: USD 39.99; Price excludes VAT (USA)

Softcover Book: USD 54.99; Price excludes VAT (USA)

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Relational String Abstract Domains

Symbolic String Transformations with Regular Lookahead and Rollback

String Abstract Domains and Their Combination

References

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_4
Chapter MATH Google Scholar
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_15
Chapter Google Scholar
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_6
Chapter Google Scholar
Bourdoncle, F.: Abstract interpretation by dynamic partitioning. J. Funct. Prog. 2(4), 407–423 (1992)
Article MathSciNet Google Scholar
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_1
Chapter Google Scholar
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
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
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_11
Chapter MATH Google Scholar
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
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
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_13
Chapter Google Scholar
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_23
Chapter Google Scholar
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
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_12
Chapter MATH Google Scholar
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
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_12
Chapter MATH Google Scholar
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_2
Chapter Google Scholar
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
Müller-Olm, M., Seidl, H.: Analysis of modular arithmetic. ACM Trans. Program. Lang. Syst. 29(5), 29 (2007)
Article Google Scholar
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_17
Chapter Google Scholar
Simon, A.: Value-Range Analysis of C Programs: Towards Proving the Absence of Buffer Overflow Vulnerabilities. Springer, London (2008)
Google Scholar
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_25
Chapter Google Scholar
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_24
Chapter Google Scholar
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
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

Download references

Author information

Authors and Affiliations

Sorbonne Université, CNRS, Laboratoire d’Informatique de Paris 6, LIP6, 75005, Paris, France
Matthieu Journault, Antoine Miné & Abdelraouf Ouadjaout

Authors

Matthieu Journault
View author publications
You can also search for this author in PubMed Google Scholar
Antoine Miné
View author publications
You can also search for this author in PubMed Google Scholar
Abdelraouf Ouadjaout
View author publications
You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Matthieu Journault .

Editor information

Editors and Affiliations

Universität Freiburg, Freiburg, Germany
Andreas Podelski

Appendices

A Tool functions

1.1 A.1 Definition of the Galois Connection

In the following denotes .

Using functions to_cells and from_cells, and under the hypothesis that $\mathfrak V = \{s_0,\dots , s_{n-1}\}$, we can define the Galois connection between the Cell abstract domain and the String abstract domain:

$$\begin{aligned} \gamma _{S^{\sharp }_m,D^{\sharp }_m}(S^{\sharp })&= \mathbf {to\_cell}(s_0,\dots , (\mathbf {to\_cell}(s_{n-1},S^{\sharp })) \dots )\\ \alpha _{S^{\sharp }_m,D^{\sharp }_m}(S^{\sharp })&= \mathbf {from\_cell}(s_0,\dots ,( \mathbf {from\_cell}(s_{n-1}, S^{\sharp }))\dots ) \end{aligned}$$

1.2 A.2 Definition of the Evaluation of a Dereferencing

$$\begin{aligned} {\mathbf {before}}&(e,s,S^{\sharp })=\\&\{([1;255], \langle C,R^{\sharp } \sqcap \{0 \le e, e< s_l, e< s_a \}, P\rangle \}\\ \mathbf {at}&(e,s,S^{\sharp })=\\&\{(0, \langle C,R^{\sharp } \sqcap \{0 \le e, e = s_l, e< s_a \}, P \rangle \}\\ \mathbf {after}&(e,s,S^{\sharp })=\\&\{([0;255], \langle C,R^{\sharp } \sqcap \{0 \le e, e > s_l, e< s_a \}, P \rangle \}\\ \mathbf {eerror}&(e,s,S^{\sharp })=\\&\mathbf {let\ } R^{\sharp }_1 = R^{\sharp } \sqcap \{e \ge s_a \} \sqcup R^{\sharp } \sqcap \{e < 0 \} \mathbf {\ in\ }\\&{\textit{ test for } \mathbf{out\_of\_bounds } (R_1^{\sharp }\sqsubseteq _{S^{\sharp }_m} \bot )?}\\&\emptyset \end{aligned}$$

1.3 A.3 Definition of the Abstract Postcondition of an Assignment

$$\begin{aligned} \mathbf {set0}&(s,e_1,e_2,\langle C, R^{\sharp }, P\rangle ) =\\&\mathbf {let\ }R^{\sharp }_1 = R^{\sharp } \sqcap \{e_1 \ge 0, e_1 \le s_l, e_1< s_a, e_2 = 0\} \mathbf {\ in}\\&\mathbf {let\ }R^{\sharp }_2 = \mathbb S^{\sharp } \llbracket s_l \leftarrow e_1 \rrbracket (R^{\sharp }_1) \mathbf {\ in}\\&\langle C, R^{\sharp }_2, P \rangle \\ \mathbf {setnon0}&(s,e_1,e_2,\langle C, R^{\sharp }, P\rangle ) =\\&\mathbf {let\ }R^{\sharp }_1 = R^{\sharp } \sqcap \{e_1 \ge 0, e_1 = s_l , e_1< s_a, e_2 \ne 0\} \mathbf {\ in}\\&\mathbf {let\ }R^{\sharp }_2 = \mathbb S^{\sharp } \llbracket s_l \leftarrow [e_1+1; s_a] \rrbracket (R^{\sharp }_1) \mathbf {\ in}\\&\langle C, R^{\sharp }_2, P \rangle \\ \mathbf {unchanged}&(s,e_1,e_2,\langle C, R^{\sharp }, P\rangle ) =\\&\mathbf {let\ }R^{\sharp }_1 = (R^{\sharp } \sqcap \{e_1 \ge 0, e_1< s_l , e_1< s_a, e_2 \ne 0\}) \\&\quad \quad \quad \sqcup (R^{\sharp } \sqcap \{e_1 \ge 0, e_1> s_l , e_1< s_a\}) \mathbf {\ in}\\&\langle C, R^{\sharp }_1, P \rangle \\ \mathbf {l\_unchanged}&(s,e_1,r,\langle C, R^{\sharp }, P\rangle ) =\\&\mathbf {let\ }R^{\sharp }_1 = (R^{\sharp } \sqcap \{e_1 \ge 0, e_1 > s_l , e_1 + r \le s_a\}) \mathbf {\ in}\\&\langle C, R^{\sharp }_1, P \rangle \\ \mathbf {forget}&(s,e_1,r,\langle C, R^{\sharp }, P \rangle ) =\\&\mathbf {let\ }R^{\sharp }_1 = R^{\sharp } \sqcap \{e_1 \ge 0, e_1 \le s_l, e_1 + r \le s_a\} \mathbf {\ in}\\&\mathbf {let\ }R^{\sharp }_2 = \mathbb S^{\sharp } \llbracket s_l\leftarrow [e_1; s_a] \rrbracket (R^{\sharp }_1) \mathbf {in}\\&\langle C, R^{\sharp }_2, P \rangle \\ \mathbf {serror}&(s,e_1,r,\langle C, R^{\sharp }, P \rangle ) =\\&\mathbf {let\ }R^{\sharp }_1 = R^{\sharp } \sqcap \{e_1 \ge s_a\} \mathbf {\ in}\\&\mathbf {let\ }R^{\sharp }_2 = R^{\sharp } \sqcap \{e_1 < 0\} \mathbf {\ in }\\&{ \textit{ test for } \mathbf{ out\_of\_bounds } ((R_2^{\sharp } \sqcup _{S_m^{\sharp }}R_1^{\sharp }) \sqsubseteq _{S^{\sharp }_m} \bot ) ?}\\&\bot \end{aligned}$$

1.4 A.4 String Declaration

B C Programs

Rights and permissions

Reprints and permissions

Copyright information

About this paper

Cite this paper

Journault, M., Miné, A., Ouadjaout, A. (2018). Modular Static Analysis of String Manipulations in C Programs. In: Podelski, A. (eds) Static Analysis. SAS 2018. Lecture Notes in Computer Science(), vol 11002. Springer, Cham. https://doi.org/10.1007/978-3-319-99725-4_16

Download citation

DOI: https://doi.org/10.1007/978-3-319-99725-4_16
Published: 29 August 2018
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-99724-7
Online ISBN: 978-3-319-99725-4
eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Modular Static Analysis of String Manipulations in C Programs

Abstract

Access this chapter

Subscribe and save

Buy Now