Verve — исследовательская операционная система , разработанная Microsoft Research . Verve проверена на сквозную безопасность типов и безопасность памяти .
Из-за своей сложности святым Граалем верификации программного обеспечения стала проверка свойств операционных систем. Операционные системы обычно пишутся на низкоуровневых языках, таких как C , которые предоставляют очень мало гарантий. Проект Singularity взял на вооружение подход написания операционной системы на C# , типобезопасном, безопасном для памяти языке. Слабость этого подхода заключается в том, что операционным системам обязательно нужно вызывать низкоуровневый код, например, для перемещения указателя стека. Verve решает эту проблему, разделяя операционную систему на проверенный язык ассемблера , который должен быть низкоуровневым, и доверенный интерфейс для остальной части операционной системы, написанный на C#. Существует доверенная спецификация, которая гарантирует, что низкоуровневый код ассемблера не изменяет кучу, а высокоуровневый код C# не изменяет стеки.
Verve состоит из небольшого Nucleus , который действует как минимальный уровень абстракции оборудования, и Kernel , который использует примитивы, предоставляемые Nucleus, чтобы предоставить более традиционный интерфейс приложениям. Все компоненты системы, кроме Nucleus, написаны на управляемом коде C# и скомпилированы Bartok (первоначально разработанном для проекта Singularity ) в типизированный язык ассемблера (TAL), который проверяется проверяющим средством TAL.
Nucleus реализует распределитель памяти и сборщик мусора, поддержку переключения стека и управление обработчиками прерываний. Он написан на BoogiePL, который служит входными данными для верификатора Boogie от MSR , который доказывает правильность Nucleus с помощью автоматизированного доказчика теорем (решателя) выполнимости по модулю теорий (SMT) теоремы Z3 . Nucleus полагается на Kernel для реализации потоков, планирования, синхронизации и предоставления большинства обработчиков прерываний. Несмотря на то, что Kernel формально не проверен, так что, например, ошибка в планировании может привести к зависанию системы, он не может нарушить безопасность типов или памяти и, таким образом, не может напрямую вызвать неопределенное поведение. Если он пытается сделать недействительные запросы к Nucleus, формальная проверка гарантирует, что Nucleus обрабатывает ситуацию контролируемым образом .
Доверенная вычислительная база Verve (TCB) ограничена: Boogie/Z3 для проверки корректности Nucleus; BoogieASM для перевода его в сборку x86; спецификация BoogiePL того, как должен вести себя Nucleus; верификатор TAL; ассемблер и компоновщик; и загрузчик. Примечательно, что ни компилятор/среда выполнения C#, ни компилятор Bartok не являются частью TCB.