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

Content Provider	ACM Digital Library
Author	Carbonneaux, Quentin Hoffmann, Jan Shao, Zhong Ramananandro, Tahina
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.
Starting Page	270
Ending Page	281
Page Count	12
File Format	PDF
ISSN	03621340 15581160
DOI	10.1145/2666356.2594301
Journal	ACM SIGPLAN Notices (SIGP)
Volume Number	49
Issue Number	6
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1983-05-01
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Program logics Quantitative verification Stack-space bounds Compiler construction Formal verification
Content Type	Text
Resource Type	Article
Subject	Computer Graphics and Computer-Aided Design Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

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

Compiler verification meets cross-language linking via data abstraction

Experiences in building C++ front end

End-to-end verification of information-flow security for C and assembly programs

Probabilistic relational verification for cryptographic implementations

Termination proofs for systems code

A formal C memory model supporting integer-pointer casts

Formal verification of object layout for c++ multiple inheritance

A design and verification methodology for secure isolated regions

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

Similar Documents

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

Compiler verification meets cross-language linking via data abstraction

Experiences in building C++ front end

End-to-end verification of information-flow security for C and assembly programs

Probabilistic relational verification for cryptographic implementations

Termination proofs for systems code

A formal C memory model supporting integer-pointer casts

Formal verification of object layout for c++ multiple inheritance

A design and verification methodology for secure isolated regions

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