버브(운영 체제)

Verve는 마이크로소프트 리서치가 개발한 연구 운영체제다.Verve는 형식 안전 및 메모리 안전성에 대해 엔드투엔드로 검증되었다.

그 복잡성 때문에 소프트웨어 검증의 성스러운 문제는 운영체제의 속성을 검증하는 것이었다.운영체제는 보통 C와 같이 극히 적은 보증을 제공하는 낮은 수준의 언어로 쓰여진다.특이점 프로젝트는 타입-세이프-메모리-세이프 언어인 C#로 운영체제를 작성하는 접근방식을 취하였다.이 접근방식의 약점은 예를 들어 스택 포인터를 이동하려면 운영 체제가 반드시 하위 레벨 코드를 호출해야 한다는 것이다.Verve는 C#에 명시된 낮은 레벨의 운영 체제와 나머지 운영 체제에 대한 신뢰할 수 있는 인터페이스가 필요한 검증된 어셈블리 언어로 운영 체제를 분할하여 이 문제를 해결한다.낮은 레벨의 조립 코드가 힙을 수정하지 않고, 높은 레벨의 C# 코드가 스택을 수정하지 않는다는 것을 보장하는 신뢰할 수 있는 규격이 있다.

Verve는 최소 하드웨어 추상화 계층의 역할을 하는 작은 핵(Nuclear)과 핵(Nuclear)이 제공하는 원시 물질을 사용하여 보다 전통적인 인터페이스를 애플리케이션에 노출시키는 커널(Kernel)로 구성되어 있다.핵 이외의 시스템의 모든 구성요소는 관리 코드 C#로 작성되고 바르토크(원래 특이성 프로젝트를 위해 개발됨)가 TAL로 컴파일하여 TAL 검사기로 검증한다.

핵은 메모리 할당자와 가비지 수집, 스택 전환 지원, 인터럽트 핸들러 관리를 구현한다.MSR의 Boogie verifier에 대한 입력 역할을 하는 BoogiePL에 기재되어 있으며, 이는 Z3 Orgin Prober 만족도 모듈로 이론(SMT) 자동 정리 perver(솔버)를 이용하여 핵이 정확함을 증명한다.핵은 스레드, 스케줄링, 동기화를 구현하고 대부분의 인터럽트 핸들러를 제공하기 위해 커널에 의존한다.커널이 정식으로 검증되지 않았음에도 불구하고, 예를 들어 스케줄링 버그로 인해 시스템이 중단될 수 있고, 유형이나 메모리 안전을 침해할 수 없으며, 따라서 정의되지 않은 행동을 직접적으로 야기할 수 없다.만약 핵에 대해 유효하지 않은 요청을 하려고 한다면, 공식적인 검증은 핵이 상황을 통제된 방식으로 다루도록 보장한다.

Verve의 신뢰할 수 있는 컴퓨팅 기반(TCB)은 다음과 같이 제한된다: 핵의 정확성 확인을 위한 Boogie/Z3; Boogie이를 x86 어셈블리로 변환하기 위한 ASM; Boogie핵이 어떻게 동작해야 하는지에 대한 PL 규격, TAL 검증기, 조립기 및 링커, 부트로더.특히, C# 컴파일러/런타임이나 Bartok 컴파일러는 TCB에 속하지 않는다.

참조

• 마지막 지침까지 안전: Jean Yang과 Chris Hawblizel의 Type-Safe 운영 체제의 자동 검증.프로그래밍 언어 설계 및 구현, 2010.
• 마지막 지침까지 안전: Jean Yang과 Chris Hawblizel의 Type-Safe 운영 체제의 자동 검증.CACM Research 하이라이트.ACM의 통신, 2010년 9월.
• 기술적 관점: 안전 우선!
• Verve: 유형 안전 운영 체제.Chris Hawblizel과의 인터뷰.
• Verve: 유형 안전 운영 체제.OS뉴스.
• Verve – Type-Safe 운영 체제 발표InfoQ.