checkedc

확인 c

확인 된 C는 경계 점검 및 유형 안전성 향상으로 C를 연장합니다. 프로그래머가 기존 C 코드를 개조하는 데 도움이됩니다. 이 repo에는 확인 된 C 사양, 샘플 코드 및 테스트 코드가 포함되어 있습니다.

• 샘플 코드에 대한 확인 된 C 및 포인터에 대한 간단한 개요는 Wiki를 참조하십시오.
• Windows, Mac 및 Ubuntu 용 Clang 컴파일러 릴리스를 여기에서 다운로드 할 수 있습니다.
• 사양은 여기에서 사용할 수 있습니다.
• 확인 된 C Clang 컴파일러의 리포지토리가 여기에 있습니다. 컴파일러는 LLVM/Clang의 포크입니다. 소스 코드에서 컴파일러를 구축하기위한 지침은 확인 된 C Clang Wiki에 있습니다.

상태 빌드 상태

출판물 및 프레젠테이션

• Jie Zhou, John Criswell 및 Michael Hicks의 C의 시간 기억 안전에 대한 뚱뚱한 포인터. 이것은 oopsla 2023에 나타났습니다. 시간적 메모리 안전을 제공하는 새로운 포인터를 추가하는 점검 된 C로의 확장을 설명합니다.

• C 3C, Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley 및 Michael Hicks의 C를 확인했습니다. 이 논문은 C를 점검 된 C로 변환하기위한 반자동 3C 도구에 대해 설명합니다. oopsla 2022에서 Sigplan Distinguished Paper Award를 수상했습니다.

• Liyi Li, Deena Postol, Leonida Lampropoulos, David Van Horn 및 Michael Hicks의 공식적인 C의 공식 모델. 이것은 2022 IEEE 35 번째 컴퓨터 보안 재단 심포지엄에 출판되었습니다. COQ 정리 공장을 사용하여 모델을 공식화 한 C의 공식적인 모델을 설명합니다.

• Checked C를 통해 점차 안전을 달성했습니다. 이것은 2019 년 보안 및 신탁 회의 원칙에서 발표되었습니다. 이 백서에서는 기존 C 코드를 PTR 유형을 사용하도록 변환하는 초기 버전 3C에 대해 설명합니다. 또한 점검 된 지역에 대한 비난의 재산을 증명합니다.이 지역은 확인 된 지역이 메모리 손상에 대해 흠이 없음을 보여줍니다. 이 증명은 언어 확장의 핵심 하위 집합에 대해 공식화됩니다.

• C : C : David Tarditi, Samuel Elliott, Andrew Ruef 및 Michael Hicks의 확장에 의해 C를 안전하게 만들었습니다. 이것은 IEEE 2018 사이버 보안 개발 회의에 실 렸습니다. 8 페이지에서 확인 된 C 경계의 주요 아이디어를 설명합니다. 그 이후로 CHECKED C에 기능을 추가했습니다. 위키 및 사양은 점검 된 C의 최신 설명을 제공합니다.

• LLVM Dev Meeting 2019에는 포스터가 발표되었습니다. 포스터는 확인 된 C에 대한 소개를 제공하고, 컴파일러 구현을 요약하고, 검사 된 C의 실험적 평가를 제공합니다.

• 2020 LLVM Virtual Dev 회의에서 대화 (슬라이드)가있었습니다. "확인 C : LLVM에 메모리 안전 지원 추가". 이 대화는 확인 된 포인터 및 배열 포인터에 대한 바운드 주석의 설계뿐만 아니라 경계의 건전성을 정적으로 점검하기위한 프레임 워크를 설명합니다. 이 대화는 또한 Null-Perminated Array의 경계를 자동으로 넓히고 동등성 표현을 비교하기위한 새로운 알고리즘을 간단히 설명합니다.

참여

우리는 도움을 받아 기쁩니다. Checked C를 시험 해보고 버그를보고하고 피드백을 제공함으로써 기여할 수 있습니다. 기여하는 다른 방법도 있습니다.

라이센스

이 저장소의 소프트웨어는 MIT 라이센스에 포함됩니다. 라이센스는 License.txt 파일을 참조하십시오. 점검 된 C 사양은 Microsoft에서 OpenWeb Foundation Final Specification Agrence, 버전 1.0에 따라 제공됩니다. 확인 된 LLVM/Clang Repos에 대한 코드 기여는 LLVM/Clang 라이센스 조건의 적용을받습니다.

역사

확인 된 C는 독립적 인 오픈 소스 프로젝트입니다. 2015 년 Microsoft에서 연구 프로젝트로 시작했습니다. Checked C와 비슷합니다. 기존 시스템 소프트웨어의 보안을 개선하고 버그 클래스를 제거 할 수있는 방법을 찾고있었습니다.

한 가지 방법은 Rust와 같은 새로운 언어로 소프트웨어를 다시 작성하는 것입니다. 그러나 코드를 다시 쓰는 것은 여러 가지 이유로 어려운 일입니다. 비용이 많이 들고 언어 산술과 같은 기본 언어 기능에도 미묘한 차이가 있으며 작업 시스템을 갖기까지 오랜 시간이 걸릴 수 있습니다. 결합하여, 이는 고위험 소프트웨어 개발 프로젝트를 다시 작성합니다. 이러한 종류의 다시 쓰기는 보안을 향상시키기 위해 수행되지 않을 것입니다. 우리는 기존 C 코드가 점차적으로 그리고 훨씬 저렴한 비용으로 향상 될 수있는 점진적인 접근법을 추구하기로 결정했습니다.

많은 대학과 회사의 연구원들은 메릴랜드 대학교, 로체스터 대학교, 워싱턴 대학교, 삼성, 러거 대학교, 펜실베이니아 대학교의 C. 연구원들에게 기여했다.

행동 강령

이 프로젝트는 행동 강령을 채택했습니다.