checkedc
Version 1.0 of the Checked C specification
Überprüft C erweitert C mit Grenzenprüfung und verbesserter Sicherheit. Es hilft den Programmierern, vorhandenen C -Code für sicherer zu sein. Dieses Repo enthält die geprüfte C -Spezifikation, den Beispielcode und den Testcode.
Fette Hinweise auf zeitliche Gedächtnissicherheit von C von Jie Zhou, John Criswell und Michael Hicks. Dies erschien in OOPSLA 2023. Es beschreibt eine Erweiterung des Checked C, die neue Zeiger hinzugefügt hat, die die Sicherheit der zeitlichen Speicher bieten.
C zu überprüft C mit 3C, von Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley und Michael Hicks. Dieses Papier beschreibt das semi-automatische 3C-Tool zum Konvertieren von C in die Überprüfung von C. Es wurde bei OOPSLA 2022 mit einem Sigplan Distinguished Paper Award ausgezeichnet.
Ein formales Modell von Checked C von Liyi Li, Deena Postol, Leonida Lampropoulos, David Van Horn und Michael Hicks. Dies wurde auf dem 35. Computer -Security -Foundations -Symposlium 2022 veröffentlicht. Es beschreibt ein formales Modell des überprüften C. Das Modell wurde unter Verwendung des CoQ -Theorem -Provers formalisiert.
Inkrementell mit überprüftes C. überprüft C. Dies wurde auf den Principles of Security and Trust Conference 2019 vorgestellt:. Dieses Papier beschreibt eine frühe Version von 3C, die vorhandenen C -Code in die Verwendung von PTR -Typen umwandelt. Es erweist sich auch als Schuld über überprüfte Regionen, die zeigt, dass überprüfte Regionen für jede Speicherbeschäftigung tadellos sind. Dieser Beweis wird für eine Kernuntergruppe der Spracherweiterung formalisiert.
Checked C: C: C Safe Cy Extension von David Tarditi, Samuel Elliott, Andrew Ruef und Michael Hicks. Dies erschien auf der Cybersecurity Development Conference 2018 2018. Es beschreibt die wichtigsten Ideen der geprüften C -Grenzen auf 8 Seiten. Seitdem haben wir Funktionen zum Überprüfen von C hinzugefügt. Das Wiki und die Spezifikation liefern aktuelle Beschreibungen von Checked C.
Auf dem LLVM Dev Meeting 2019 wurde ein Poster vorgestellt: "Überläufe sind weg: Überprüfte C auf Speichersicherheit". Das Poster bietet eine Einführung in das Checked C, beschreibt die Compiler -Implementierung und präsentiert eine experimentelle Bewertung von Checked C.
Es gab einen Vortrag (Folien) beim Treffen von Virtual Dev 2020 LLVM: "Überprüft: C: Hinzufügen von Speichersicherheitsunterstützung zu LLVM". Der Vortrag beschreibt das Design von Grenzenanmerkungen für überprüfte Zeiger und Array -Zeiger sowie den Rahmen für die statische Überprüfung der Klanggrenzen. Der Vortrag beschreibt auch kurz neue Algorithmen, um die Grenzen für null-terminierte Arrays automatisch zu erweitern und den Ausdrücke für die Äquivalenzvergleich zu vergleich.
Wir freuen uns, die Hilfe zu haben. Sie können einen Beitrag leisten, indem Sie überprüft werden, C -Meldungen und Feedback geben. Es gibt auch andere Möglichkeiten, um einen Beitrag zu leisten.
Die Software in diesem Repository wird von der MIT -Lizenz abgedeckt. Siehe die Datei lizenz.txt für die Lizenz. Die geprüfte C -Spezifikation wird von Microsoft im Rahmen der endgültigen Spezifikationsvereinbarung von OpenWeb Foundation, Version 1.0, zur Verfügung gestellt. Beiträge von Code zu den geprüften LLVM/Clang -Repos unterliegen den LLVM/Clang -Lizenzbegriffen.
Checked C ist ein unabhängiges Open-Source-Projekt. Es begann 2015 als Forschungsprojekt bei Microsoft. Ähnlich wie überprüft C. Wir suchten nach einer Möglichkeit, die Sicherheit vorhandener Systemsoftware zu verbessern und Klassen von Fehler zu beseitigen.
Ein Ansatz besteht darin, die Software in einer neueren Sprache wie Rost umzuschreiben. Das Umschreiben von Code ist jedoch aus einer Reihe von Gründen eine Herausforderung: Es ist teuer, es gibt subtile Unterschiede in selbst grundlegenden Sprachmerkmalen wie Arithmetik über Sprachen und es kann lange dauern, bis Sie über ein Arbeitssystem verfügen. Kombiniert macht dies ein Umschreiben zu einem Hochrisiko-Softwareentwicklungsprojekt. Es ist unwahrscheinlich, dass diese Art von Umschreibungen nur zur Verbesserung der Sicherheit geschaffen werden. Wir haben uns entschlossen, einen inkrementellen Ansatz zu verfolgen, mit dem vorhandener C -Code allmählich und zu viel geringeren Kosten verbessert werden kann.
Forscher aus vielen Universitäten und Unternehmen haben zu Überprüfungen von C. Forschern an der Universität von Maryland, der Universität von Rochester, der University of Washington, Samsung, der Rutgers University und der University of Pennsylvania beigetragen, die zu einem geprüften C. Apple beigetragen haben, die sich auf eine ähnliche C -Erweiterung in ähnlicher Weise auf dynamischere Überprüfung stützen.
Dieses Projekt hat einen Verhaltenskodex angenommen.
