research-article

End-to-end verification of stack-space bounds for C programs

Authors:

Quentin Carbonneaux,

Tahina Ramananandro,

Zhong ShaoAuthors Info & Claims

ACM SIGPLAN Notices, Volume 49, Issue 6

Pages 270 - 281

https://doi.org/10.1145/2666356.2594301

Published: 09 June 2014 Publication History

Abstract

Verified compilers guarantee the preservation of semantic properties and thus enable formal verification of programs at the source level. However, important quantitative properties such as memory and time usage still have to be verified at the machine level where interactive proofs tend to be more tedious and automation is more challenging.

This article describes a framework that enables the formal verification of stack-space bounds of compiled machine code at the C level. It consists of a verified CompCert-based compiler that preserves quantitative properties, a verified quantitative program logic for interactive stack-bound development, and a verified stack analyzer that automatically derives stack bounds during compilation.

The framework is based on event traces that record function calls and returns. The source language is CompCert Clight and the target language is x86 assembly. The compiler is implemented in the Coq Proof Assistant and it is proved that crucial properties of event traces are preserved during compilation. A novel quantitative Hoare logic is developed to verify stack-space bounds at the CompCert Clight level. The quantitative logic is implemented in Coq and proved sound with respect to event traces generated by the small-step semantics of CompCert Clight. Stack-space bounds can be proved at the source level without taking into account low-level details that depend on the implementation of the compiler. The compiler fills in these low-level details during compilation and generates a concrete stack-space bound that applies to the produced machine code. The verified stack analyzer is guaranteed to automatically derive bounds for code with non-recursive functions. It generates a derivation in the quantitative logic to ensure soundness as well as interoperability with interactively developed stack bounds.

In an experimental evaluation, the developed framework is used to obtain verified stack-space bounds for micro benchmarks as well as real system code. The examples include the verified operating-system kernel CertiKOS, parts of the MiBench embedded benchmark suite, and programs from the CompCert benchmarks. The derived bounds are close to the measured stack-space usage of executions of the compiled programs on a Linux x86 system.

References

[1]

E. Albert, P. Arenas, S. Genaim, M. Gómez-Zamalloa, and G. Puebla. Cost Analysis of Concurrent OO Programs. In Prog. Langs. and Systems - 9th Asian Symposium (APLAS'11), pages 238--254, 2011.

Digital Library

[2]

E. Albert, R. Bubel, S. Genaim, R. Hähnle, and G. Román-Díez. Verified Resource Guarantees for Heap Manipulating Programs. In Fundamental Approaches to Soft. Eng. - 15th Int. Conf. (FASE'12), pages 130--145, 2012.

Digital Library

[3]

A. W. Appel et al. Program Logics for Certified Compilers. Cambridge University Press, 2013.

[4]

D. Aspinall, L. Beringer, M. Hofmann, H.-W. Loidl, and A. Momigliano. A Program Logic for Resources. Theor. Comput. Sci., 389(3):411--445, 2007.

Digital Library

[5]

R. Atkey. Amortised Resource Analysis with Separation Logic. In 19th Euro. Symp. on Prog. (ESOP'10), pages 85--103, 2010.

Digital Library

[6]

R. Bedin França, S. Blazy, D. Favre-Felix, X. Leroy, M. Pantel, and J. Souyris. Formally Verified Optimizing Compilation in ACG-based Flight Control Software. In Embedded Real Time Software and Systems (ERTS 2012), 2012.

[7]

S. Blazy, A. Maroneze, and D. Pichardie. Formal Verification of Loop Bound Estimation for WCET Analysis. In Verified Software: Theories, Tools, Experiments - 5th Int. Conf. (VSTTE'13), 2013. To appear.

[8]

D. Brylow, N. Damgaard, and J. Palsberg. Static Checking of Interrupt-Driven Software. In 23rd Int. Conf. on Soft. Engineering (ICSE'01), pages 47--56, 2001.

Digital Library

[9]

Q. Carbonneaux, J. Hoffmann, T. Ramananandro, and Z. Shao. End-to-End Verification of Stack-Space Bounds for C Programs. Technical Report YALEU/DCS/TR-1487, Yale University, March 2014.

Digital Library

[10]

W.-N. Chin, H. H. Nguyen, C. Popeea, and S. Qin. Analysing Memory Resource Bounds for Low-Level Programs. In 7th Int Symp. on Memory Management (ISMM'08), pages 151--160, 2008.

Digital Library

[11]

A. Chlipala. A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language. In 28th Conf. on Prog. Lang. Design and Impl. (PLDI'07), pages 54--65, 2007.

Digital Library

[12]

K. Crary and S. Weirich. Resource Bound Certification. In 27th ACM Symp. on Principles of Prog. Langs. (POPL'00), pages 184--198, 2000.

Digital Library

[13]

Express Logic, Inc. Helping you avoid stack overflow crashes! White Paper, 2014. URL http://rtos.com/images/uploads/Stack_Analysis_White_paper.1_.pdf.

[14]

C. Ferdinand, R. Heckmann, and B. Franzen. Static Memory and Timing Analysis of Embedded Systems Code. In 3rd Europ. Symp. on Verification and Validation of Software Systems (VVSS'07), 2007.

[15]

L. Gu, A. Vaynberg, B. Ford, Z. Shao, and D. Costanzo. CertiKOS: A Certified Kernel for Secure Cloud Computing. In Asia Pacific Workshop on Systems (APSys'11), 2011.

Digital Library

[16]

S. Gulwani, K. K. Mehra, and T. M. Chilimbi. SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In 36th ACM Symp. on Principles of Prog. Langs. (POPL'09), pages 127--139, 2009.

Digital Library

[17]

M. R. Guthaus, J. S. Ringenberg, D. Ernst, T. M. Austin, T. Mudge, and R. B. Brown. MiBench: A Free, Commercially Representative Embedded Benchmark Suite. In IEEE International Workshop on Workload Characterization (WWC'01), pages 3--14, 2001.

Digital Library

[18]

K. Hammond and G. Michaelson. Hume: A Domain-Specific Language for Real-Time Embedded Systems. In Generative Progr. and Component Eng., 2nd Int. Conf. (GPCE'03), pages 37--56, 2003.

Digital Library

[19]

J. Hoffmann, K. Aehlig, and M. Hofmann. Multivariate Amortized Resource Analysis. ACM Trans. Program. Lang. Syst., 2012.

Digital Library

[20]

J. Hoffmann, M. Marmar, and Z. Shao. Quantitative Reasoning for Proving Lock-Freedom. In 28th ACM/IEEE Symposium on Logic in Computer Science (LICS'13), 2013.

Digital Library

[21]

M. Hofmann and S. Jost. Static Prediction of Heap Space Usage for First-Order Functional Programs. In 30th ACM Symp. on Principles of Prog. Langs. (POPL'03), pages 185--197, 2003.

Digital Library

[22]

J. B. Jensen, N. Benton, and A. Kennedy. High-Level Separation Logic for Low-Level Code. In 40th ACM Symp. on Principles of Prog. Langs. (POPL'13), pages 301--314, 2013.

Digital Library

[23]

S. Jost, H.-W. Loidl, K. Hammond, N. Scaife, and M. Hofmann. Carbon Credits for Resource-Bounded Computations using Amortised Analysis. In 16th Symp. on Form. Meth. (FM'09), pages 354--369, 2009.

Digital Library

[24]

G. Klein and T. Nipkow. A Machine-Checked Model for a Java-Like Language, Virtual Machine, and Compiler. ACM Trans. Program. Lang. Syst., 28(4):619--695, 2006.

Digital Library

[25]

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: Formal Verification of an Operating-System Kernel. Commun. ACM, 53(6):107--115, 2010.

Digital Library

[26]

X. Leroy. Formal Certification of a Compiler Back-End, or: Programming a Compiler with a Proof Assistant. In 33rd Symposium on Principles of Prog. Langs. (POPL'06), pages 42--54, 2006.

Digital Library

[27]

X. Leroy. Formal Verification of a Realistic Compiler. Communications of the ACM, 52(7):107--115, 2009.

Digital Library

[28]

Y. Moy, E. Ledinot, H. Delseny, V. Wiels, and B. Monate. Testing or Formal Verification: DO-178C Alternatives and Industrial Experience. IEEE Software, 30(3):50--57, 2013. ISSN 0740--7459.

Digital Library

[29]

Z. Ni and Z. Shao. Certified Assembly Programming with Embedded Code Pointers. In 33th ACM Symp. on Principles of Prog. Langs. (POPL'06), pages 320--333, 2006.

Digital Library

[30]

T. Nipkow. Hoare Logics in Isabelle/HOL. In Proof and System-Reliability, volume 62 of NATO Science Series, pages 341--367. Springer, 2002.

[31]

J. Regehr, A. Reid, and K. Webb. Eliminating Stack Overflow by Abstract Interpretation. ACM Trans. Embed. Comput. Syst., 4(4):751--778, 2005.

Digital Library

[32]

J. Sevcík, V. Vafeiadis, F. Z. Nardelli, S. Jagannathan, and P. Sewell. CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency. J. ACM, 60(3), 2013.

Digital Library

[33]

Z. Shao. Certified software. Commun. ACM, 53(12):56--66, 2010.

Digital Library

[34]

R. Wilhelm et al. The Worst-Case Execution-Time Problem --- Overview of Methods and Survey of Tools. ACM Trans. Embedded Comput. Syst., 7(3), 2008.

Digital Library

[35]

X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and Understanding Bugs in C Compilers. In 32nd Conf. on Prog. Lang. Design and Impl. (PLDI'11), pages 283--294, 2011.

Digital Library

[36]

F. Zuleger, M. Sinn, S. Gulwani, and H. Veith. Bound Analysis of Imperative Programs with the Size-change Abstraction. In 18th Int. Static Analysis Symposium (SAS'11), 2011.

Digital Library

Cited By

Batz KKaminski BKatoen JMatheja CVerscht L(2023)A Calculus for Amortized Expected RuntimesProceedings of the ACM on Programming Languages10.1145/35712607:POPL(1957-1986)Online publication date: 11-Jan-2023
https://doi.org/10.1145/3571260
Moine ACharguéraud APottier F(2023)A High-Level Separation Logic for Heap Space under Garbage CollectionProceedings of the ACM on Programming Languages10.1145/35712187:POPL(718-747)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571218
Madiot JPottier F(2022)A separation logic for heap space under garbage collectionProceedings of the ACM on Programming Languages10.1145/34986726:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498672
Show More Cited By

Index Terms

End-to-end verification of stack-space bounds for C programs

Recommendations

End-to-end verification of stack-space bounds for C programs
PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation

Verified compilers guarantee the preservation of semantic properties and thus enable formal verification of programs at the source level. However, important quantitative properties such as memory and time usage still have to be verified at the machine ...
A Deductive Verification Infrastructure for Probabilistic Programs

This paper presents a quantitative program verification infrastructure for discrete probabilistic programs. Our infrastructure can be viewed as the probabilistic analogue of Boogie: its central components are an intermediate verification language (...
Hoare-Style Logic for Unstructured Programs
Software Engineering and Formal Methods
Abstract
Enabling Hoare-style reasoning for low-level code is attractive since it opens the way to regain structure and modularity in a domain where structure is essentially absent. The field, however, has not yet arrived at a fully satisfactory solution, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 49, Issue 6

PLDI '14

June 2014

598 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2666356

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

PLDI '14: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2014
619 pages
ISBN:9781450327848
DOI:10.1145/2594291
General Chair:
Michael O'Boyle
University of Edinburgh
,
Program Chair:
Keshav Pingali
University of Texas, Austin

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 June 2014

Published in SIGPLAN Volume 49, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

61
Total Citations
View Citations
368
Total Downloads

Downloads (Last 12 months)18
Downloads (Last 6 weeks)5

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Batz KKaminski BKatoen JMatheja CVerscht L(2023)A Calculus for Amortized Expected RuntimesProceedings of the ACM on Programming Languages10.1145/35712607:POPL(1957-1986)Online publication date: 11-Jan-2023
https://doi.org/10.1145/3571260
Moine ACharguéraud APottier F(2023)A High-Level Separation Logic for Heap Space under Garbage CollectionProceedings of the ACM on Programming Languages10.1145/35712187:POPL(718-747)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571218
Madiot JPottier F(2022)A separation logic for heap space under garbage collectionProceedings of the ACM on Programming Languages10.1145/34986726:POPL(1-28)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498672
Zhang LLian KXiao HZhang ZLiu PZhang YYang MDuan H(2022)Exploit the Last Straw That Breaks Android Systems2022 IEEE Symposium on Security and Privacy (SP)10.1109/SP46214.2022.9833563(2230-2247)Online publication date: May-2022
https://doi.org/10.1109/SP46214.2022.9833563
Albert EGenaim SMerayo ARomán-Díez G(2022)When COSTA Met KeY: Verified Cost BoundsThe Logic of Software. A Tasting Menu of Formal Methods10.1007/978-3-031-08166-8_2(19-37)Online publication date: 4-Jul-2022
https://doi.org/10.1007/978-3-031-08166-8_2
Gómez-Londoño AMyreen M(2021)A flat reachability-based measure for CakeML’s cost semanticsProceedings of the 33rd Symposium on Implementation and Application of Functional Languages10.1145/3544885.3544887(1-9)Online publication date: 1-Sep-2021
https://dl.acm.org/doi/10.1145/3544885.3544887
Abate CBlanco RCiobâcă ŞDurier AGarg DHriţcu CPatrignani MTanter ÉThibault J(2021)An Extended Account of Trace-relating Compiler Correctness and Secure CompilationACM Transactions on Programming Languages and Systems10.1145/346086043:4(1-48)Online publication date: 10-Nov-2021
https://dl.acm.org/doi/10.1145/3460860
Wen CWang HLi YQin SLiu YXu ZChen HXie XPu GLiu TRothermel GBae D(2020)MemLockProceedings of the ACM/IEEE 42nd International Conference on Software Engineering10.1145/3377811.3380396(765-777)Online publication date: 27-Jun-2020
https://dl.acm.org/doi/10.1145/3377811.3380396
Le XSanan DJun SLin S(2020)Automatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications2020 25th International Conference on Engineering of Complex Computer Systems (ICECCS)10.1109/ICECCS51672.2020.00013(43-52)Online publication date: Oct-2020
https://doi.org/10.1109/ICECCS51672.2020.00013
Paraskevopoulou ZAppel A(2019)Closure conversion is safe for spaceProceedings of the ACM on Programming Languages10.1145/33416873:ICFP(1-29)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341687
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents