ล่าสุดมีข่าวออกมาว่า ได้จัดทำข้อเสนอให้รวมอยู่ใน เคอร์เนลของ Linux 5.20 (หรือบางทีสาขาจะมีหมายเลข 6.0 ทั้งหมดขึ้นอยู่กับการตัดสินใจของ Linus Torvalds เนื่องจากความคิดเห็นของเขาเกี่ยวกับการเปิดตัว Kernel 5.19)
ข้อเสนอที่ทำเป็นเรื่องเกี่ยวกับ ชุดของแพตช์พร้อมการนำกลไก RV ไปใช้ (Runtime Verification) ซึ่งเป็นวิธีการตรวจสอบการทำงานที่ถูกต้องในระบบที่มีความน่าเชื่อถือสูงซึ่งรับประกันว่าไม่มีข้อผิดพลาด
การตรวจสอบความถูกต้อง ทำที่รันไทม์โดยแนบตัวจัดการเข้ากับจุดติดตาม ที่ตรวจสอบความคืบหน้าที่แท้จริงของการดำเนินการกับแบบจำลองอ้างอิงที่กำหนดไว้ล่วงหน้าของหุ่นยนต์ที่กำหนดพฤติกรรมที่คาดหวังของระบบ
ผู้พัฒนาลินุกซ์, Daniel Bristot de Oliveira กล่าวว่า:
ในช่วงไม่กี่ปีที่ผ่านมา ฉันได้สำรวจความเป็นไปได้ในการตรวจสอบพฤติกรรมของเคอร์เนล Linux โดยใช้การตรวจสอบรันไทม์
การตรวจสอบรันไทม์ (RV) เป็นวิธีการแบบเบา (แต่เข้มงวด) ที่เสริมเทคนิคการตรวจสอบอย่างละเอียดแบบคลาสสิก (เช่น การตรวจสอบแบบจำลองและการพิสูจน์ทฤษฎีบท) ด้วยวิธีการลงมือปฏิบัติจริงกับระบบที่ซับซ้อน แทนที่จะอาศัยแบบจำลองโดยละเอียดของระบบ (เช่น การนำระดับคำสั่งมาใช้ใหม่) VR ทำงานโดยการวิเคราะห์การติดตามการดำเนินการจริงของระบบ เปรียบเทียบกับข้อกำหนดอย่างเป็นทางการของพฤติกรรมของระบบ
การใช้ออโตมาตาที่กำหนดขึ้นเองสำหรับ VR เป็นแนวทางที่มั่นคง สำหรับกรณีเฉพาะของเคอร์เนล Linux คุณสามารถเรียนรู้วิธีจำลองพฤติกรรมที่ซับซ้อนของเคอร์เนล Linux ได้จากบทความนี้:
เดอ โอลิเวรา, แดเนียล บริสตอต; Cucinotta, ทอมมาโซ; เด โอลิเวร่า, โรมูโล่ ซิลวา. *การตรวจสอบอย่างเป็นทางการอย่างมีประสิทธิภาพสำหรับเคอร์เนล Linux* ใน: การประชุมระหว่างประเทศเกี่ยวกับวิศวกรรมซอฟต์แวร์และวิธีการที่เป็นทางการ สปริงเกอร์ จาม 2019. p. 315-332.
และวิธีนี้มีประสิทธิภาพเพียงใดที่นี่:
เดอ โอลิเวรา, แดเนียล บี.; De Oliveira, Romulo S.; คูชินอตตา, ทอมมาโซ. *โมเดลการซิงโครไนซ์เธรดสำหรับเคอร์เนล PREEMPT_RT Linux* Journal of Systems Architecture, 2020, 107: 101729
TLDR: พฤติกรรมที่ซับซ้อนสามารถสร้างแบบจำลองในแบบโมดูลาร์ โดยมีค่าโสหุ้ยที่ยอมรับได้ (แม้กระทั่งสำหรับระบบการผลิต)
เป็นที่กล่าวขวัญกันว่า ข้อมูลจุดติดตามจะย้ายโมเดลจากสถานะหนึ่งไปยังอีกสถานะหนึ่งและหากสถานะใหม่ไม่ตรงกับพารามิเตอร์โมเดล คำเตือนจะถูกสร้างขึ้นหรือเคอร์เนลเข้าสู่สถานะ "ตื่นตระหนก" (สมมติว่าระบบที่มีความน่าเชื่อถือสูงจะตรวจจับและตอบสนองต่อสถานการณ์ดังกล่าว)
โมเดลหุ่นยนต์ กำหนดการเปลี่ยนจากสถานะหนึ่งไปอีกสถานะหนึ่งจะถูกส่งออกไปยังรูปแบบ "จุด" (graphviz) หลังจากนั้นจะแปลโดยใช้ยูทิลิตี้ dot2c เป็นตัวแทน C ซึ่งโหลดในรูปแบบของโมดูลเคอร์เนลที่ติดตามการเบี่ยงเบน การดำเนินการจากแบบจำลองที่กำหนดไว้ล่วงหน้า
การตรวจสอบรุ่นขณะใช้งานจริงอยู่ในตำแหน่งเป็นวิธีที่เบากว่าและง่ายกว่า เพื่อนำไปใช้ในการตรวจสอบความถูกต้องของการดำเนินการในระบบที่มีความสำคัญต่อภารกิจ ซึ่งช่วยเสริมวิธีการตรวจสอบความน่าเชื่อถือแบบคลาสสิก เช่น การตรวจสอบแบบจำลองและการพิสูจน์ทางคณิตศาสตร์ของการปฏิบัติตามรหัสด้วยข้อกำหนดที่กำหนดในภาษาที่เป็นทางการ
ผู้ดูแลระบบย่อยการติดตาม Steven Rostedt สรุปได้ดังนี้:
» นี่คือการเปลี่ยนแปลงครั้งใหญ่ที่สุดสำหรับคำขอดึงนี้ แนะนำการตรวจสอบรันไทม์ที่จำเป็นสำหรับการรัน Linux บนระบบที่มีความสำคัญต่อความปลอดภัย อนุญาตให้แทรกโมเดลออโตมาตาที่กำหนดขึ้นในเคอร์เนลเพื่อแนบกับจุดติดตาม โดยที่ข้อมูลเกี่ยวกับจุดติดตามเหล่านี้จะย้ายโมเดลจากสถานะหนึ่งไปยังอีกสถานะหนึ่ง
ข้อดีที่กล่าวถึงของ RV คือความสามารถในการให้การตรวจสอบอย่างเข้มงวดโดยไม่ต้องมีการใช้งานทั้งระบบในภาษาการสร้างแบบจำลองแยกจากกัน รวมถึงการตอบสนองต่อเหตุการณ์ที่ไม่คาดฝันได้อย่างยืดหยุ่น เช่น เพื่อป้องกันการแพร่กระจายของความล้มเหลวของระบบที่สำคัญ
สุดท้ายนี้ หากสนใจอยากทราบข้อมูลเพิ่มเติม สามารถเข้าไปดูรายละเอียดใน ลิงค์ต่อไปนี้
Fuente: https://www.phoronix.com/