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

 (github.com/verus-lang)
1 คะแนน โดย GN⁺ 2024-05-06 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • Verus เป็นเครื่องมือสำหรับตรวจพิสูจน์ความถูกต้องของโค้ดที่เขียนด้วย Rust โดยเมื่อนักพัฒนาระบุสิ่งที่โค้ดควรทำเป็น สเปก แล้ว เครื่องมือจะตรวจสอบแบบสแตติกว่าโค้ด Rust ที่รันได้จะสอดคล้องกับสเปกนั้นในการทำงานที่เป็นไปได้ทั้งหมดหรือไม่
  • ใช้วิธีพิสูจน์ว่าโค้ดถูกต้องด้วย solver ที่ทรงพลังโดยไม่เพิ่มการตรวจสอบขณะรันไทม์ และปัจจุบันยังรองรับเพียงบางส่วนของ Rust
  • ในบางกรณีสามารถตรวจสอบแบบสแตติกได้แม้กระทั่งความถูกต้องของโค้ดที่จัดการ raw pointer ซึ่งเกินขอบเขตของระบบชนิดข้อมูลมาตรฐานของ Rust
  • โครงการนี้ยังอยู่ในช่วง พัฒนาอย่างต่อเนื่อง และอาจมีฟังก์ชันที่เสีย ใช้งานไม่ได้ หรือยังขาดอยู่ รวมถึงเอกสารที่ยังไม่สมบูรณ์ ดังนั้นผู้ใช้ควรเตรียมพร้อมขอความช่วยเหลือผ่าน Zulip
  • มี Verus Playground สำหรับใช้งานบนเบราว์เซอร์ รวมถึงคำแนะนำการติดตั้ง บทช่วยสอนและเอกสารอ้างอิง เอกสาร API ของไลบรารีมาตรฐาน คู่มือการพิสูจน์โค้ดแบบทำงานพร้อมกัน ตลอดจนตัวอย่างและการทดสอบสำหรับใช้เรียนรู้และทดลอง

Verus ตรวจพิสูจน์อะไรบ้าง

  • Verus เป็นเครื่องมือสำหรับตรวจพิสูจน์ความถูกต้องของโค้ด Rust
  • นักพัฒนาจะเขียนพฤติกรรมที่โค้ดต้องทำเป็น สเปก
  • Verus จะตรวจสอบแบบสแตติกว่าโค้ด Rust ที่รันได้จะสอดคล้องกับสเปกนั้นเสมอในการทำงานที่เป็นไปได้ทั้งหมดหรือไม่
  • แทนที่จะเพิ่มการตรวจสอบขณะรันไทม์ Verus ใช้ solver เพื่อพิสูจน์ว่าโค้ดนั้นถูกต้อง
  • ขอบเขตการรองรับในปัจจุบันยังเป็นเพียง ส่วนย่อย ของ Rust และกำลังมีการขยายการรองรับให้กว้างขึ้น
  • ในบางกรณีสามารถตรวจสอบแบบสแตติกความถูกต้องของโค้ดที่เกินกว่าระบบชนิดข้อมูลมาตรฐานของ Rust ได้ เช่น โค้ดที่จัดการ raw pointer

สถานะการพัฒนาและข้อควรระวังในการใช้งาน

  • Verus เป็นโครงการที่อยู่ระหว่าง พัฒนาอย่างต่อเนื่อง
  • ฟังก์ชันบางอย่างอาจเสียหรือยังขาดอยู่
  • เอกสารยัง ไม่สมบูรณ์
  • หากต้องการลองใช้ Verus ควรเตรียมพร้อมขอความช่วยเหลือผ่าน Zulip
  • ชุมชน Verus ได้เผยแพร่งานวิจัยหลายฉบับ และมีโครงการหลากหลายทั้งจากภาคอุตสาหกรรมและภาควิชาการที่ใช้งาน Verus
  • สามารถดูรายการที่เกี่ยวข้องได้ที่หน้า publications and projects

วิธีเริ่มต้นและเครื่องมือพัฒนา

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

เอกสารและสื่อการเรียนรู้

  • ทรัพยากรเอกสารที่กำลังพัฒนาอยู่ประกอบด้วย
    • Tutorial and reference: บทช่วยสอนและเอกสารอ้างอิงของ Verus
    • API documentation for Verus's standard library: เอกสาร API ของไลบรารีมาตรฐานของ Verus
    • Guide for verifying concurrent code: คู่มือสำหรับ การพิสูจน์โค้ดแบบทำงานพร้อมกัน
    • Contributing to Verus
    • Best Practices สำหรับการเผยแพร่ crate ที่เกี่ยวข้องกับ Verus ไปยัง crates.io
    • Verus License
    • Verus Logos

ตัวอย่างและการมีส่วนร่วมกับชุมชน

  • ตัวอย่างการใช้งาน Verus นอกเหนือจากเอกสาร ยังมีจุดเริ่มต้นอีกหลายแบบ
    • Publications and projects: สิ่งพิมพ์และโครงการที่ใช้ Verus
    • Videos, slides, and exercises: วิดีโอ สไลด์ และแบบฝึกหัดจากบทช่วยสอน Verus แบบหนึ่งวัน
    • Standalone examples: ตัวอย่างแยกเดี่ยวที่ใช้ Verus กับงานขนาดเล็กและเฉพาะเจาะจง
    • Small and medium-sized examples: ตัวอย่างที่แสดงความสามารถหลากหลายของ Verus
    • Unit tests: ชุดทดสอบที่มีตัวอย่างไวยากรณ์และฟังก์ชันของ Verus
  • การรายงานปัญหาและการสนทนาสามารถทำได้ผ่าน GitHub หรือ Zulip
  • สำหรับคำขอฟีเจอร์และการพูดคุยแบบเปิดใช้ GitHub discussions ส่วนบั๊กที่เกิดขึ้นซ้ำได้ของฟังก์ชันที่มีอยู่ให้ส่งใน GitHub issues
  • หากต้องการมีส่วนร่วมกับโค้ด สามารถดูคำแนะนำได้ใน Contributing to Verus

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

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

 
GN⁺ 2024-05-06
ความคิดเห็นจาก Hacker News

  • เคยลองเขียน Kubernetes controller ที่ผ่านการพิสูจน์เชิงรูปแบบด้วย Verus
    โดยพื้นฐานแล้วสามารถพิสูจน์ คุณสมบัติด้านความมีชีวิต ได้ เช่น “ในที่สุด controller จะปรับคลัสเตอร์ให้เข้าสู่สถานะเป้าหมายที่ร้องขอ”
    แต่เมื่อคำนึงถึงกรณีที่สถานะเป้าหมายเปลี่ยนเร็ว ความไม่ประสานเวลา ความล้มเหลว ฯลฯ แม้แต่การระบุว่าอะไรคือ “ความถูกต้อง” เองก็มีจุดละเอียดอ่อนอยู่มาก
    โค้ด: https://github.com/vmware-research/verifiable-controllers/, และบทความที่เกี่ยวข้องมีกำหนดจะตีพิมพ์ใน OSDI 2024

    • สงสัยว่ามันทำอะไรได้มากกว่าการทดสอบหน่วยบ้าง

  • ในฐานะก้าวเล็ก ๆ ไปสู่ Verus สามารถลองใส่ debug_assert ของ Rust เป็นเงื่อนไขก่อนและเงื่อนไขหลังได้
    โดยปกติ Rust compiler จะตัดสิ่งนี้ออกใน production build
    ตัวอย่างการตรวจพิสูจน์ในบทเรียน Verus จะเขียนช่วงอินพุตและเงื่อนไขของผลลัพธ์ด้วย requires และ ensures ส่วนเวอร์ชันตรวจสอบขณะรันไทม์ก็จะตรวจเงื่อนไขเดียวกันระหว่างรัน เช่น debug_assert(-16 <= x1), debug_assert(x8 == 8 * x1)

    • ปัญหาหนึ่งของ ไวยากรณ์ Verus ตอนนี้คือ ต้องครอบโค้ดทั้งหมดด้วย procedural macro
      เครื่องมือ Rust สำหรับการพิสูจน์/การตรวจพิสูจน์/การออกแบบแบบสัญญาอื่น ๆ เช่น Creusot ใช้ไวยากรณ์แบบ attribute ซึ่งโดยทั่วไปเบากว่าและให้ความรู้สึกเป็น Rust มากกว่า
      คงจะดีถ้า Verus รุ่นถัดไปทำแบบนี้ได้ด้วย
    • อยากให้มีคนใช้ assert แบบนี้มากขึ้น
      มันยอดเยี่ยมมากในฐานะเครื่องมือเอกสาร และช่วยเสริม type system กับการทดสอบได้ดีมาก
    • อาจลองใช้ crate "contracts" ได้เช่นกัน: https://docs.rs/contracts/latest/contracts/
    • ตัวอย่าง Verus คล้ายกับวิธีที่ฉันเขียนโค้ด Clojure
      คือใส่ เงื่อนไขก่อนและเงื่อนไขหลัง ให้กับฟังก์ชันส่วนใหญ่ และบน JVM ก็มีแฟล็กที่เอาสิ่งเหล่านี้ออกจาก production build ได้ง่าย

  • ในฐานะคนที่ไม่มีประสบการณ์ด้านวิทยาการคอมพิวเตอร์จริงจังมากนัก สงสัยว่าใน README ที่บอกว่า “ตรวจพิสูจน์ความถูกต้องของโค้ด” คำว่า การตรวจพิสูจน์ ต่างจากคำว่า “การพิสูจน์” ที่พูดในที่อื่นอย่างไร?
    แล้วก็อยากรู้ว่ามีสื่อไหนบ้างที่เหมาะกับโปรแกรมเมอร์สายงานจริงที่ไม่ได้มีพื้นฐานคณิตศาสตร์/วิทยาการคอมพิวเตอร์เข้มมาก แต่อยากเรียนเรื่อง “การพิสูจน์” ของโค้ด
    อีกอย่างคือยังไม่ค่อยเข้าใจว่าทำไม zero-knowledge proof ถึงสำคัญและเกี่ยวข้องมากนัก เช่นเคยได้ยินคนพูดถึง x.com/ZorpZK แต่ไม่เข้าใจว่ามันเจ๋งตรงไหน

    • มี Software Foundations ซึ่งเป็นแหล่งเรียนรู้ที่ดีสำหรับการเรียนการตรวจพิสูจน์โค้ดควบคู่กับ functional programming: https://softwarefoundations.cis.upenn.edu
      อย่างไรก็ตาม Verus กับ Coq ที่ใช้ใน Software Foundations มีแนวทางต่างกัน
      Verus พยายามพิสูจน์คุณสมบัติโดยอัตโนมัติด้วย SMT solver ซึ่งเป็นระบบแก้ข้อจำกัดอัตโนมัติ ส่วน Coq ต้องพิสูจน์ด้วยมือมากกว่ามาก และการทำอัตโนมัติมีจำกัด
      ทั้งสองแบบมีข้อดีข้อเสีย และระบบอัตโนมัติก็ดีมากเมื่อมันใช้ได้ แต่จะน่าหงุดหงิดเมื่อมันใช้ไม่ได้
      zero-knowledge proof ควรมองว่าเป็นอีกสาขาหนึ่งจะเหมาะกว่า และหลายคนที่ทำงานด้านการตรวจพิสูจน์/การพิสูจน์เชิงรูปแบบก็ไม่ได้แตะมันเลย มองเป็น primitive ทางคริปโตจะดีกว่า
    • ในที่นี้ใช้คำว่า การตรวจพิสูจน์ กับ การพิสูจน์ ในความหมายเดียวกัน และตรงช่วงท้ายของย่อหน้าแรกก็ชัดเจนแบบนั้น
      ส่วน zero-knowledge proof ยังมี overhead สูง และยังขาดสิ่งที่เรียกว่า “killer app” จึงยังไม่ได้มีประโยชน์ใช้สอย ความสำคัญ หรือความเกี่ยวข้องมากนัก แต่ในเชิงแนวคิดก็น่าสนใจ
    • ในบริบทนี้ “การตรวจพิสูจน์” กับ “การพิสูจน์” คือเรื่องเดียวกัน
      สื่อการเรียนรู้ฉันเองก็อยากให้มีมากกว่านี้ เอกสารของ Dafny ค่อนข้างดี แต่การตรวจพิสูจน์ซอฟต์แวร์เชิงรูปแบบยังดูไม่ถึงขั้นที่โปรแกรมเมอร์ทั่วไปซึ่งไม่ได้จบปริญญาเอกด้านคอมพิวเตอร์/คณิตศาสตร์จะหยิบมาใช้ได้สะดวก
      ดูจากตัวอย่างเหมือนจะค่อนข้างง่าย แต่ไม่นานก็จะเจอจุดที่ “พิสูจน์ไม่ได้” แล้วคำอธิบายว่าทำไมก็มักพาไปสู่รายละเอียดการติดตั้งภายในลึก ๆ ที่น่าจะมีแต่ผู้เขียนเครื่องมือเท่านั้นที่รู้
    • เท่าที่ฉันเข้าใจ zero-knowledge proof ช่วยให้พิสูจน์ได้ว่าคุณรู้บางสิ่ง โดยไม่ต้องเปิดเผยว่าสิ่งนั้นคืออะไร
      ตัวอย่างเช่น คุณสามารถยืนยันได้ว่าคุณรู้รหัสผ่านโดยไม่ต้องส่งรหัสผ่านให้เซิร์ฟเวอร์ จึงทำให้เซิร์ฟเวอร์อันตรายหรือผู้โจมตีแบบ man-in-the-middle ขโมยรหัสผ่านได้ยากขึ้น
      มันยังเปิดทางเลือกที่ดีกว่าสำหรับการยืนยันตัวตนได้ด้วย เช่นพิสูจน์ว่าคุณมีบัตรประจำตัวที่รัฐบาลออกให้โดยไม่ต้องส่งเอกสารจริงให้เซิร์ฟเวอร์ จึงลดปัญหาการเก็บข้อมูลไว้ “สูงสุด 2 ปี/3 ปี/6 เดือน” แล้วสุดท้ายก็รั่วไหล
    • ฉันมองว่าคำว่า “โปรแกรมเมอร์สายงานจริงพิสูจน์โค้ด” ยังแทบจะเป็นคำที่ขัดกันในตัว
      การพิสูจน์เกี่ยวกับโค้ดยังไม่ใช่งานที่โปรแกรมเมอร์สายงานจริงทำกัน
      ตรรกะแบบ Hoare เป็นจุดเริ่มต้นที่ดี และบางครั้งก็มีสอนในวิชาพื้นฐานวิทยาการคอมพิวเตอร์
      Coq มีเส้นโค้งการเรียนรู้ที่ชัน และจะยิ่งยากถ้าไม่คุ้นกับ OCaml หรือภาษาใกล้เคียง Why3 อาจเป็นมิตรกับผู้เริ่มต้นมากกว่า: https://www.why3.org
      การพิสูจน์กับการตรวจพิสูจน์อาจหมายถึงสิ่งเดียวกันก็ได้ แต่คำว่าการพิสูจน์ให้ความรู้สึกเชิงโต้ตอบมากกว่า ขณะที่การตรวจพิสูจน์ให้ความรู้สึกว่าสามารถทำให้เป็นอัตโนมัติได้ เช่น model checking หรือการแก้ SMT สำหรับโปรแกรมที่ใส่คำอธิบายกำกับไว้

  • ถ้าใครยังไม่รู้จักโครงการคล้ายกัน Dafny คือ “ภาษาโปรแกรมที่ตระหนักรู้เรื่องการตรวจพิสูจน์” ซึ่งคอมไพล์เป็น Rust ได้: https://github.com/dafny-lang/dafny

  • ดูน่าสนใจมาก ถ้ามีคำแนะนำหรือตัวอย่างเกี่ยวกับวิธี เพิ่ม proof เข้าไปในโค้ดเบสที่มีอยู่เดิมก็น่าจะเป็นประโยชน์กับคนจำนวนมาก
    ยกตัวอย่างเช่น แอป GUI แบบเล็กที่สุดที่มีแค่กล่องข้อความหนึ่งกล่อง รับอาร์เรย์ที่เชื่อถือไม่ได้และไม่อาจรู้ได้ตอนคอมไพล์ผ่าน HTTP request จากนั้นนำไป bubble sort แล้วแสดงผล
    ใน bubble sort มีบั๊กที่ใส่ไว้โดยตั้งใจ เช่น off-by-one error ที่ทำให้องค์ประกอบสุดท้ายยังคงค้างอยู่ และ unit test ก็อาจพลาดไม่เจอบั๊กนั้นโดยบังเอิญ ความกังวลว่าการทดสอบอาจไม่สมบูรณ์อาจเป็นแรงจูงใจหลักในการหันไปใช้ proof
    จากนั้นถ้าแสดงให้เห็นกระบวนการแทนที่ unit test ด้วย proof พร้อมทั้งค้นพบบั๊กและแก้ไขมันไปด้วยก็น่าจะดี
    ไม่จำเป็นต้องอธิบายรายละเอียดของโค้ด proof เองมากนัก แต่ควรโฟกัสที่รายละเอียดเชิงปฏิบัติ เช่น ขอบเขตระหว่างโค้ดคณิตศาสตร์ที่พิสูจน์แล้วกับโค้ด I/O ที่ยังไม่ได้พิสูจน์, command line ที่ใช้สำหรับ proof และการ build, หรือ zip archive ที่คนเอาไปลองเล่นเองได้
    อันที่จริง แค่อ่านจาก standard input แล้วเขียนไปที่ standard output ก็น่าจะเพียงพอแล้ว

  • หนึ่งในผู้มีส่วนร่วมหลักเคยพูดเกี่ยวกับ Verus ได้ยอดเยี่ยมมากใน Zürich Rust meetup: https://www.youtube.com/watch?v=ZZTk-zS4ZCY
    ประทับใจที่โค้ด “ghost” แบบนี้เข้ากับโปรแกรมได้อย่างแนบเนียนมาก และก็ทำให้นึกถึง Ada ขึ้นมานิดหน่อย

  • สงสัยว่า Rust เองมี มาตรฐาน อยู่แล้วแบบที่ C/C++, Common Lisp, Ada/SPARK2014 มีหรือยัง
    ถ้ายังไม่มี เวลานำไปเทียบกับเครื่องมือตรวจพิสูจน์ที่พัฒนาสำหรับ Ada/SPARK2014 ก็จะเหมือนเป็นเป้าที่ขยับตลอดเวลา
    อีกทั้งมรดกของ Ada/SPARK2014 ที่ครอบคลุมตั้งแต่ bare metal ไปจนถึงแอปพลิเคชันความปลอดภัยเชิงวิกฤตที่มีความถูกต้องสูงก็เป็นสิ่งที่มองข้ามได้ยาก

  • สงสัยว่ามันมีความสัมพันธ์อะไรกับ Kani บ้าง ทำงานต่างกันไหม?
    https://github.com/model-checking/kani

    • โดยทั่วไป model checker จะสำรวจสถานะได้เพียงจำนวนจำกัด จึงมีประสิทธิภาพในการหาบั๊ก และหลายครั้งก็ไม่ต้องใส่คำอธิบายประกอบเพิ่มในโปรแกรม
      ส่วนตัวตรวจพิสูจน์อัตโนมัติที่อิง SMT อย่าง Verus, Dafny, F* และ VCC ของฉัน มักต้องใส่คำอธิบายประกอบให้แทบทุกฟังก์ชันและทุกลูป แต่ให้การรับประกันที่กว้างกว่ามากเกี่ยวกับความถูกต้องของโปรแกรม
      ขณะที่เครื่องมือที่อิง interactive prover อย่าง Coq หรือ Lean มักต้องอาศัยการชี้นำจากผู้ใช้มากกว่า แต่ก็สามารถรับประกันคุณสมบัติที่ซับซ้อนกว่าได้

  • สงสัยว่า Verus เทียบกับ SPARK แล้วเป็นอย่างไร
    มันอยู่ในกลุ่มทั่วไปเดียวกันของตัวตรวจพิสูจน์หรือไม่? นอกจากจะเป็นตัวตรวจพิสูจน์สำหรับ Rust แทนที่จะเป็นของ Ada แล้ว Verus ต่างออกไปอย่างไร?

  • ถ้ามีคนที่รู้จัก Verus ดีช่วยอธิบายความต่างด้านประสิทธิภาพและพลังในการแสดงออกระหว่าง Verus กับ Lean4 ได้ก็น่าจะดี
    ฉันเข้าใจว่า Verus เป็นเครื่องมือตรวจพิสูจน์ที่อิง SMT ส่วน Lean เป็นทั้ง interactive prover และก็เป็นเครื่องมือที่อิง SMT ด้วย
    แต่ฉันยังมีความเข้าใจเรื่อง formal verification ค่อนข้างจำกัด เลยอยากรู้มุมมองจากคนที่เชี่ยวชาญ formal methods สำหรับซอฟต์แวร์

    • Lean คล้ายกับ Coq
      ยกตัวอย่างเช่น คุณสามารถตั้งข้อความอ้างเกี่ยวกับโค้ด C แล้วพิสูจน์มันได้เหมือนในหนังสือ “Software Foundations” ของ Coq แต่ดูเหมือนแทบไม่มีใครทำแบบนั้นด้วย Lean และเครื่องมือก็ยังมีไม่มาก
      คุณยังสามารถเขียนโปรแกรมด้วย Lean4 แล้วพิสูจน์เกี่ยวกับโปรแกรมนั้นได้ด้วย ซึ่งก็มีบางคนทำอยู่เล็กน้อย
      ปัจจุบัน วิธีใช้งานหลักของ Lean4 และ Coq คือการทำ formalization ของคณิตศาสตร์บริสุทธิ์และตีพิมพ์งานวิจัยจากสิ่งนั้น
      ประเภทของสิ่งที่ Lean/Coq สามารถระบุและพิสูจน์ได้จริงนั้นมีความทั่วไปมากกว่า แต่กับโปรแกรมในโลกความเป็นจริง ความทั่วไประดับนั้นอาจไม่จำเป็นเสมอไป