checkedc
Version 1.0 of the Checked C specification
Проверено C расширяет C с проверкой границ и улучшенной безопасностью типа. Это помогает программистам модернизировать существующий C -код, чтобы быть более безопасным. Этот репо содержит проверенную спецификацию C, пример кода и тестовый код.
Жирные указатели на безопасность временной памяти С Джи Чжоу, Джона Крисвелла и Майкла Хикса. Это появилось в OOPSLA 2023. Он описывает расширение для проверенного C, которое добавляет новые указатели, которые обеспечивают временную безопасность памяти.
C, чтобы проверить C по 3C, Аравинд Мачири, Джон Кастнер, Мэтт Маккатчен, Аарон Элин, Кайл Хедли и Майкл Хикс. В этой статье описывается полуавтоматический инструмент 3C для преобразования C в проверенный C. Он выиграл награду Sigplan выдающуюся бумагу на OOPSLA 2022.
Формальная модель проверенной C, Лии Ли, Дина Постол, Леонида Лампропулос, Дэвид Ван Хорн и Майкл Хикс. Это было опубликовано на 2022 году IEEE 35 -й Симпослий Фонда компьютерной безопасности. Он описывает формальную модель проверенной C. Модель была формализована с использованием Prower Coq Theoreem.
Достижение безопасности постепенно с проверено C. Это было представлено на Конференции по обеспечению безопасности и доверия 2019 года: В этой статье описывается ранняя версия 3C, которая преобразует существующий C -код в использование типов PTR. Это также доказывает собственность вины в области проверенных регионов, в которых показывается, что проверенные регионы являются безупречными для любой развращения памяти. Это доказательство формализовано для основного подмножества расширения языка.
Проверено C: Сделав C в безопасности по расширению Дэвида Тардити, Сэмюэля Эллиота, Эндрю Рюфа и Майкла Хикса. Это появилось на конференции по развитию кибербезопасности IEEE 2018. Он описывает ключевые идеи проверенных границ C, проверяющих 8 страниц. С тех пор мы добавили функции в проверку C. Вики и спецификация предоставляют актуальные описания проверенной C.
На собрании LLVM Dev 2019 был представлен плакат: «Переполнения пропадают: проверено C для безопасности памяти». На плакате представлено введение в проверенный C, описывает реализацию компилятора и представляет экспериментальную оценку проверенной C.
Был разговор (слайды) на собрании виртуального разработки LLVM 2020 года: «Проверено C: добавление поддержки безопасности памяти в LLVM». В разговоре описывается дизайн аннотаций границ для проверенных указателей и указателей массива, а также структуру для статической проверки обоснованности границ. В разговоре также кратко описывается новые алгоритмы для автоматического расширения границ для массивов с нулевым, и для сравнения выражений для эквивалентности.
Мы рады получить помощь. Вы можете внести свой вклад, попробовав проверенный C, сообщив об ошибках и предоставив нам отзывы. Есть и другие способы внести свой вклад.
Программное обеспечение в этом репозитории покрывается лицензией MIT. См. File License.txt для лицензии. Проверенная спецификация C предоставляется Microsoft в соответствии с соглашением о окончательной спецификации OpenWeb Foundation, версии 1.0. Взносы кода в проверенные репозиции LLVM/Clang подлежат условиям лицензирования LLVM/Clang.
Проверено C-независимый проект с открытым исходным кодом. Он начался как исследовательский проект в Microsoft в 2015 году. Подобно проверенному C. Мы искали способ повысить безопасность существующего системного программного обеспечения и устранить классы ошибок.
Одним из подходов является переписывание программного обеспечения на более новом языке, таком как Rust. Тем не менее, переписывание кода является сложной задачей по ряду причин: он дорого, существуют тонкие различия даже в основных языковых функциях, таких как арифметика между языками, и может занять много времени, прежде чем у вас будет рабочая система. В совокупности это делает переписывание проекта по разработке программного обеспечения с высоким риском. Эти виды переписываний вряд ли будут сделаны только для повышения безопасности. Мы решили использовать постепенный подход, который позволяет улучшать существующий код C постепенно и при гораздо меньшей стоимости.
Исследователи из многих университетов и компаний внесли свой вклад в проверку C. Исследователей из Университета Мэриленда, Университета Рочестера, Университета Вашингтона, Самсунг, Университет Рутгерса и Университета Пенсильвании, внесли свой вклад в проверку C. Apple предложили расширение C, аналогичное проверенному C, который полагается на более динамическую проверку.
Этот проект принял кодекс поведения.
