Linking C and assembly for denotation-based verified compositional compilation

Abstract

Modern software often integrates assembly code into C programs for performance-critical tasks, such as big integer computation in the GMP library and cryptographic algorithms in the OpenSSL library. Though the formal semantics of C and assembly are well-studied, linking these languages for realistic compiler verification remains challenging due to their abstraction gap. In this article, we address the problem of linking C with assembly by introducing a denotation-based framework and we apply this framework to support verified compositional compilation (VCC) for C and x86 assembly in CompCert. Specifically, we propose a novel semantic transformation operator that systematically interprets the denotational semantics of assembly into that of C. This semantic transformation bridges the interaction differences between the two languages, enabling their semantic linking to be effectively implemented under a unified language interface. Furthermore, we demonstrate the soundness of such semantic linking by applying it to the context of VCC, where two key properties are proved: 1) the transformed C semantics is faithfully preserved by the original assembly semantics, and 2) this preservation is compositional with the compilation correctness of other open modules. As a result, our approach advances the use of denotational semantics for VCC when both C and assembly are involved. All results in this article are formally verified in the Coq proof assistant.

Graphical abstract

Keywords

semantic transformation / denotational semantics / verified compositional compilation

References

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

[2] Appel A W. Verified software toolchain - (invited talk). In: Proceedings of the 20th European Symposium on Programming. 2011, 1−17

[3] Beringer L. Verified software units. In: Proceedings of the 30th European Symposium on Programming. 2021, 118−147

[4] Cao Q, Beringer L, Gruetter S, Dodds J, Appel A W . VST-Floyd: a separation logic tool to verify correctness of C programs. Journal of Automated Reasoning, 2018, 61( 1): 367–422

[5] Granlund T. GNU MP 6.0 Multiple Precision Arithmetic Library. London: Samurai Media Limited, 2015

[6] Daemen J, Rijmen V. The Design of Rijndael: AES − The Advanced Encryption Standard. Berlin: Springer, 2002

[7] Rivest R L, Shamir A, Adleman L . A method for obtaining digital signatures and public-key cryptosystems. Communications of the ACM, 1983, 26( 1): 96–99

[8] Preneel B . Cryptographic hash functions. European Transactions on Telecommunications, 1994, 5( 4): 431–448

[9] Stewart G, Beringer L, Cuellar S, Appel A W. Compositional CompCert. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2015, 275−287

[10] Song Y, Cho M, Kim D, Kim Y, Kang J, Hur C K . CompCertM: CompCert with C-assembly linking and lightweight modular verification. Proceedings of the ACM on Programming Languages, 2020, 4( POPL): 23

[11] Koenig J, Shao Z. CompCertO: compiling certified open C components. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. 2021, 1095−1109

[12] Beringer L, Stewart G, Dockins R, Appel A W. Verified compilation for shared-memory C. In: Proceedings of the 23rd European Symposium on Programming. 2014, 107−127

[13] Cheng Z, Wu J, Wang D, Cao Q. Denotation-based compositional compiler verification. 2024, arXiv preprint arXiv: 2404.17297

[14] Zhang L, Wang Y, Wu J, Koenig J, Shao Z . Fully composable and adequate verified compilation with direct refinements between open modules. Proceedings of the ACM on Programming Languages, 2024, 8( POPL): 72

[15] Blazy S, Leroy X . Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 2009, 43( 3): 263–288

[16] Liang H, Feng X, Fu M. A rely-guarantee-based simulation for verifying concurrent program transformations. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2012, 455−468

[17] Bekić H. Definable operations in general algebras, and the theory of automata and flowcharts. In: Jones C B, ed. Programming Languages and Their Definition. Berlin: Springer, 1984, 30−55

[18] Blazy S, Dargaye Z, Leroy X. Formal verification of a C compiler front-end. In: Proceedings of the 14th International Symposium on Formal Methods. 2006, 460−475

[19] Leroy X . Formal verification of a realistic compiler. Communications of the ACM, 2009, 52( 7): 107–115

[20] Kang J, Kim Y, Hur C K, Dreyer D, Vafeiadis V. Lightweight verification of separate compilation. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2016, 178−190

[21] Ramananandro T, Shao Z, Weng S C, Koenig J, Fu Y. A compositional semantics for verified separate compilation and linking. In: Proceedings of 2015 Conference on Certified Programs and Proofs. 2015, 3−14

[22] Gu R, Koenig J, Ramananandro T, Shao Z, Wu X, Weng S C, Zhang H, Guo Y. Deep specifications and certified abstraction layers. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2015, 595−608

[23] Gu L, Vaynberg A, Ford B, Shao Z, Costanzo D. CertiKOS: a certified kernel for secure cloud computing. In: Proceedings of the 2nd Asia-Pacific Workshop on Systems. 2011, 3

[24] Gu R, Shao Z, Chen H, Wu X, Kim J, Sjöberg V, Costanzo D. CertiKOS: an extensible architecture for building certified concurrent OS kernels. In: Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation. 2016, 653−669

[25] Wang Y, Wilke P, Shao Z . An abstract stack based approach to verified compositional compilation to machine code. Proceedings of the ACM on Programming Languages, 2019, 3( POPL): 62

[26] Smyth M B . Power domains. Journal of Computer and System Sciences, 1978, 16( 1): 23–36

[27] Plotkin G D. A powerdomain for countable non-determinism (extended abstract). In: Proceedings of the 9th Colloquium Aarhus on Automata, Languages and Programming. 1982, 418−428

[28] Park D. On the semantics of fair parallelism. In: Proceedings of 1979 Copenhagen Winter School on Abstract Software Specifications. 1979, 504−526

[29] Winskel G . On powerdomains and modality. Theoretical Computer Science, 1985, 36: 127–137

[30] Back R J R . A continuous semantics for unbounded nondeterminism. Theoretical Computer Science, 1983, 23( 2): 187–210

[31] Hur C K, Dreyer D, Neis G, Vafeiadis V. The marriage of bisimulations and Kripke logical relations. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2012, 59−72

[32] Neis G, Hur C K, Kaiser J O, McLaughlin C, Dreyer D, Vafeiadis V. Pilsner: a compositionally verified compiler for a higher-order imperative language. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming. 2015, 166−178

[33] Hur C K, Neis G, Dreyer D, Vafeiadis V. The power of parameterization in coinductive proof. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2013, 193−206

[34] Hur C K, Dreyer D. A Kripke logical relation between ML and assembly. In: Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2011, 133−146

[35] New M S, Bowman W J, Ahmed A. Fully abstract compilation via universal embedding. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming. 2016, 103−116

[36] Patterson D, Perconti J, Dimoulas C, Ahmed A. FunTAL: reasonably mixing a functional language with assembly. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. 2017, 495−509

[37] Perconti J T, Ahmed A. Verifying an open compiler using multi-language semantics. In: Proceedings of the 23rd European Symposium on Programming. 2014, 128−148

[38] Scherer G, New M, Rioux N, Ahmed A. FabULous interoperability for ML and a linear language. In: Proceedings of the 21st International Conference on Foundations of Software Science and Computation Structures. 2018, 146−162

[39] Wang P, Cuellar S, Chlipala A . Compiler verification meets cross-language linking via data abstraction. ACM SIGPLAN Notices, 2014, 49( 10): 675–690

[40] Patterson D, Ahmed A . The next 700 compiler correctness theorems (functional pearl). Proceedings of the ACM on Programming Languages, 2019, 3( ICFP): 85

[41] Leroy X, Blazy S . Formal verification of a C-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 2008, 41( 1): 1–31

RIGHTS & PERMISSIONS

Higher Education Press