一种可编程控制器的形式化模型
A Formal Model of Checked C
摘要：
我们提出了一个正式的模型，CMAC，方言的C，旨在加强空间内存安全。我们的模型特别注意动态大小的语义，可能空终止数组。我们在Coq中形式化了这个模型，并证明了任何空间内存安全错误都可以归咎于标记为未检查的程序部分;这是一个支持增量移植和向后兼容性的CNOC功能。虽然我们的模型的操作语义使用注释（“胖”）指针来执行空间安全，我们表明，这样的注释可以安全地删除：使用PLT Redex我们正式的可执行版本的模型和编译过程，从它到一个无类型的C类语言，并使用随机测试来验证生成的代码忠实地模拟原来的。最后，我们为Redex模型中的良好类型和几乎良好类型的术语开发了一个自定义的随机生成器，并使用它来搜索我们的模型和Clang Java实现之间的不一致。我们发现这些步骤是共同开发一种语言（CISC仍在开发中）和它的核心模型的有用方法。
英文摘要：
We present a formal model of Checked C, a dialect of C that aims to enforce spatial memory safety. Our model pays particular attention to the semantics of dynamically sized, potentially null-terminated arrays. We formalize this model in Coq, and prove that any spatial memory safety errors can be blamed on portions of the program labeled unchecked; this is a Checked C feature that supports incremental porting and backward compatibility. While our model's operational semantics uses annotated ("fat") pointers to enforce spatial safety, we show that such annotations can be safely erased: Using PLT Redex we formalize an executable version of our model and a compilation procedure from it to an untyped C-like language, and use randomized testing to validate that generated code faithfully simulates the original. Finally, we develop a custom random generator for well-typed and almost-well-typed terms in our Redex model, and use it to search for inconsistencies between our model and the Clang Checked C implementation. We find these steps to be a useful way to co-develop a language (Checked C is still in development) and a core model of it.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
