seL4, AArch64에서 기밀성 증명까지 완료해 보안 격리 증명 마침

seL4를 실제로 쓰는 운영체제가 궁금함. GenodeOS, LionsOS, 중국 자동차 업체의 차량 하이퍼바이저 사례 말고 비공개 배포 사례가 더 있는지 알고 싶음.

iOS Secure Enclave의 sepOS는 초기 UNSW/NICTA L4 나노커널 계열 포크임. 애플도 언젠가 하드웨어 보안 기능을 붙인 seL4 파생형으로 갈 가능성이 있다고 보지만, 지금은 Kry10 KOS 같은 사례를 보는 편이 나음.

타이밍이나 물리 접근 같은 공격은 보통 이런 연구에서 범위 밖으로 두는지 궁금함. 이 증명이 그런 공격을 어떻게 다루는지 잘 모르겠음.

증명이 유효하다는 전제라면 seL4의 보안을 깨는 부채널 공격은 다른 어떤 OS의 보장도 같이 깨는 셈이라, 그 비판은 좀 불공정하다고 봄.

타이밍 채널을 막는 time protection 연구도 진행 중이고, seL4가 시간 보호를 제공한다는 증명도 있음.

L4 커널은 스케줄링, IPC, capability 정도만 처리해서 커널 자체를 상대로 한 부채널 공격의 실익은 작을 듯함. 다만 파일시스템 같은 민감한 기능을 사용자 공간으로 옮긴다고 그 프로세스의 보안 문제가 사라지는 건 아님.

가정 문서에 부채널 범위가 명시돼 있음. 기밀성 증명은 하드웨어 이진 모델에 나타난 채널만 다루며, 커널 내부 저장소 채널은 다루지만 타이밍 채널은 다루지 않음. 증명이 무효라는 뜻은 아니지만 비밀이 절대 안 샌다는 결론도 아님.

Rowhammer류 공격도 별도 문제임.

타이밍 부채널은 마이크로아키텍처 수준이고, seL4 보안 증명은 아키텍처 수준을 대상으로 함.

문서의 작은 글씨를 봐야 함. 범위는 non-MCS, unicore임.

임베디드와 군수 시장은 계속 자금을 댈 수 있겠지만, capability 모델이 시스템 보안을 높인다고 하려면 native seL4/Linux가 필요하다고 봄. 보안 부트 기반 가상화 플랫폼은 이제 흔함.

seL4는 이미 Linux VM을 호스팅할 수 있고, 하드웨어 가상화 없이 Linux 코드나 바이너리를 실행하는 방법도 있음.

현재 가치는 기존의 특수 목적 장비가 물리적으로 분리한 칩들을 하나로 합치면서도 검증 가능한 격리 요건을 충족한다고 말할 수 있다는 데 있음. 보안 향상보다는 비용, 전력, 공간 절감 논리임.

'seL4/Linux'를 GNU/Linux처럼 쓴 거라면 GNU/seL4가 맞을 듯함. Linux 커널과 seL4 커널을 섞는 방법은 한쪽이 다른 쪽을 VM으로 돌리는 것뿐임.