Verve (операционная система)
| Разработчик | Microsoft Исследования |
|---|---|
| Написано в | БугиПЛ, C# ; загрузчик на языке ассемблера , C++ ; может использовать другие общие промежуточные языки (CIL) |
| Семейство ОС | Языковые операционные системы |
| Рабочее состояние | В разработке |
| Исходная модель | Доступен исходный код (через Инициативу общего источника ) |
| Первоначальный выпуск | сентябрь 2010 г |
| Последний выпуск | r73999 / 10 ноября 2013 г |
| Платформы | х86 |
| ядра Тип | Микроядро , основанное на языке |
| Лицензия | Лицензия Microsoft на исследования |
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 с помощью (решателя) теорем Z3 теоремы выполнимости по модулю теорий (SMT) автоматического средства доказательства . Nucleus полагается на ядро для реализации потоков, планирования, синхронизации и предоставления большинства обработчиков прерываний. Несмотря на то, что ядро формально не проверено, например, ошибка в планировании может привести к зависанию системы, оно не может нарушать безопасность типа или памяти и, следовательно, не может напрямую вызывать неопределенное поведение. Если он попытается отправить недействительные запросы к Ядру, формальная проверка гарантирует, что Ядро обработает ситуацию контролируемым образом .
Verve Доверенная вычислительная база (TCB) ограничена: Boogie/Z3 для проверки правильности Nucleus; BoogieASM для перевода на х86-сборку; спецификация BoogiePL о том, как должен вести себя Nucleus; верификатор ТАЛ; ассемблер и компоновщик; и загрузчик. Примечательно, что ни компилятор/среда выполнения C#, ни компилятор Bartok не являются частью TCB.
Ссылки
[ редактировать ]- Безопасно до последней инструкции: автоматическая проверка типобезопасной операционной системы , Джин Янг и Крис Хоблицель. Проектирование и реализация языков программирования , 2010.
- Безопасно до последней инструкции: автоматическая проверка типобезопасной операционной системы , Джин Янг и Крис Хоблицель. Основные моменты исследования CACM. Сообщения ACM , сентябрь 2010 г.
- Техническая перспектива: безопасность превыше всего!
- Verve: Типобезопасная операционная система . Интервью с Крисом Хоблицелем.
- Verve: Типобезопасная операционная система . ОСньюс .
- Анонс Verve — типобезопасная операционная система . ИнфоQ .
Операционные системы Microsoft |
|---|
