แปล crate `core` และ `alloc` ของ Rust เป็น Coq เพื่อการตรวจพิสูจน์เชิงรูปนัย

 (formal.land)
1 คะแนน โดย GN⁺ 2024-05-16 | 1 ความคิดเห็น | แชร์ทาง WhatsApp
  • coq-of-rust ซึ่งใช้ย้ายโปรแกรม Rust ไปยัง Coq เริ่มรองรับ crate core และ alloc ของไลบรารีมาตรฐานแล้ว ช่วยลดภาระที่ก่อนหน้านี้ต้องเขียน นิยาม Coq ของฟังก์ชัน primitive ทีละตัวด้วยมือ
  • เนื่องจากทั้งสอง crate เป็นโค้ดเบสขนาดใหญ่ที่มีทั้ง unsafe และโค้ด Rust ขั้นสูงจำนวนมาก โจทย์สำคัญจึงอยู่ที่การจัดการผลลัพธ์จากการแปลให้อยู่ในหน่วยที่สามารถคอมไพล์และตรวจพิสูจน์ได้
  • เมื่อแยกผลลัพธ์ออกตามไฟล์ Rust ต้นทาง alloc มี 54 ไฟล์ 171,783 บรรทัด และ core มี 190 ไฟล์ 592,065 บรรทัด ทำให้คอมไพล์แบบขนานและดีบักได้ง่ายขึ้น
  • ปัญหา ชื่อโมดูลชนกัน ในบล็อก impl ถูกบรรเทาด้วยการใส่ข้อมูลจากเงื่อนไข where เพิ่มเข้าไป แต่ตอนนี้ยังมีไฟล์ที่คอมไพล์บน Coq ไม่ผ่านอยู่ 4% ของทั้งหมด
  • ตัวอย่าง Option::unwrap_or_default แสดงวิธีใช้งานโดยพิสูจน์ว่านิยามที่แปลอัตโนมัติกับนิยามเชิงฟังก์ชันแบบง่ายมีความสมมูลกัน ซึ่งต้องอาศัยทั้งความเชื่อมั่นต่อระบบอัตโนมัติและการตรวจสอบในขั้นพิสูจน์

การจัดการ primitive ของไลบรารีมาตรฐาน Rust

  • Formal Land กำลังพัฒนา coq-of-rust เพื่อแปลโปรแกรม Rust ไปยังระบบพิสูจน์เชิงรูปนัย Coq
  • ก่อนหน้านี้ เพื่อจัดการองค์ประกอบ primitive ของไลบรารีมาตรฐาน Rust จำเป็นต้องสร้าง นิยาม Coq แยกต่างหากเพื่ออธิบายพฤติกรรมของแต่ละฟังก์ชัน
    • ตัวอย่าง: Option::unwrap_or_default
    • การนิยามด้วยมือเป็นงานที่ซ้ำซากและแทรกข้อผิดพลาดได้ง่าย
  • เพื่อลดภาระนี้ จึงมีการแปล crate core และ alloc ของ Rust ด้วย coq-of-rust
  • สามารถดูผลลัพธ์การแปลได้ที่

ผลลัพธ์จากการรันแปลครั้งแรก

  • เมื่อนำ coq-of-rust ไปรันกับ alloc และ core ในครั้งแรก ได้ไฟล์ Coq 2 ไฟล์ขนาด หลายแสนบรรทัด ซึ่งแต่ละไฟล์ครอบคลุมทั้ง crate
  • แม้จะยืนยันได้ว่าเครื่องมือนี้ทำงานกับโค้ดเบสขนาดใหญ่ได้ แต่โค้ด Coq ที่สร้างขึ้นยังไม่สามารถคอมไพล์ได้ทันที
  • ข้อผิดพลาดไม่ได้เกิดถี่มากนัก แต่อยู่ในระดับประมาณหนึ่งจุดต่อทุก ๆ หลายพันบรรทัด
  • ขนาดของโค้ด Rust ต้นทางตาม cloc มีดังนี้
    • alloc: โค้ด Rust 26,299 บรรทัด
    • core: โค้ด Rust 54,192 บรรทัด
  • เนื่องจากมีการ ขยายแมโคร ระหว่างกระบวนการแปล เป้าหมายที่แปลจริงจึงมีขนาดใหญ่กว่าจำนวนบรรทัดต้นฉบับ

การแยกโค้ด Coq ที่สร้างขึ้น

  • การเปลี่ยนแปลงที่ใหญ่ที่สุดคือการแยกผลลัพธ์ของ coq-of-rust ให้เป็นไฟล์ Coq หนึ่งไฟล์ต่อไฟล์ Rust ต้นทางหนึ่งไฟล์
  • การแยกนี้ทำได้เพราะการแปล ไม่ไวต่อ ลำดับของนิยาม และมีลักษณะ context-free
  • โดยทั่วไปแล้ว ระหว่างไฟล์ Rust มักมีการพึ่งพาแบบวนกลับ ซึ่ง Coq ไม่อนุญาต แต่แนวทางการแปลนี้ยังคงแยกระดับไฟล์ได้
  • หลังแยกแล้ว ขนาดผลลัพธ์มีดังนี้
    • alloc: ไฟล์ Coq 54 ไฟล์, โค้ด Coq 171,783 บรรทัด
    • core: ไฟล์ Coq 190 ไฟล์, โค้ด Coq 592,065 บรรทัด
  • การแยกไฟล์ทำให้การสำรวจและดูแลรักษาโค้ดที่สร้างขึ้นง่ายขึ้น
    • คอมไพล์แบบ ขนาน ได้ง่าย
    • โฟกัสดีบักทีละไฟล์ได้
    • ตัดไฟล์ที่คอมไพล์ไม่ผ่านออกได้ง่าย
    • ติดตาม diff ของไฟล์เดี่ยวได้ง่าย

การแก้ปัญหาชื่อโมดูลชนกันและไฟล์ที่ยังเหลือ

  • บั๊กบางส่วนเกิดจาก ชื่อโมดูลชนกัน ในบล็อก impl
  • วิธีแก้คือใส่ข้อมูลในชื่อโมดูลให้มากขึ้นเพื่อเพิ่มความเป็นเอกลักษณ์
    • โดยเพิ่มข้อมูลจากเงื่อนไข where ที่ก่อนหน้านี้ยังไม่มี
    • ตัวอย่างเช่น ในการติดตั้ง trait Default ให้กับ Mapping<K, V> จะมีการสะท้อนเงื่อนไขที่ทั้ง K และ V ต้องติดตั้ง Default ด้วยลงไปในชื่อโมดูล
  • ปัจจุบันไฟล์ที่ยังคอมไพล์บน Coq ไม่ผ่านมีดังนี้
    • alloc/boxed.v
    • core/any.v
    • core/array/mod.v
    • core/cmp/bytewise.v
    • core/error.v
    • core/escape.v
    • core/iter/adapters/flatten.v
    • core/net/ip_addr.v
  • คิดเป็น 4% ของไฟล์ทั้งหมด
  • อย่างไรก็ตาม แม้ในไฟล์ที่คอมไพล์ได้ ก็ยังมีองค์ประกอบของ Rust ที่ระบบยังจัดการไม่ได้และถูกทำให้เป็นสัจพจน์อยู่ ดังนั้นสัดส่วนนี้เพียงอย่างเดียวจึงยังใช้ตัดสินขอบเขตที่ยังไม่รองรับทั้งหมดไม่ได้

ตัวอย่างการแปล Option::unwrap_or_default

  • Option::unwrap_or_default ของ Rust จะคืนค่า x เมื่อเป็น Some(x) และจะเรียก T::default() เมื่อเป็น None
  • coq-of-rust แปลสิ่งนี้เป็นนิยาม Coq ในรูปแบบ monadic
    • จับคู่กับอาร์กิวเมนต์ขาเข้าและชนิดข้อมูล
    • ในแขนง Some จะดึง tuple field มาและคัดลอกค่า
    • ในแขนง None จะเรียกเมธอด default ของ trait core::default::Default
  • ในการตรวจพิสูจน์จริง จะใช้ นิยามเชิงฟังก์ชัน ที่ง่ายกว่านี้แทนนิยามที่สร้างอัตโนมัติ
    • หากเป็น None จะคืน core.simulations.default.Default.default
    • หากเป็น Some x จะคืน x
  • การพิสูจน์ว่านิยามที่สร้างอัตโนมัติกับนิยามแบบง่ายมีความสมมูลกันอยู่ใน CoqOfRust/core/proofs/option.v
  • หากโค้ด Rust ต้นฉบับเปลี่ยนไป การพิสูจน์นี้จะช่วยจับความเปลี่ยนแปลงได้
  • เนื่องจากการแปลไลบรารี core ทำแบบอัตโนมัติ จึงอาจเชื่อถือในนิยามที่สร้างขึ้นได้มากกว่านิยามที่เขียนด้วยมือ
  • อย่างไรก็ตาม coq-of-rust เองก็อาจมีข้อผิดพลาดหรือความไม่สมบูรณ์อยู่ จึงจำเป็นต้องตรวจสอบความถูกต้องของโค้ดในขั้นตอนการพิสูจน์ด้วย

โจทย์ที่ยังเหลือ

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

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

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

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

  • น่าประทับใจจริง ๆ
    การแปลอัตโนมัติแบบนี้ย้ายเป้าหมายของความเชื่อถือไปอยู่ที่เครื่องมือ ตัว coq-of-rust เองเขียนด้วย Rust ไม่ใช่ Coq โครงสร้างแบบเวียนกลับจึงค่อนข้างน่าทึ่ง แต่ถ้าผสมแนวทางแบบ CompCert เข้ากับวิธีเลี่ยงการโจมตี Trusting Trust ของ Ken Thompson ด้วยคอมไพเลอร์ตัวที่สอง ตาม “Countering Trusting Trust through Diverse Double-Compiling” (2009) [0] ของ David A. Wheeler ก็ดูเหมือนจะพิสูจน์ความถูกต้องได้
    ในการตรวจสอบ ก็แปลงตัวแปล coq-of-rust จาก Rust เป็น Coq ด้วย coq-of-rust และแม้การแปลนั้นทำด้วย Rust จึงไม่จำเป็นต้องเชื่อถือ ก็พิสูจน์คุณสมบัติความถูกต้องที่ต้องการภายใน Coq ได้ โดยเฉพาะว่ามันรักษาความหมายไว้เมื่อแปลโปรแกรม Rust เป็น Coq
    อย่างในบทความ มีโอกาสสูงว่าการพิสูจน์ด้วยนิยามที่เป็นเชิงฟังก์ชันมากกว่านิยามที่สร้างออกมาจะง่ายกว่า ดังนั้นก็ทำกระบวนการพิสูจน์ความเทียบเท่าระหว่างนิยาม เหมือนที่ทำในไลบรารีมาตรฐานได้ ถ้าตัวแปล coq-of-rust ปัจจุบัน โดยเฉพาะ lib/ [1] มี Rust 6,350 บรรทัด การเขียนตัวแปลทั้งหมดเป็น Coq แล้วพิสูจน์ว่าเทียบเท่ากับสิ่งที่สร้างออกมาก็ดูเป็นไปได้จริง
    จากนั้นเมื่อนำตัวแปล coq-of-rust เวอร์ชัน Coq ที่พิสูจน์แล้วไปรันกับซอร์ส coq-of-rust ที่เขียนด้วย Rust นิยาม Coq ที่ได้ออกมาควรตรงกับเอาต์พุตของตัวแปล coq-of-rust เวอร์ชัน Rust ที่ใช้ในตอนแรก
    นอกเรื่องเล็กน้อย การได้เห็นงานแบบนี้มีเงินทุนจากอุตสาหกรรมสนับสนุนเป็นเรื่องดี แม้ผมจะค่อนข้างเย้ยหยันคริปโตเคอร์เรนซี แต่ก็จริงที่ความต้องการด้านความถูกต้องของวงการนั้นช่วยผลักดันการพัฒนาในสิ่งที่ผมสนใจ เช่น Rust, Coq และการสนับสนุนนักศึกษาปริญญาโทที่รู้จัก
    [0]: https://dwheeler.com/trusting-trust/wheelerd-trust.pdf
    [1]: https://github.com/formal-land/coq-of-rust/tree/main/lib

    • ผมเป็นหนึ่งในผู้เขียน และจริง ๆ แล้วขั้นตอนแบบนั้นอาจเป็นวิธีที่ดีสำหรับ การตรวจสอบ coq-of-rust ได้
      แต่แม้ตัวโค้ดเองจะสั้น ก็ยังพึ่งพาคอมไพเลอร์ Rust ในการพาร์สและตรวจชนิดของโค้ด Rust ที่รับเข้ามา ดังนั้นส่วนนั้นก็ต้องตรวจสอบด้วย หรืออย่างน้อยต้องมีสเปกเชิงรูปแบบแม้จะยังไม่มีการพิสูจน์ สิ่งที่เป็นอุปสรรคคือ API ของ rustc ค่อนข้างใหญ่และไม่เสถียร แต่ถึงอย่างนั้นก็อาจเป็นวิธีหนึ่งในการเพิ่มระดับความเชื่อถือได้
    • นึกถึงตอนที่เคยทำงานกับ SPARK Ada ในอดีต สำหรับโปรเจกต์ที่ไม่มีเป้าหมาย Ada รองรับ โดยเฉพาะบนอุปกรณ์ขนาดเล็กมาก ๆ เรามักแปลง Ada เป็น C แล้วคอมไพล์ไปยังเป้าหมายนั้น ทำให้ฝั่ง SPARK สามารถทำการวิเคราะห์เชิงสถิตได้หลายรูปแบบ
      แน่นอนว่ามีปัญหาเรื่องต้องตรวจสอบเอาต์พุตหรือตัวแปลง แต่โค้ด C ที่ได้ค่อนข้างอ่านง่ายเพื่อวัตถุประสงค์ในการตรวจสอบ และมีสไตล์ที่จำกัด รวมถึงมีความเชื่อมั่นต่อเครื่องมือสูงด้วย การวิเคราะห์เชิงสถิตของ SPARK เป็นเพียงส่วนหนึ่งของกระบวนการตรวจสอบและยืนยันทั้งหมด และการทดสอบกับกิจกรรมอื่น ๆ ก็ให้ชั้นความเชื่อมั่นเพิ่มเติม โดยรวมแล้วเป็นแนวทางที่ใช้ได้ผลค่อนข้างดี
    • เหตุผลที่คริปโตเคอร์เรนซีช่วยงานแบบนี้ ไม่ใช่แค่เพราะข้อจำกัดด้านความถูกต้อง แต่ยังเพราะความมั่งคั่งจำนวนมากถูกถ่ายโอนไปยัง คนที่สนใจวิทยาการคอมพิวเตอร์ ด้วย
      ที่พวกเขาใช้เงินนั้นกับการวิจัยวิทยาการคอมพิวเตอร์ ไม่ใช่แค่เพราะเป็นประโยชน์ต่อตัวเอง แต่ยังเป็นการทำกุศลที่เชื่อมโยงกับงานอดิเรกของพวกเขาด้วย
    • ผมยังไม่ค่อยเข้าใจว่าแนวทางนั้นจะป้องกันไม่ให้ คอมไพเลอร์ Rust ที่ใช้สร้างไบนารีฉีดเพย์โหลดอันตรายได้อย่างไร อาจสร้าง A เป็น B แล้วสร้าง B เป็น A จากนั้นเปรียบเทียบไบนารีได้ก็จริง
      อีกแนวทางหนึ่งคือโค้ดที่พกพาการพิสูจน์มาด้วย ให้คอมไพเลอร์ Rust ส่งออกการพิสูจน์ใน Coq แนบมาด้วยว่าเอาต์พุตไฟล์ปฏิบัติการสอดคล้องกับความหมายของซอร์สโค้ดอินพุต
      แน่นอนว่าอาจเขียนคอมไพเลอร์สำหรับซับเซตของ Rust เช่นไม่มี borrow checker หรือการปรับแต่งประสิทธิภาพ ให้เป็นภาษาเครื่องของสถาปัตยกรรมเฉพาะ แล้วบูตสแตรปทุกอย่างจากตรงนั้นก็ได้

  • โปรแกรมที่ตรวจสอบตั้งแต่ต้นจนจบด้วย ระบบพิสูจน์อนุมานกึ่งอัตโนมัติอย่าง Coq มักมีขนาดเล็ก ไลบรารีอาจง่ายกว่าเพราะโค้ดมีระดับการโต้ตอบกันต่ำกว่า แต่โปรแกรมทั่วไปไม่เป็นเช่นนั้น
    จริง ๆ แล้วการเพิ่มขึ้นของขนาดโปรแกรมที่ตรวจสอบได้ด้วยวิธีนี้เติบโตช้ากว่าการเพิ่มขึ้นของขนาดเฉลี่ยของโปรแกรมทั้งหมด การตรวจสอบซอฟต์แวร์แบบ sound คือการแสดงว่าเป็นไปตามสเปก 100% นั้นมีประโยชน์ชัดเจนในงานอย่างการพิสูจน์ความถูกต้องของอัลกอริทึมหลัก แต่ขยายขนาดได้ไม่ดี
    ด้วยเหตุนี้ งานวิจัยจึงมีแง่มุมที่ย้ายไปสู่วิธีแบบไม่ sound มากขึ้น ต้นทุนของการรับประกัน 100% อาจเป็น 10 เท่าของการรับประกัน 99.9999% และส่วนต่างของความน่าจะเป็นนั้นอาจเล็กกว่าความน่าจะเป็นของความล้มเหลวนอกซอฟต์แวร์ด้วยซ้ำ ระบบกายภาพตั้งแต่แรกก็พิสูจน์ไม่ได้ว่าเป็นไปตามสเปก และตัวสเปกเองก็มีความน่าจะเป็นที่จะไม่ตรงกับความเป็นจริงเพียงพอ

    • ประเด็นสำคัญคือ ถ้าพิสูจน์ ส่วน unsafe ของไลบรารีมาตรฐาน และการรับประกันความปลอดภัยของ Rust ได้ ก็จะพิสูจน์แบบส่งผ่านได้ว่าโค้ด Rust ที่ปลอดภัยทั้งหมดซึ่งใช้เฉพาะไลบรารีมาตรฐานมีความปลอดภัยของหน่วยความจำ ไม่มี data race เป็นต้น
      การพิสูจน์ว่าเฉพาะโค้ด unsafe ถูกต้องนั้นทำได้โดยใช้ความพยายามน้อยกว่าการพิสูจน์โค้ด Rust ทั้งหมดมาก นี่เป็นคำตอบต่อคำวิจารณ์ที่มักเกิดขึ้นเมื่อพูดถึงการรับประกันความปลอดภัยของ Rust ว่า “แล้วโค้ด unsafe ล่ะจะทำอย่างไร” ช่องว่างที่ระบบชนิดของ Rust ยังไม่ทรงพลังพอจะจัดการได้ สามารถเติมเต็มด้วยระบบที่แข็งแรงกว่าอย่าง Coq

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

    • รู้ไม่ได้ สุดท้ายก็ต้อง เชื่อถืออะไรบางอย่าง อยู่ดี เช่น ฮาร์ดแวร์ คอมไพเลอร์ สเปก เคอร์เนลที่เชื่อถือได้ของ Coq เป็นต้น
      การตรวจสอบเชิงรูปแบบมักถูกพูดถึงเหมือนกับว่าจะกำจัดความเป็นไปได้ของบั๊กได้ทั้งหมด แต่ในความเป็นจริงใกล้เคียงกับการลดโอกาสเกิดบั๊กลงอย่างมากมากกว่า ถึงอย่างนั้น การแปลอัตโนมัติระหว่าง Rust กับ Coq ก็ลดความซับซ้อนของสิ่งที่ต้องเชื่อถือลงได้มาก จึงควรถูกเลือกใช้มากกว่าการแปลด้วยมือ
    • เป็นข้อจำกัดที่ถูกต้อง แต่ก็ไม่ได้เลวร้ายขนาดนั้น
      ในหลายกรณี บั๊กในการแปลจะทำให้พิสูจน์ไม่ได้เฉย ๆ แล้วก็จะมีคนสืบว่าทำไมการพิสูจน์ถึงไม่ผ่าน จนพบว่ามีบั๊กในการแปล
      ปัญหาจริง ๆ คือกรณีที่บั๊กในการแปลไปหักล้างบั๊กในโค้ดต้นฉบับได้พอดี หากไม่มีความเสี่ยงเชิงระบบ การที่บั๊กสองตัวจะลบล้างกันแบบนี้ถือว่ามีโอกาสค่อนข้างต่ำ
    • โค้ดถูกแปลอัตโนมัติด้วย coq-of-rust หากพบปัญหาในการแปล ก็แก้ที่เครื่องมือ coq-of-rust ครั้งเดียว แล้วผลลัพธ์การแปลทั้งหมดก็จะถูกอัปเดต

  • สำหรับผู้อ่านที่สนใจ: ผมส่งบทความบล็อกนี้มาเพราะเนื้อหาเกี่ยวกับคริปโทเคอร์เรนซีโดยตรงน้อยกว่าบทความอื่น ๆ ในบล็อกเดียวกัน แต่ที่นั่นมีบทความที่น่าสนใจเชิงเทคนิคอีกมาก
    โดยเฉพาะสองบทความล่าสุดที่พูดถึงการนำแนวทางเดียวกันนี้ไปใช้กับ Python แทนที่จะเป็น Rust

  • จำได้ว่ามีการบรรยาย [1] เมื่อก่อนเกี่ยวกับ fuzzer ที่พบบั๊กใน คอมไพเลอร์ C ที่ตรวจสอบเชิงรูปแบบแล้ว เพราะการตรวจสอบเชิงรูปแบบไม่ได้ครอบคลุม frontend และ backend
    ผมเข้าใจว่ามีคำถามว่าเราจะเชื่อถือ Coq เองหรือการแปลได้แค่ไหน และก็สงสัยด้วยว่าจะซิงก์กับการอัปเดตของ Rust อย่างไร แต่แม้แต่การตรวจสอบเชิงรูปแบบที่สมบูรณ์แบบก็ไม่ได้หมายความว่าถูกต้อง 100% ตั้งแต่ต้นจนจบ
    [1] https://youtu.be/Ux0YnVEaI6A

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

    • ความปลอดภัยของ Rust แทบไม่เกี่ยวกับบั๊ก
      Rust มีนิยาม “safe” ของตัวเอง และถือได้ว่าเป็นส่วนย่อยของ memory safety แม้แต่โค้ด Rust ที่ปลอดภัยทั้งหมดก็ยังเกิด data race, deadlock, memory exhaustion ฯลฯ ได้ ยังไม่ต้องพูดถึงข้อผิดพลาดทางตรรกะ
    • ในระดับหนึ่ง ผมคิดว่านั่นคือความฝัน แต่มีเงื่อนไขเยอะ และต้องมีหลายอย่างลงตัว
      อย่างแรก ต้องทำให้ semantics ของ unsafe Rust เป็นรูปแบบทางการ งาน RustBelt[1] อันบุกเบิกของ Ralf Jung เป็นความก้าวหน้าครั้งใหญ่ แต่ยังไม่สมบูรณ์ โดยเฉพาะ pointer provenance กลายเป็นองค์ประกอบที่ยุ่งยาก
      อย่างที่สอง ในฐานะส่วนหนึ่งของเรื่องนั้น จำเป็นต้องมีโมเดลเชิงรูปแบบของ borrow checker Stacked borrows[2] เป็นความพยายามที่ดีแต่มีข้อบกพร่อง และ Tree borrows[3] อาจแก้ได้ หรืออาจมีบางอย่างที่ละเอียดกว่านั้นออกมาก็ได้
      อย่างที่สาม ต้องมีโมเดลหน่วยความจำเชิงรูปแบบ เรื่องนี้ส่วนใหญ่เกี่ยวกับพฤติกรรมของ atomic operations และ synchronization จึงสำคัญมากต่อองค์ประกอบของ standard library อย่าง Arc เป็นที่ยอมรับกันกว้างขวางว่าโมเดลหน่วยความจำของ Rust ควรคล้ายกับ C++ และต้องทำงานร่วมกันได้ แต่ยังเหลือปัญหา “out of thin air” และฟีเจอร์ที่ขาดไปอย่าง seqlock อยู่ นี่เป็นหนึ่งในเหตุผลที่ Linux kernel ยังใช้โมเดลของตัวเอง
      อย่างที่สี่ ต้องมีการพิสูจน์ว่าการรับประกันความปลอดภัยประกอบกันได้ดี โดยเฉพาะเมื่อโค้ดที่ sound ซึ่งเขียนด้วย unsafe Rust ถูกประกอบเข้ากับโค้ด safe Rust แล้ว การรับประกันความปลอดภัยต้องยังคงอยู่ จนถึงตอนนี้มีผลลัพธ์ที่ดี แต่ต้องพิสูจน์สำหรับทั้งระบบ
      อย่างที่ห้า เพื่อให้การพิสูจน์แบบนั้นใช้ได้กับทุกโค้ด ต้องปิดบั๊กด้าน soundness ที่ยังเหลืออยู่ใน Rust[1] ทั้งหมด ปัญหาจำนวนมากในกลุ่มนี้มีความสำคัญจริง ๆ แค่ในเชิงทฤษฎีหรือในโค้ดแบบมุ่งร้าย[5] ทำให้ความคืบหน้าช้า
      แม้ทั้งหมดนี้เสร็จแล้ว ก็ยังเป็นเพียงการรับประกันบางส่วนเท่านั้น พื้นผิวจำนวนมหาศาลที่ระบบเชื่อมต่อด้วยอิงอยู่กับโค้ด unsafe ถ้าทำแค่การคำนวณล้วน ๆ ก็อีกเรื่อง แต่ถ้าสร้าง UI กราฟิกเป็นต้น ก็ยังมีสิ่งที่ผิดพลาดได้มากมาย
      ถึงอย่างนั้นก็ยังมีเส้นทางเดินหน้าที่ใช้งานได้จริง และมันจะนำไปสู่สถานการณ์ที่ดีกว่าสภาพทั่วไปของระบบที่เต็มไปด้วยช่องโหว่ในปัจจุบันมาก
      [1]: https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf
      [2]: https://plv.mpi-sws.org/rustbelt/stacked-borrows/
      [3]: https://www.ralfj.de/blog/2023/06/02/tree-borrows.html
      [4]: https://github.com/rust-lang/rust/issues?q=is%3Aissue+is%3Ao...
      [5]: https://github.com/Speykious/cve-rs
    • ผมไม่ใช่ผู้เชี่ยวชาญ Rust แต่ดูเหมือนในโค้ด core จะมี unsafe อยู่ค่อนข้างมาก ซึ่งก็สมเหตุสมผล
      https://github.com/search?q=repo%3Arust-lang%2Frust+unsafe+l...
      ผมไม่คิดว่า Coq ในแนวทางที่เสนอไว้นี้จะตรวจสอบการเรียก unsafe ทั้งหมดได้

  • แนวทางนี้ต่างจาก Aeneas หรือ RustHornBelt อย่างไรบ้าง? แล้วจัดการพอยน์เตอร์กับการยืมแบบแก้ไขได้อย่างไร?

    • ไม่รู้ว่า RustHornBelt ทำงานอย่างไร เราโฟกัสที่โค้ดที่ปลอดภัย แต่สำหรับบล็อก unsafe ก็ยังสร้างการแปลแบบ “พยายามให้ดีที่สุด” ด้วย
      เมื่อเทียบกับ Aeneas เป้าหมายคล้ายกันมาก เพราะทั้งสองพยายามตรวจพิสูจน์โปรแกรม Rust ด้วยตัวพิสูจน์ทฤษฎีบทแบบโต้ตอบได้ แต่ใน coq-of-rust เราจะเขียนโค้ดเวอร์ชันฟังก์ชันบริสุทธิ์ที่จะเป็นเป้าหมายของการพิสูจน์ด้วยมือ หรือถ้าเป็นงานซ้ำ ๆ ก็ใช้ความช่วยเหลือจาก GitHub Copilot แล้วพิสูจน์ว่าโค้ดนั้นสมมูลกับผลลัพธ์ที่แปลอัตโนมัติ ส่วน Aeneas ตั้งเป้าที่จะสร้างเวอร์ชันฟังก์ชันโดยตรง
      พอยน์เตอร์ทั้งหมดถูกจัดการเหมือนเป็นพอยน์เตอร์ที่แก้ไขได้ กล่าวคือเป็นชนิด * เราไม่ได้ใช้ข้อมูลจาก borrow checker ของ Rust ซึ่งทำให้การแปลง่ายขึ้น แต่ต้องไปจ่ายต้นทุนนี้ในขั้นตอนการพิสูจน์
      เพื่ออนุมานพอยน์เตอร์ในการพิสูจน์ เราให้ผู้ใช้จัดเตรียมตัวจัดสรรแบบกำหนดเองที่ออกแบบได้ตามวิธีที่หน่วยความจำจะถูกใช้งาน ตัวอย่างเช่น ถ้าโปรแกรมใช้ตัวแปรโกลบอลแบบแก้ไขได้สามตัว ก็อาจกำหนดหน่วยความจำเป็นเรคอร์ดที่มีสามรายการได้ รายการเหล่านี้ตอนแรกจะเป็น None เพื่อแทนสถานะที่ยังไม่ได้จัดสรร
      เรายังไม่รู้ว่าเทคนิคนี้จะขยายสเกลได้แค่ไหน แต่อย่างน้อยตอนนี้ก็หลีกเลี่ยงการให้เหตุผลด้วย separation logic ได้ เราคาดว่าโปรแกรมส่วนใหญ่ที่ต้องการตรวจพิสูจน์ โดยเฉพาะฝั่งแอปพลิเคชัน จะมีวินัยการใช้หน่วยความจำที่ค่อนข้าง “เรียบง่าย”

  • การเขียนสเปกสำหรับการตรวจพิสูจน์เชิงรูปแบบ คล้ายกับการใช้ property-based testing ที่ซับซ้อนขึ้นหรือไม่? พอเลยโปรแกรมที่ไม่ซับซ้อนไปแล้ว การเขียน property-based test ก็ค่อนข้างยากและใช้เวลามากเหมือนกัน

    • คล้ายกัน แต่ไม่เหมือนกันเสมอไป โดยทั่วไป property-based testing จะระบุคำอธิบายของอินพุตที่ระดับอินเทอร์เฟซของระบบ ระดับฟังก์ชันหรือโพรซีเยอร์ หรือระดับที่สูงกว่านั้น แล้วทดสอบว่าเอาต์พุตเป็นไปตามคุณสมบัติหนึ่งข้อหรือชุดคุณสมบัติใด ๆ หรือไม่
      เมื่อตรวจพิสูจน์เชิงรูปแบบในระดับเดียวกัน ก็อาจดูคล้ายกันมาก แต่เครื่องมือสำหรับการตรวจพิสูจน์เชิงรูปแบบสามารถลงลึกกว่าได้ เช่น ตอบคำถามเกี่ยวกับสถานะของระบบภายในระหว่างการคำนวณได้ว่า “มี loop invariant นี้อยู่ พิสูจน์ได้ไหมว่ามันคงอยู่จริงในทุกรอบ?” หรือ “พิสูจน์ได้ไหมว่าไม่มี underflow/overflow เกิดขึ้นเลยในการคำนวณขั้นกลางใด ๆ ระหว่างการคำนวณนี้?”
      กรณีแรกทำด้วย property-based testing ได้เช่นกัน หากแยกแกนของลูปออกมาเป็นโพรซีเยอร์ต่างหาก แล้วรันกับสถานะกลางจำนวนมากเพื่อทดสอบคุณสมบัติ invariant ส่วนกรณีหลังยากกว่ามาก เว้นแต่จะแตกโปรแกรมออกเป็นชิ้นเล็กมากจนแทบจะรันแยกได้ทีละบรรทัด

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

  • ใครช่วยอธิบายแนวคิด “การตรวจพิสูจน์” แบบง่ายมาก ๆ ได้ไหม? อยากรู้ว่าทำไมถึงต้องมีภาษาทั้งภาษาอย่าง Coq อยู่เพื่อจุดประสงค์นี้โดยเฉพาะ และมันมีความหมายเชิงปฏิบัติอย่างไรต่อสังคมในวงกว้าง