Linux의 경우 커널의 정확성을 검증하는 메커니즘이 제안됩니다.

Linux 커널 5.20(아마도 분기 번호는 6.0이 될 것임)에 포함하기 위해 RV(런타임 검증) 메커니즘을 구현한 패치 세트가 제안되었습니다. 이 메커니즘은 신뢰성이 높은 시스템에서 올바른 작동을 확인하는 도구를 제공합니다. 실패가 없습니다. 확인은 시스템의 예상 동작을 정의하는 자동 장치의 사전 결정된 참조 결정론적 모델에 대해 실제 실행 진행 상황을 확인하는 추적 지점에 핸들러를 연결하여 런타임에 수행됩니다.

추적점의 정보는 모델을 한 상태에서 다른 상태로 이동시키며, 새 상태가 모델의 매개변수와 일치하지 않으면 경고가 생성되거나 커널이 "패닉" 상태에 놓이게 됩니다(신뢰도가 높은 시스템에서는 이를 감지할 것으로 예상됨). 그러한 상황에 대응합니다). 한 상태에서 다른 상태로의 전환을 정의하는 자동화 모델은 "점" 형식(graphviz)으로 내보낸 후 dot2c 유틸리티를 사용하여 C 표현으로 변환됩니다. 이는 커널 모듈 형태로 로드됩니다. 사전 정의된 모델과의 실행 진행률 편차를 추적합니다.

런타임 모델 검사는 미션 크리티컬 시스템에서 올바른 실행을 확인하는 더 가볍고 구현하기 쉬운 방법으로 자리잡고 있으며, 모델 검사 및 공식 문서에 제공된 사양에 대한 코드 준수에 대한 수학적 증명과 같은 기존 신뢰성 확인 방법을 보완합니다. 언어. RV의 장점 중에는 모델링 언어로 전체 시스템을 별도로 구현하지 않고도 엄격한 검증을 제공할 수 있는 능력과 예상치 못한 이벤트에 유연하게 대응할 수 있는 능력(예: 중요한 시스템의 장애가 추가로 전파되는 것을 차단하는 능력)이 있습니다.

출처 : opennet.ru