ข่าว 
ข้อมูลเหรียญ 
แนะนำสื่อ 
มีการเปิดเผยแนวทางการออกแบบและพัฒนา 5 รูปแบบสำหรับใช้การตรวจสอบแบบเป็นทางการ เพื่อลดฐานคอมพิวติ้งที่เชื่อถือได้ (TCB) ของไคลเอนต์อีเธอเรียม(Ethereum)
จอร์จ คาเดียแนคิส(George Kadianakis) สมาชิกมูลนิธิอีเธอเรียม(Ethereum Foundation) และเคฟ เวดเดอร์เบิร์น(Kev Wedderburn) สมาชิกมูลนิธิอีเธอเรียม โพสต์บทความที่เกี่ยวข้องในฟอรัมวิจัยอีเธอเรียมเมื่อวันที่ 25 โดยอธิบายแนวทางลดขอบเขตสิ่งที่ต้องไว้วางใจในไคลเอนต์อีเธอเรียมผ่านการตรวจสอบแบบเป็นทางการ
TCB หมายถึงองค์ประกอบ ข้อกำหนด เครื่องมือ และสมมติฐานที่ต้องอาศัยความไว้วางใจ แทนที่จะผ่านการตรวจสอบทั้งหมด แม้การตรวจสอบแบบเป็นทางการจะไม่สามารถกำจัด TCB ได้ทั้งหมด แต่ช่วยลดขอบเขตที่มนุษย์ต้องไว้วางใจโดยตรงได้
นักวิจัยเสนอให้แบ่งไคลเอนต์เชิงนามธรรมออกเป็นหลายโมดูล จากนั้นตรวจสอบบทบาทและขอบเขตการรับประกันของแต่ละโมดูลแยกกัน หากเชื่อมการรับประกันของแต่ละโมดูลผ่านอินเทอร์เฟซ ก็จะสามารถตรวจสอบคุณสมบัติด้านความปลอดภัยของไคลเอนต์ทั้งระบบได้
ประเด็นสำคัญคือการแยก ‘โมดูลบริสุทธิ์’ ออกจาก ‘โมดูลไม่บริสุทธิ์’ โดยส่วนที่มีผลข้างเคียงน้อยและมีโครงสร้างทางคณิตศาสตร์ชัดเจน เช่น การเข้ารหัส SSZ และกฎการเลือกฟอร์ก ถูกจัดเป็นโมดูลบริสุทธิ์ที่เหมาะกับการตรวจสอบแบบเป็นทางการ ส่วนเครือข่ายซึ่งมีอินพุต เอาต์พุต และสถานะภายนอกจำนวนมาก รวมถึงต้องพิจารณาลำดับข้อความ การขาดการเชื่อมต่อ และความล่าช้า ถูกจัดเป็นโมดูลไม่บริสุทธิ์
นักวิจัยเสนอให้ออกแบบโมดูลไม่บริสุทธิ์โดยไม่ถือว่าเชื่อถือได้ตั้งแต่ต้น ตัวอย่างเช่น แทนที่จะเชื่อถือลายเซ็นที่โมดูลเครือข่ายส่งต่อมาโดยตรง ควรนำไปประมวลผลซ้ำผ่านโมดูลตรวจสอบลายเซ็นบริสุทธิ์ วิธีนี้ทำให้บั๊กในโมดูลเครือข่ายถูกจัดการในลักษณะเดียวกับอินพุตภายนอกที่เป็นอันตราย
ในระยะยาว ยังมีการเสนอให้ย้ายขอบเขตการตรวจสอบเข้าใกล้เครือข่ายมากขึ้น แทนที่จะสร้างแบบจำลองเครือข่ายทั้งหมด ควรเริ่มจากการตรวจสอบพาร์เซอร์ กฎกอสซิป และตรรกะการซิงก์ เพื่อป้องกันไม่ให้ข้อความที่ไม่ถูกต้องทำให้ระบบหยุดทำงานหรือใช้ทรัพยากรมากเกินไป
บทความยังระบุว่าการเชื่อมโยงระหว่างข้อกำหนดกับไฟล์โปรแกรมที่นำไปใช้งานจริงเป็นอีกโจทย์หนึ่ง นักวิจัยแยกการเขียนข้อกำหนดแบบเป็นทางการและพิสูจน์คุณสมบัติด้วย Lean4 ออกจากการพิสูจน์ว่าโค้ดที่นำไปใช้งานจริงเป็นไปตามข้อกำหนดดังกล่าว เนื่องจากผู้ใช้ให้ความสำคัญกับความปลอดภัยของโค้ดที่ทำงานบนคอมพิวเตอร์ของตนเอง จึงจำเป็นต้องดำเนินการตรวจสอบทั้งสองขั้นตอน
เส้นทางการพัฒนาที่เสนอประกอบด้วย △การแปลงโค้ดที่เขียนด้วย Rust และภาษาอื่นเป็น Lean4 โดยอัตโนมัติ △การดึงโมดูลที่เขียนด้วย Lean4 ออกมาเป็นโค้ด C △การเขียนไคลเอนต์ทั้งหมดด้วย Lean4 และเชื่อมเฉพาะโมดูลที่มีผลข้างเคียงสูงเข้ากับภาษาอื่น △การเขียนโมดูลสำคัญโดยตรงด้วยแอสเซมบลี RISC-V และ △การใช้คอมไพเลอร์ที่ผ่านการตรวจสอบแล้ว
หากแปลงโค้ด Rust เป็น Lean4 ตัวแปลงและคอมไพเลอร์ Rust ที่ใช้สร้างไบนารีสุดท้ายจะยังคงอยู่ใน TCB หากดึงโค้ด Lean4 ออกมาเป็น C หรือเขียนไคลเอนต์ส่วนใหญ่ด้วย Lean4 ตัวดึงโค้ด คอมไพเลอร์ C และอินเทอร์เฟซฟังก์ชันภายนอกจะเป็นสิ่งที่ต้องไว้วางใจ
การเขียนโมดูลสำคัญด้วยแอสเซมบลี RISC-V ช่วยนำคอมไพเลอร์ทั่วไปออกจาก TCB ได้ แต่แบบจำลองคำสั่ง RISC-V ที่เป็นทางการและเครื่องมือแปลงแอสเซมบลีเป็นโค้ดสำหรับโปรเซสเซอร์ประเภทอื่นจะกลายเป็นสิ่งที่ต้องไว้วางใจเพิ่มเติม ส่วนการใช้คอมไพเลอร์ที่ผ่านการตรวจสอบแล้วจะช่วยนำตัวดึงโค้ดและคอมไพเลอร์ C ออกจาก TCB ได้
นักวิจัยมองว่าไม่จำเป็นต้องใช้วิธีเดียวกันกับทุกโมดูล โมดูลที่มีโครงสร้างทางคณิตศาสตร์ชัดเจนอาจตรวจสอบด้วย Lean4 ขณะที่โมดูลที่มีโครงสร้างข้อมูลซับซ้อนหรือมีขนาดใหญ่สามารถใช้ตัวแปลงหรือคอมไพเลอร์ที่ผ่านการตรวจสอบแล้ว ทำให้เกิดแนวทางแบบผสมได้
บทความนี้ไม่ได้ประกาศว่าไคลเอนต์อีเธอเรียมทั้งระบบผ่านการตรวจสอบแบบเป็นทางการแล้ว แต่เป็นการเสนอแนวทางการออกแบบว่าควรแบ่งการตรวจสอบข้อกำหนดแบบเป็นทางการ การนำไปใช้งานจริง และกระบวนการคอมไพล์ออกเป็นหน่วยใด รวมถึงควรขยายขอบเขตการตรวจสอบไปถึงระดับใด
ความคิดเห็น 0