checkedc
Version 1.0 of the Checked C specification
ตรวจสอบ C ขยาย C พร้อมการตรวจสอบขอบเขตและความปลอดภัยประเภทที่ดีขึ้น ช่วยให้โปรแกรมเมอร์ติดตั้งรหัส C ที่มีอยู่ให้ปลอดภัยยิ่งขึ้น repo นี้มีข้อกำหนด C ที่ตรวจสอบรหัสตัวอย่างและรหัสทดสอบ
พอยน์เตอร์ไขมันเพื่อความปลอดภัยของหน่วยความจำชั่วคราวของ C โดย Jie Zhou, John Criswell และ Michael Hicks สิ่งนี้ปรากฏใน Oopsla 2023 มันอธิบายถึงส่วนขยายเพื่อตรวจสอบ C ที่เพิ่มพอยน์เตอร์ใหม่ที่ให้ความปลอดภัยของหน่วยความจำชั่วคราว
C เพื่อตรวจสอบ C โดย 3C โดย Aravind Machiry, John Kastner, Matt McCutchen, Aaron Eline, Kyle Headley และ Michael Hicks บทความนี้อธิบายถึงเครื่องมือ 3C แบบกึ่งอัตโนมัติสำหรับการแปลง C ให้ตรวจสอบ C. ได้รับรางวัล Sigplan Distinguished Paper Award ที่ Oopsla 2022
รูปแบบที่เป็นทางการของ Checked C โดย Liyi Li, Deena Postol, Leonida Lampropoulos, David Van Horn และ Michael Hicks สิ่งนี้ถูกตีพิมพ์ในปี 2022 IEEE 35th Computer Security Foundations Symposlium มันอธิบายรูปแบบที่เป็นทางการของ CEADED C. โมเดลถูกทำให้เป็นทางการโดยใช้ Prover THEOREM COQ
การบรรลุความปลอดภัยเพิ่มขึ้นด้วยการตรวจสอบ C. สิ่งนี้ถูกนำเสนอในการประชุมความปลอดภัยและความน่าเชื่อถือในปี 2562: บทความนี้อธิบายถึงรุ่นแรกของ 3C ที่แปลงรหัส C ที่มีอยู่เพื่อใช้ประเภท PTR นอกจากนี้ยังพิสูจน์ให้เห็นถึงคุณสมบัติการตำหนิเกี่ยวกับภูมิภาคที่ตรวจสอบซึ่งแสดงให้เห็นว่าภูมิภาคที่ตรวจสอบนั้นไม่มีที่ติสำหรับการทุจริตหน่วยความจำ หลักฐานนี้เป็นทางการสำหรับชุดย่อยหลักของส่วนขยายภาษา
ตรวจสอบ C: ทำให้ C ปลอดภัยโดยการขยายโดย David Tarditi, Samuel Elliott, Andrew Ruef และ Michael Hicks สิ่งนี้ปรากฏในการประชุมการพัฒนาความปลอดภัยทางไซเบอร์ IEEE 2018 มันอธิบายแนวคิดสำคัญของการตรวจสอบขอบเขต C ตรวจสอบใน 8 หน้า เราได้เพิ่มคุณสมบัติในการตรวจสอบ C ตั้งแต่นั้นมา วิกิและข้อกำหนดให้คำอธิบายที่ทันสมัยของการตรวจสอบ C.
มีโปสเตอร์ที่นำเสนอในการประชุม LLVM DEV 2019: "ล้นหายไป: ตรวจสอบ C เพื่อความปลอดภัยของหน่วยความจำ" โปสเตอร์ให้คำแนะนำเกี่ยวกับการตรวจสอบ C สรุปการใช้งานคอมไพเลอร์และนำเสนอการประเมินผลการทดลองของ CEADED C.
มีการพูดคุย (สไลด์) ในการประชุม DEV เสมือนจริงของปี 2020 LLVM: "ตรวจสอบ C: เพิ่มการสนับสนุนความปลอดภัยของหน่วยความจำให้กับ LLVM" การพูดคุยอธิบายการออกแบบของคำอธิบายประกอบขอบเขตสำหรับพอยน์เตอร์ที่ตรวจสอบและพอยน์เตอร์อาร์เรย์รวมถึงกรอบการทำงานสำหรับการตรวจสอบแบบคงที่ของความสมบูรณ์ของขอบเขต การพูดคุยยังอธิบายถึงอัลกอริทึมนวนิยายสั้น ๆ เพื่อขยายขอบเขตโดยอัตโนมัติสำหรับอาร์เรย์ที่สิ้นสุดแบบไม่มีค่าและสำหรับการเปรียบเทียบการแสดงออกเพื่อความเท่าเทียมกัน
เรามีความสุขที่ได้รับความช่วยเหลือ คุณสามารถมีส่วนร่วมได้โดยการลองตรวจสอบ C รายงานข้อบกพร่องและให้ข้อเสนอแนะกับเรา มีวิธีอื่นในการมีส่วนร่วมเช่นกัน
ซอฟต์แวร์ในที่เก็บนี้ครอบคลุมโดยใบอนุญาต MIT ดู File License.txt สำหรับใบอนุญาต Microsoft ภายใต้ข้อตกลงข้อกำหนดสุดท้ายของ OpenWeb Foundation Final, เวอร์ชัน 1.0 การมีส่วนร่วมของรหัสไปยัง repos LLVM/Clang ที่ตรวจสอบจะอยู่ภายใต้เงื่อนไขการออกใบอนุญาต LLVM/Clang
Checked C เป็นโครงการโอเพ่นซอร์สอิสระ มันเริ่มต้นจากโครงการวิจัยที่ Microsoft ในปี 2558 คล้ายกับ Checked C. เรากำลังมองหาวิธีการปรับปรุงความปลอดภัยของซอฟต์แวร์ระบบที่มีอยู่และกำจัดคลาสของข้อบกพร่อง
วิธีหนึ่งคือการเขียนซอฟต์แวร์ใหม่ในภาษาใหม่เช่น Rust อย่างไรก็ตามรหัสการเขียนใหม่นั้นมีความท้าทายด้วยเหตุผลหลายประการ: มีค่าใช้จ่ายสูงมีความแตกต่างเล็กน้อยในคุณสมบัติภาษาพื้นฐานเช่นเลขคณิตข้ามภาษาและอาจใช้เวลานานก่อนที่คุณจะมีระบบการทำงาน เมื่อรวมกันแล้วสิ่งนี้ทำให้การเขียนโครงการพัฒนาซอฟต์แวร์ที่มีความเสี่ยงสูง การเขียนใหม่เหล่านี้ไม่น่าจะทำเพียงเพื่อปรับปรุงความปลอดภัย เราตัดสินใจที่จะใช้วิธีการที่เพิ่มขึ้นซึ่งช่วยให้รหัส C ที่มีอยู่ได้รับการปรับปรุงอย่างค่อยเป็นค่อยไปและในราคาที่ต่ำกว่ามาก
นักวิจัยจากมหาวิทยาลัยและ บริษัท หลายแห่งมีส่วนร่วมในการตรวจสอบ C. นักวิจัยที่มหาวิทยาลัยแมริแลนด์มหาวิทยาลัยโรเชสเตอร์มหาวิทยาลัยวอชิงตันซัมซุงมหาวิทยาลัยรัทเกอร์และมหาวิทยาลัยเพนซิลเวเนียได้มีส่วนร่วมในการตรวจสอบ C. Apple ได้เสนอส่วนขยาย C
โครงการนี้ได้ใช้จรรยาบรรณ
