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代碼逐漸改進，並且成本要低得多。

來自許多大學和公司的研究人員為馬里蘭州大學，羅切斯特大學，華盛頓大學，三星，羅格斯大學和賓夕法尼亞大學的檢查人員做出了貢獻。

行為守則

該項目採用了行為準則。