작은 신뢰 기반 구성
중요한 작업과 신뢰하지 않는 작업을 같은 시스템에서 분리해 실행하려면 커널의 경계 유지가 중요하다. seL4는 이런 격리 기반을 제공한다. 커널 위에서 실행되는 서비스와 응용 프로그램은 별도의 설계와 검증 대상이다.
증명이 보장하는 범위
형식 증명은 명세와 구현이 어떻게 연결되는지, 어떤 보안 성질이 유지되는지 다룬다. 하지만 지원하는 모든 플랫폼과 모든 설정이 동일한 증명을 갖는 것은 아니다. 사용할 아키텍처와 구성에 대응하는 증명 상태를 확인해야 한다.
남아 있는 가정
부트 코드와 어셈블리, 하드웨어 인터페이스, DMA 등 증명에서 가정하는 영역이 있다. 증명된 커널을 선택했다는 사실이 전체 장치와 응용 프로그램의 모든 결함을 제거하지는 않는다. 시스템을 평가할 때는 커널의 보장과 외부 가정을 분리한다.
관련 문서
CompCert / CakeML / HOL4 / Sail 명세 언어