More Web Proxy on the site http://driver.im/

research-article

A formal C memory model supporting integer-pointer casts

Authors:

William Mansky,

Dmitri Garbuzov,

Steve Zdancewic,

Viktor VafeiadisAuthors Info & Claims

ACM SIGPLAN Notices, Volume 50, Issue 6

Pages 326 - 335

https://doi.org/10.1145/2813885.2738005

Published: 03 June 2015 Publication History

Abstract

The ISO C standard does not specify the semantics of many valid programs that use non-portable idioms such as integer-pointer casts. Recent efforts at formal definitions and verified implementation of the C language inherit this feature. By adopting high-level abstract memory models, they validate common optimizations. On the other hand, this prevents reasoning about much low-level code relying on the behavior of common implementations, where formal verification has many applications. We present the first formal memory model that allows many common optimizations and fully supports operations on the representation of pointers. All arithmetic operations are well-defined for pointers that have been cast to integers. Crucially, our model is also simple to understand and program with. All our results are fully formalized in Coq.

References

[1]

F. Besson, S. Blazy, and P. Wilke. A precise and abstract memory model for C using symbolic values. In APLAS, 2014.

[2]

C. Ellison and G. Rosu. An executable formal semantics of C with applications. In POPL, 2012.

Digital Library

[3]

D. Greenaway, J. Lim, J. Andronick, and G. Klein. Don’t sweat the small stuff: Formal verification of C code without the pain. In PLDI, 2014.

Digital Library

[4]

C.-K. Hur, D. Dreyer, G. Neis, and V. Vafeiadis. The marriage of bisimulations and Kripke logical relations. In POPL, 2012.

Digital Library

[5]

ISO. ISO/IEC 9899:2011 Information technology – Programming languages – C. 2011.

[6]

R. Krebbers. Aliasing restrictions of C11 formalized in Coq. In CPP, 2013.

Digital Library

[7]

R. Krebbers, X. Leroy, and F. Wiedijk. Formal C semantics: CompCert and the C standard. In ITP, 2014.

[8]

R. Krebbers and F. Wiedijk. A formalization of the C99 standard in HOL, Isabelle and Coq. In CICM, 2011.

Digital Library

[9]

X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363–446, 2009.

Digital Library

[10]

X. Leroy, A. W. Appel, S. Blazy, and G. Stewart. The CompCert memory model, version 2. Research report RR-7987, INRIA, June 2012.

[11]

M. Norrish. C formalised in HOL. Computer Laboratory Technical Report 453, University of Cambridge, Nov. 1998.

[12]

J. ˇSevˇc´ık, V. Vafeiadis, F. Zappa Nardelli, S. Jagannathan, and P. Sewell. CompCertTSO: A verified compiler for relaxed-memory concurrency. Journal of the ACM, 60(3):22, 2013.

Digital Library

[13]

X. Wang, N. Zeldovich, M. F. Kaashoek, and A. Solar-Lezama. Towards optimization-safe systems: Analyzing the impact of undefined behavior. In SOSP, 2013.

Digital Library

[14]

X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and understanding bugs in C compilers. In PLDI, 2011.

Digital Library

[15]

J. Zhao, S. Nagarakatte, M. M. Martin, and S. Zdancewic. Formalizing the LLVM intermediate representation for verified program transformations. In POPL, 2012.

Digital Library

[16]

J. Zhao, S. Nagarakatte, M. M. Martin, and S. Zdancewic. Formal verification of SSA-based optimizations for LLVM. In PLDI, 2013.

Digital Library

Cited By

Zou CHe DSui YXue J(2024)TIPS: Tracking Integer-Pointer Value Flows for C++ Member Function PointersProceedings of the ACM on Software Engineering10.1145/36607791:FSE(1609-1631)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3660779
Li LLiu YPostol DLampropoulos LVan Horn DHicks M(2023)A formal model of Checked C1Journal of Computer Security10.3233/JCS-23004031:5(581-614)Online publication date: 13-Oct-2023
https://doi.org/10.3233/JCS-230040
Rocha RSprokholt DFink MGouicem RSpink TChakraborty SBhatotia PJhala RDillig I(2022)Lasagne: a static binary translator for weak memory model architecturesProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523719(888-902)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523719
Show More Cited By

Index Terms

A formal C memory model supporting integer-pointer casts

Recommendations

A formal C memory model supporting integer-pointer casts
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

The ISO C standard does not specify the semantics of many valid programs that use non-portable idioms such as integer-pointer casts. Recent efforts at formal definitions and verified implementation of the C language inherit this feature. By adopting ...
A Formal Framework for ASTRAL Intralevel Proof Obligations

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...
Towards a Formal Basis for the Formal Development Method and the Ina Jo Specification Language
Special issue on computer security and privacy

In carrying out SDC's Formal Development Method, one writes a specification of a system under design in the Ina Jo™ specification language and proves that the specification meets the requirements of the system. This paper develops an abstract machine ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 50, Issue 6

PLDI '15

June 2015

630 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2813885

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2015
630 pages
ISBN:9781450334686
DOI:10.1145/2737924
General Chair:
David Grove
IBM Research, USA
,
Program Chair:
Steve Blackburn
Australian National University, Australia

Copyright © 2015 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: 03 June 2015

Published in SIGPLAN Volume 50, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

MSIP / NRF
EC FP7
NSF

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

44
Total Citations
View Citations
447
Total Downloads

Downloads (Last 12 months)24
Downloads (Last 6 weeks)3

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zou CHe DSui YXue J(2024)TIPS: Tracking Integer-Pointer Value Flows for C++ Member Function PointersProceedings of the ACM on Software Engineering10.1145/36607791:FSE(1609-1631)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3660779
Li LLiu YPostol DLampropoulos LVan Horn DHicks M(2023)A formal model of Checked C1Journal of Computer Security10.3233/JCS-23004031:5(581-614)Online publication date: 13-Oct-2023
https://doi.org/10.3233/JCS-230040
Rocha RSprokholt DFink MGouicem RSpink TChakraborty SBhatotia PJhala RDillig I(2022)Lasagne: a static binary translator for weak memory model architecturesProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523719(888-902)Online publication date: 9-Jun-2022
https://dl.acm.org/doi/10.1145/3519939.3523719
Sadykov RMandrykin M(2022)Complete Decision Procedure for the Theory of Bounded Pointer ArithmeticProgramming and Computing Software10.1134/S036176882208002348:8(770-780)Online publication date: 1-Dec-2022
https://dl.acm.org/doi/10.1134/S0361768822080023
Li LLiu YPostol DLampropoulos LVan Horn DHicks M(2022)A Formal Model of Checked C2022 IEEE 35th Computer Security Foundations Symposium (CSF)10.1109/CSF54842.2022.9919657(49-63)Online publication date: Aug-2022
https://doi.org/10.1109/CSF54842.2022.9919657
Yodaiken V(2021)How ISO C became unusable for operating systems developmentProceedings of the 11th Workshop on Programming Languages and Operating Systems10.1145/3477113.3487274(84-90)Online publication date: 25-Oct-2021
https://dl.acm.org/doi/10.1145/3477113.3487274
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
Jung RDang HKang JDreyer D(2019)Stacked borrows: an aliasing model for RustProceedings of the ACM on Programming Languages10.1145/33711094:POPL(1-32)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371109
Frumin DGondelman LKrebbers R(2019)Semi-automated Reasoning About Non-determinism in C ExpressionsProgramming Languages and Systems10.1007/978-3-030-17184-1_3(60-87)Online publication date: 6-Apr-2019
https://doi.org/10.1007/978-3-030-17184-1_3
Kim YCho MLee JKim JYoon TSong YHur C(2025)Archmage and CompCertCast: End-to-End Verification Supporting Integer-Pointer CastingProceedings of the ACM on Programming Languages10.1145/37048819:POPL(1326-1354)Online publication date: 9-Jan-2025
https://dl.acm.org/doi/10.1145/3704881
Show More Cited By

View Options

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