Могут ли приложения, работающие в ring0, быть безопасными без формальной проверки?

Вопрос немного сбивает с толку, но я постараюсь ответить на него.

Выполнение любого ненадежного кода в привилегированном режиме вряд ли будет" безопасным " в том смысле, в каком его понимает большинство людей. Однако, как вы правильно предполагаете, можно использовать что-то похожее на виртуальную машину, чтобы умерить действия, которые ненадежный процесс может предпринять в этой среде. Это принцип, по которому работают современные "гипервизоры" - доступ к аппаратному обеспечению (или памяти) осуществляется через интернет. модерируется какой-то частью программного или аппаратного обеспечения "монитора".

Тем не менее, если вы используете такой подход, то, скорее всего, формальная проверка виртуальной машины очень желательна. В противном случае кажется возможным, что вредоносная программа может найти способ сбежать из виртуальной машины или заставить виртуальную машину вести себя нежелательным образом.

Разумным современным подходом к этой проблеме является использование кода, несущего доказательство, в котором часть ненадежный код несет с собой проверяемое машиной доказательство того, что он ведет себя в соответствии с некоторой политикой безопасности. Все, что нужно сделать хост-операционной системе на этом этапе, - это проверить доказательство против кода (достаточно дешевая с точки зрения вычислений операция), а затем безопасно запустить этот код без необходимости его виртуализации или какой-либо проверки во время выполнения.