checkedc

检查c

检查的C通过界限检查和改进的类型安全性扩展。它可以帮助程序员改造现有的C代码以更安全。此存储库包含检查的C规范，示例代码和测试代码。

• 有关检查C和指针的快速概述，请参见我们的Wiki。
• 您可以在此处下载Windows，Mac和Ubuntu的Clang Clang编译器发行版。
• 该规范可在此处提供。
• 检查的C Clang编译器的存储库在这里。编译器是llvm/clang的叉子。从源代码构建编译器的说明在已检查的C Clang Wiki上。

建立状态

出版物和演示

• Jie Zhou，John Criswell和Michael Hicks的C的时间记忆安全性。它出现在OOPSLA 2023中。它描述了检查C的扩展名，该扩展名添加了提供时间记忆安全的新指针。

• C到3C检查C，由Aravind Machiry，John Kastner，Matt McCutchen，Aaron Eline，Kyle Headley和Michael Hicks检查。本文介绍了用于将C转换为检查的半自动化的3C工具。它在2022年OOPSLA赢得了Sigplan Decline Paper Award。

• Liyi Li，Deena Postol，Leonida Lampropoulos，David Van Horn和Michael Hicks的正式模型。这发表在2022 IEEE第35届计算机安全基础研讨会上。它描述了检查的正式模型C.使用COQ定理供体式形式化了该模型。

• 通过检查C逐渐实现安全性。本文描述了3C的早期版本，该版本将现有的C代码转换为使用PTR类型。这也证明了关于检查区域的责备财产，表明检查区域对于任何记忆损坏都是无罪的。该证明是为语言扩展的核心子集形式化的。

• 检查的C：David Tarditi，Samuel Elliott，Andrew Ruef和Michael Hicks的延期安全。这出现在IEEE 2018网络安全开发会议上。它描述了在8页中检查的检查C边界检查的关键思想。从那时起，我们为检查C添加了功能。 Wiki和规范提供了检查C的最新描述。

• 2019年LLVM开发会议上有一张海报：“溢出消失：检查C以确保记忆安全”。海报提供了检查C的介绍，概述了编译器实施，并提供了检查C的实验评估。

• 在2020 LLVM虚拟开发会议上有一个谈话（幻灯片）：“检查C：向LLVM添加内存安全支持”。演讲描述了检查指针和阵列指针的界限注释的设计，以及静态检查界限的框架。演讲还简要描述了新的算法，以自动扩大零终止阵列的界限，并比较表达式的等效性。

参与

我们很高兴得到帮助。您可以通过尝试检查C，报告错误并给我们反馈来做出贡献。还有其他方法可以做出贡献。

许可

本存储库中的软件由麻省理工学院许可证涵盖。请参阅文件许可证。txt以获取许可证。 Microsoft根据OpenWeb Foundation最终规范协议版本1.0提供了检查的C规范。代码对检查的LLVM/CLANG存储库的贡献受LLVM/CLANG许可条款的约束。

历史

检查C是一个独立的开源项目。它最初是在2015年在微软的研究项目。类似于检查C。我们正在寻找一种改善现有系统软件安全性并消除错误类别的方法。

一种方法是用诸如Rust之类的新语言重写软件。但是，由于多种原因，重写代码具有挑战性：这是昂贵的，即使是基本语言功能，例如跨语言的算法也存在细微的差异，并且可能需要很长时间才能拥有工作系统。结合在一起，这使得重写高风险的软件开发项目。这些重写不太可能仅仅是为了提高安全性。我们决定采用一种增量方法，该方法允许现有的C代码逐渐改进，并且成本要低得多。

来自许多大学和公司的研究人员为马里兰州大学，罗切斯特大学，华盛顿大学，三星，罗格斯大学和宾夕法尼亚大学的检查人员做出了贡献。

行为守则

该项目采用了行为准则。