สำหรับ Linux มีการเสนอกลไกเพื่อตรวจสอบการทำงานที่ถูกต้องของเคอร์เนล

สำหรับการรวมไว้ในเคอร์เนล Linux 5.20 (บางทีสาขาอาจมีหมายเลข 6.0) มีการเสนอชุดแพตช์พร้อมกับการใช้กลไก RV (Runtime Verification) ซึ่งมีเครื่องมือสำหรับตรวจสอบการทำงานที่ถูกต้องบนระบบที่เชื่อถือได้สูงซึ่งรับประกัน ไม่มีความล้มเหลว การตรวจสอบจะดำเนินการในขณะรันไทม์โดยการแนบตัวจัดการเพื่อติดตามจุดที่ตรวจสอบความคืบหน้าที่แท้จริงของการดำเนินการกับแบบจำลองที่กำหนดการอ้างอิงที่กำหนดไว้ล่วงหน้าของหุ่นยนต์ที่กำหนดพฤติกรรมที่คาดหวังของระบบ

ข้อมูลจากจุดติดตามจะย้ายโมเดลจากสถานะหนึ่งไปยังอีกสถานะหนึ่ง และหากสถานะใหม่ไม่ตรงกับพารามิเตอร์ของโมเดล จะมีการสร้างคำเตือนหรือเคอร์เนลอยู่ในสถานะ "ตื่นตระหนก" (คาดว่าระบบที่มีความน่าเชื่อถือสูงจะตรวจจับได้) และตอบสนองต่อสถานการณ์ดังกล่าว) โมเดลหุ่นยนต์ซึ่งกำหนดการเปลี่ยนจากสถานะหนึ่งไปอีกสถานะหนึ่งจะถูกส่งออกเป็นรูปแบบ "จุด" (graphviz) หลังจากนั้นจะถูกแปลโดยใช้ยูทิลิตี้ dot2c เป็นการเป็นตัวแทน C ซึ่งโหลดในรูปแบบของโมดูลเคอร์เนลที่ ติดตามความเบี่ยงเบนของความคืบหน้าในการดำเนินการจากแบบจำลองที่กำหนดไว้ล่วงหน้า

สำหรับ Linux มีการเสนอกลไกเพื่อตรวจสอบการทำงานที่ถูกต้องของเคอร์เนล

การตรวจสอบแบบจำลองรันไทม์อยู่ในตำแหน่งที่มีน้ำหนักเบากว่าและง่ายต่อการนำไปใช้ในการตรวจสอบการดำเนินการที่ถูกต้องบนระบบที่มีความสำคัญต่อภารกิจ เสริมวิธีการตรวจสอบความน่าเชื่อถือแบบคลาสสิก เช่น การตรวจสอบแบบจำลองและการพิสูจน์ทางคณิตศาสตร์ของการปฏิบัติตามโค้ดตามข้อกำหนดที่กำหนดอย่างเป็นทางการ ภาษา. ข้อดีของ RV คือความสามารถในการให้การตรวจสอบที่เข้มงวดโดยไม่ต้องแยกการใช้งานระบบทั้งหมดในภาษาการสร้างแบบจำลอง เช่นเดียวกับการตอบสนองที่ยืดหยุ่นต่อเหตุการณ์ที่ไม่คาดฝัน เช่น เพื่อป้องกันการแพร่กระจายของความล้มเหลวในระบบที่สำคัญ

ที่มา: opennet.ru

เพิ่มความคิดเห็น