×

Verifying pointer safety for programs with unknown calls. (English) Zbl 1208.68149

Summary: We study the automated verification of pointer safety for heap-manipulating imperative programs with unknown procedure calls. Given a Hoare-style partial correctness specification \(S = \{\text{Pre}\}C\{\text{Post}\}\) in separation logic, where the program \(C\) contains calls to some unknown procedure \(U\), we infer a specification \(S_U\) for the unknown procedure \(U\) from the calling contexts. We show that the problem of verifying the program \(C\) against the specification \(S\) can be safely reduced to the problem of proving that the procedure \(U\) (once its code is available) meets the derived specification \(S_U\). The expected specification \(S_U\) for the unknown procedure \(U\) is automatically calculated using an abduction-based shape analysis. We have also implemented a prototype system to validate the viability of our approach. Preliminary results show that the specifications derived by our tool fully capture the behaviors of the unknown code in many cases.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)

Software:

FreeRTOS; HIP
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ammons, Glenn; Bodik, Rastislav; Larus, James R., Mining specifications, (Proc. of 29th Principles of Programming Languages, POPL (2002), ACM Press: ACM Press New York, NY, USA), 4-16 · Zbl 1323.68361
[3] Berdine, Josh; Calcagno, Cristiano; O’Hearn, Peter W., A decidable fragment of separation logic, (Proc. of Foundations of Software Technology and Theoretical Computer Science, FSTTCS. Proc. of Foundations of Software Technology and Theoretical Computer Science, FSTTCS, LNCS, vol. 3328 (2004), Springer: Springer Chennai, India), 97-109 · Zbl 1117.03337
[4] Berdine, Josh; Calcagno, Cristiano; O’Hearn, Peter W., Symbolic execution with separation logic, (Proc. of 3rd Asian Symposium on Programming Languages and Systems, APLAS. Proc. of 3rd Asian Symposium on Programming Languages and Systems, APLAS, LNCS, vol. 3780 (2005), Springer: Springer Tsukuba, Japan), 52-68 · Zbl 1159.68363
[5] Calcagno, Cristiano; Distefano, Dino; O’Hearn, Peter W.; Yang, Hongseok, Footprint analysis: A shape analysis that discovers preconditions, (Proc. of 14th International Symposium on Static Analysis, SAS. Proc. of 14th International Symposium on Static Analysis, SAS, LNCS, vol. 4634 (2007), Springer: Springer Denmark), 402-418
[6] Calcagno, Cristiano; Distefano, Dino; O’Hearn, Peter W.; Yang, Hongseok, Compositional shape analysis by means of bi-abduction, (Proc. of 36th Principles of Programming Languages, POPL (2009), ACM Press: ACM Press Savannah, Georgia, USA), 289-300 · Zbl 1315.68085
[7] Chin, Wei-Ngan; David, Cristina; Nguyen, Huu Hai; Qin, Shengchao, Automated verification of shape, size and bag properties, (Proc. of 12th International Conference on Engineering of Complex Computer Systems, ICECCS (2007), IEEE: IEEE Auckland, New Zealand), 307-320 · Zbl 1243.68148
[9] Distefano, Dino; O’Hearn, Peter W.; Yang, Hongseok, A local shape analysis based on separation logic, (Proc. of 12th Tools and Algorithms for the Construction and Analysis of Systems, TACAS. Proc. of 12th Tools and Algorithms for the Construction and Analysis of Systems, TACAS, LNCS, vol. 3920 (2006), Springer: Springer Vienna, Austria), 287-302 · Zbl 1180.68112
[10] Emami, Maryam; Ghiya, Rakesh; Hendren, Laurie J., Context-sensitive interprocedural points-to analysis in the presence of function pointers, (Proc. of Programming Language Design and Implementation, PLDI (1994), ACM Press: ACM Press New York, NY, USA), 242-256
[11] Giacobazzi, Roberto, Abductive analysis of modular logic programs, (Proc. of the International Symposium on Logic Programming, ISLP (1994), The MIT Press), 377-391 · Zbl 0904.68039
[12] Gopan, Denis; Reps, Thomas, Low-level library analysis and summarization, (Proc. of 19th Computer Aided Verification, CAV. Proc. of 19th Computer Aided Verification, CAV, LNCS, vol. 4590 (2007), Springer: Springer Berlin, Germany), 68-81 · Zbl 1211.68087
[13] Gulavani, Bhargav S.; Chakraborty, Supratik; Ramalingam, Ganesan; Nori, Aditya V., Bottom-up shape analysis, (Proc. of 16th International Symposium on Static Analysis, SAS. Proc. of 16th International Symposium on Static Analysis, SAS, LNCS, vol. 5673 (2009), Springer: Springer Los Angeles, CA, USA), 188-204 · Zbl 1248.68145
[14] Jones, Cliff; O’Hearn, Peter W.; Woodcock, Jim, Verified Software: A Grand Challenge, IEEE Computer, 39, 4, 93-95 (2006)
[15] Müller, Peter; Poetzsch-Heffter, Arnd; Leavens, Gary T., Modular specification of frame properties in JML, (Concurrency and Computation: Practice and Experience, 15 (2003)), 117-154 · Zbl 1005.68583
[16] Nguyen, Huu Hai; David, Cristina; Qin, Shengchao; Chin, Wei-Ngan, Automated verification of shape and size properties via separation logic, (Proc. of 8th Verification, Model Checking, and Abstract Interpretation, VMCAI. Proc. of 8th Verification, Model Checking, and Abstract Interpretation, VMCAI, LNCS, vol. 4349 (2007), Springer: Springer Nice, France), 251-266 · Zbl 1132.68477
[17] Nielson, Flemming; Nielson, Hanne Riis; Hankin, Chris, Principles of Program Analysis (2005), Springer · Zbl 1069.68534
[18] O’Hearn, Peter W.; Yang, Hongseok; Reynolds, John C., Separation and information hiding, (Proc. of 31st Principles of Programming Languages, POPL (2004), ACM Press: ACM Press Venice, Italy), 268-280 · Zbl 1325.68069
[19] Reynolds, John C., Separation logic: a logic for shared mutable data structures, (Proc. of 17th IEEE Symposium on Logic in Computer Science, LICS (2002), IEEE: IEEE Copenhagen, Denmark), 55-74
[20] Sessions, Roger, COM and DCOM: Microsoft’s Vision for Distributed Objects (1998), John Wiley & Sons, Inc.: John Wiley & Sons, Inc. New York, NY, USA
[21] Woodcock, Jim, Verified software grand challenge, (Proc. of 14th International Symposium on Formal Methods (FM). Proc. of 14th International Symposium on Formal Methods (FM), LNCS, vol. 4085 (2006), Springer: Springer Hamilton, Canada), 617
[22] Yang, Hongseok; Lee, Oukseh; Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter W., Scalable shape analysis for systems code, (Proc. of 20th Computer Aided Verification, CAV. Proc. of 20th Computer Aided Verification, CAV, LNCS, vol. 5123 (2008), Springer: Springer Princeton, NJ, USA), 385-398 · Zbl 1155.68359
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.