checkedc
Version 1.0 of the Checked C specification
Checked C拡張境界チェックとタイプの安全性の改善でCを拡張します。これにより、プログラマーは既存のCコードをより安全にするようになります。このレポは、チェックされたC仕様、サンプルコード、およびテストコードが含まれています。
Jie Zhou、John Criswell、Michael HicksによるCの時間的記憶安全性のための脂肪ポインター。これは、Oopsla 2023に登場しました。これは、時間の記憶の安全性を提供する新しいポインターを追加するChecked Cの拡張を説明しています。
c Aravind Machiry、John Kastner、Matt McCutchen、Aaron Eline、Kyle Headley、Michael HicksによるCを3Cで確認します。このホワイトペーパーでは、CをチェックしたCに変換するための半自動化された3Cツールについて説明します。これは、Oopsla 2022でSigplan Distinguished Paper Awardを受賞しました。
Checked Cの正式なモデル、Liyi Li、Deena Postol、Leonida Lampropoulos、David Van Horn、Michael Hicks。これは、2022年のIEEE第35コンピューターセキュリティファンデーションシンポジウムに掲載されました。 Checked Cの正式なモデルを説明しています。モデルは、Coq定理を使用して正式に化されました。
チェックされたCで徐々に安全を達成することは、2019年のセキュリティアンドトラスト会議の原則で提示されました。このペーパーでは、既存のCコードをPTRタイプを使用するように変換する3Cの初期バージョンについて説明します。また、チェックされた領域が記憶の腐敗について非難されていることを示すチェックされた地域に関する責任のある財産も証明しています。この証明は、言語拡張機能のコアサブセットに対して正式化されています。
Checked C：David Tarditi、Samuel Elliott、Andrew Ruef、Michael Hicksによる拡張によりCを安全にします。これは、IEEE 2018サイバーセキュリティ開発会議に掲載されました。 8ページでチェックされているチェックされたCの境界の重要なアイデアについて説明します。それ以来、Cをチェックした機能を追加しました。 Wikiと仕様は、チェックされたCの最新の説明を提供します。
LLVM Dev Meeting 2019で発表されたポスターがありました。ポスターは、チェックされたCの紹介を提供し、コンパイラの実装の概要を説明し、チェックされたCの実験的評価を提示します。
2020 LLVM Virtual Dev Meetingで講演（スライド）がありました。「Checked C：LLVMへのメモリ安全サポートの追加」。講演では、チェックされたポインターとアレイポインターのための境界注釈の設計と、境界の健全性の静的チェックのフレームワークについて説明しています。また、この講演では、ヌル終端配列の境界を自動的に拡大し、等価性の式の比較のために、新しいアルゴリズムを簡単に説明しています。
助けてくれてうれしいです。チェックされたCを試して、バグの報告、フィードバックを提供することで貢献できます。貢献する他の方法もあります。
このリポジトリのソフトウェアは、MITライセンスでカバーされています。ライセンスについては、ファイルライセンスを参照してください。チェックされたC仕様は、MicrosoftがOpenWeb Foundationの最終仕様契約であるバージョン1.0で利用可能にします。チェックされたLLVM/Clangレポスへのコードの貢献は、LLVM/Clangライセンス条件の対象となります。
Checked Cは独立したオープンソースプロジェクトです。 2015年にMicrosoftで研究プロジェクトとして始まりました。CheckedCと同様に、既存のシステムソフトウェアのセキュリティを改善し、バグのクラスを排除する方法を探していました。
1つのアプローチは、Rustなどの新しい言語でソフトウェアを書き換えることです。ただし、書き換えコードはいくつかの理由で挑戦的です。コストがかかり、言語間での算術などの基本的な言語機能にも微妙な違いがあり、作業システムがあるまでに長い時間がかかる場合があります。組み合わせて、これにより、リスクの高いソフトウェア開発プロジェクトを書き直します。これらの種類の書き換えは、セキュリティを改善するためだけに行われる可能性は低いです。既存のCコードを徐々に、はるかに低コストで改善できるようにする漸進的なアプローチを追求することにしました。
多くの大学や企業の研究者がチェックされたC.メリーランド大学、ロチェスター大学、ワシントン大学、サムスン大学、ラトガーズ大学、ペンシルバニア大学の研究者がチェックCを貢献しています。
このプロジェクトは、行動規範を採用しています。
