เทคโนโลยีการพิสูจน์ความถูกต้องของ Rust สำหรับโค้ดระบบระดับล่าง

 (github.com/verus-lang)
1 คะแนน โดย GN⁺ 2024-05-06 | 1 ความคิดเห็น | แชร์ทาง WhatsApp

เครื่องมือ Verus สำหรับการตรวจสอบความถูกต้องของโค้ด Rust

  • Verus คือเครื่องมือสำหรับการพิสูจน์ความถูกต้องของโค้ดที่เขียนด้วยภาษา Rust
  • นักพัฒนาสามารถเขียนสเปกที่โค้ดควรปฏิบัติตามได้ และ Verus จะตรวจสอบแบบคงที่ว่าโค้ด Rust ที่สามารถรันได้สอดคล้องกับสเปกนี้ในทุกเส้นทางการทำงานที่เป็นไปได้เสมอ
  • แทนที่จะเพิ่มการตรวจสอบระหว่างการรันไทม์ Verus อาศัย solver ที่ทรงพลังเพื่อพิสูจน์ว่าโค้ดทำงานได้อย่างถูกต้อง
  • ขณะนี้ Verus รองรับเฉพาะ subset ของ Rust (กำลังขยายตัวอยู่) และบางครั้งช่วยให้นักพัฒนาสามารถตรวจสอบความถูกต้องของโค้ดในเชิงสถิติเกินขอบเขตระบบชนิดของ Rust มาตรฐานได้ (เช่น การจัดการตัวชี้ดิบ)

สถานะปัจจุบันของ Verus

  • Verus กำลังพัฒนาอย่างแข็งขัน
  • อาจมีกรณีที่ฟังก์ชันขัดข้องหรือขาดหายได้ และเอกสารก็ยังไม่สมบูรณ์
  • หากต้องการลองใช้ Verus ควรเตรียมพร้อมที่จะขอความช่วยเหลือใน Zulip

ทดลองใช้งาน Verus

  • หากต้องการลองใช้งาน Verus บนเว็บเบราว์เซอร์ ให้ไปที่ Verus Playground
  • สำหรับการพัฒนาที่ซับซ้อนมากขึ้น ให้ปฏิบัติตามคำแนะนำการติดตั้ง เริ่มจากบทช่วยสอนและเอกสารอ้างอิง แล้วตรวจสอบเอกสารด้านล่าง

เอกสาร Verus

  • บทช่วยสอนและเอกสารอ้างอิง
  • เอกสาร API ของไลบรารีมาตรฐาน Verus
  • คู่มือการพิสูจน์ความถูกต้องสำหรับโค้ดแบบพร้อมกัน
  • เป้าหมายโครงการ
  • การมีส่วนร่วมใน Verus
  • ใบอนุญาต

ติดต่อ ร้องขอ issue และเริ่มการสนทนา

  • ใน GitHub ให้รายงาน issue หรือเริ่มการอภิปราย และหากต้องการรับความช่วยเหลือแบบเรียลไทม์ให้เข้าร่วม Zulip
  • สำหรับปัญหาที่ทำซ้ำได้ของฟังก์ชันที่มีอยู่ (bug) ให้ใช้ GitHub Issues และสำหรับการสนทนาแบบเปิดกว้างเกี่ยวกับคำขอฟีเจอร์และฟีเจอร์ที่วางแผนไว้ล่วงหน้า ให้ใช้ GitHub Discussions
  • ยินดีต้อนรับการมีส่วนร่วม หากต้องการร่วมพัฒนาโค้ดให้ดูเคล็ดลับการมีส่วนร่วมใน Verus

ความคิดเห็นของ GN⁺

  • Rust เป็นภาษาที่มีชื่อเสียงด้านความปลอดภัยและประสิทธิภาพสูงสำหรับการเขียนโปรแกรมระบบ Verus ดูเป็นโครงการที่น่าจะเสริมข้อดีเหล่านี้ของ Rust ได้มากขึ้น โดยเฉพาะฟังก์ชันการพิสูจน์ความถูกต้องด้าน concurrent programming ที่ดูน่าสนใจมาก
  • อย่างไรก็ตาม Verus ยังอยู่ในระยะเริ่มต้น และการรองรับไวยากรณ์ของ Rust ดูยังมีข้อจำกัด ทำให้ยังต้องพัฒนาเพิ่มหากต้องการนำไปใช้งานจริงใน production ได้ แต่ด้วยความสำคัญของการรับรองความปลอดภัยของโค้ดล่วงหน้าผ่านการวิเคราะห์แบบ static analysis จึงมีแนวโน้มเติบโตสูง
  • มีจุดที่ต้องพัฒนาหลายด้าน เช่น เอกสารยังไม่ครบ และการรองรับไวยากรณ์ที่จำกัด แต่ระยะยาวแล้วดูเหมือนจะเป็นโครงการที่มีบทบาทสำคัญในระบบนิเวศ Rust โดยเฉพาะในงานระบบโปรแกรมหรือบล็อกเชนที่ต้องการความเชื่อถือได้สูง

บทความที่เกี่ยวข้อง

1 ความคิดเห็น

 
GN⁺ 2024-05-06
ความคิดเห็นจาก Hacker News
  • เขียน Kubernetes controller ที่ผ่านการตรวจสอบอย่างเป็นทางการด้วย Verus
    • สามารถพิสูจน์คุณสมบัติแบบ liveness ได้ว่า controller จะปรับคลัสเตอร์ให้ตรงกับ desired state ที่ต้องการเสมอในที่สุด
    • การกำหนดความถูกต้องมีความละเอียดอ่อนและหลายแง่มุมมาก (เช่น ความต้องการของ desired state ที่เปลี่ยนเร็ว, ลักษณะ asynchronous, ความล้มเหลว และอื่นๆ)
    • โค้ดอยู่ที่ ลิงก์ GitHub และเชื่อมกับ paper ที่กำลังตีพิมพ์ใน OSDI 2024
  • ก้าวเล็กๆ สู่ Verus โดยการใช้ debug_assert ของ Rust เพื่อเพิ่มเงื่อนไขก่อนและหลัง
    • ตัวคอมไพล์ของ Rust จะลบออกโดยอัตโนมัติใน production build
    • มีตัวอย่างในบทช่วยสอนของ Verus และตัวอย่างการเช็กแบบ runtime ด้วย debug_assert
  • คำถามสำหรับผู้เริ่มต้นเรื่องความแตกต่างระหว่าง "การพิสูจน์ความถูกต้องของโค้ด" กับ "การพิสูจน์ว่าโค้ดถูกต้อง"
    • ถามว่ามีแหล่งเรียนรู้ที่ดีๆ เกี่ยวกับการ "พิสูจน์" โค้ดสำหรับวิศวกรภาคสนามที่มีพื้นฐาน CS/คณิตไม่แข็งแรงหรือไม่
    • คิดอยากรู้ว่าทำไม zero-knowledge proof จึงสำคัญ และทำไมมันถึงเกี่ยวข้องมากขนาดนั้น
  • Rust ยังไม่มี standard แบบเดียวกับ C/C++, Common Lisp, Ada/SPARK2014
    • เปรียบเทียบกับเครื่องมือ verification ที่พัฒนาสำหรับ Ada/SPARK2014 เป็นต้น มันเป็นเป้าหมายที่เปลี่ยนแปลงได้ (moving target)
  • Dafny คือภาษาการเขียนโปรแกรมที่รองรับการตรวจสอบ (verification-aware programming language) ที่สามารถคอมไพล์เป็น Rust ได้ (ลิงก์ GitHub)
  • หนึ่งในผู้ร่วมพัฒนาหลักได้ทำการนำเสนอ Verus ที่ยอดเยี่ยมใน Rust meetup ที่ซูริก (ลิงก์ YouTube)
    • สิ่งที่น่าประทับใจคือ code แบบ ghost เข้ากับโปรแกรมได้อย่างสวยงาม (ทำให้นึกถึง Ada เล็กน้อย)
  • การเปรียบเทียบ Verus กับ SPARK
    • มันเป็นตัวตรวจสอบอัจฉริยะในคลาสเดียวกันหรือไม่? นอกจากตรงที่ Verus เป็นตัวตรวจสอบสำหรับ Rust ไม่ใช่ Ada แล้ว มันต่างกันอย่างไรอีก?
  • ใครที่ชำนาญ Verus อธิบายความแตกต่างด้าน performance และ expressiveness ระหว่าง Verus กับ Lean4 ได้ไหม
    • ผมเข้าใจว่า Verus คือเครื่องมือที่พึ่งพา SMT และ Lean เป็น interactive theorem prover และเครื่องมือที่พึ่ง SMT
    • อย่างไรก็ตามความเข้าใจในสาขา formal verification ยังจำกัด จึงน่าจะได้ฟังความคิดเห็นจากผู้เชี่ยวชาญด้านเทคนิค formal methods ในซอฟต์แวร์
  • Verus กับ Kani มีความสัมพันธ์กันไหม? ทำงานต่างกันอย่างไร? (ลิงก์ GitHub ของ Kani)
  • มีวิธีทำให้รหัสที่ได้กลับมาเป็น Rust code ที่คอมไพล์ผ่านเครื่องมือ Rust แบบ vanilla ได้อยู่ดีหรือไม่