흥미로운 프로젝트임. 최악 실행 시간(WCET) 의 형식적 검증 한계가 궁금함
seL4, atmosphere 같은 다른 검증된 커널도 있고, genode처럼 POSIX 호환 계층을 쌓을 수도 있음
QNX나 VxWorks처럼 완전 호환되고 성숙한 커널도 있어서, 완전한 검증이 큰 가치 추가가 아닐 수도 있음
하지만 WCET + 형식 검증 + POSIX 호환성을 모두 갖춘 사례는 거의 못 봤음
현재 단계에서는 문서에 나오는 실시간 용도에 바로 쓸 수 있을 정도로 성숙도가 높다고 보긴 어려움
어떤 정부든 OS에 RCE를 얻을 수 있는 세상임. 그래서 프로세스 격리의 형식 검증이 정말 중요함
seL4는 Linux보다 훨씬 빠르지만, 이건 느릴 것 같음. POSIX는 본질적으로 결함이 있고, MAC은 너무 복잡해서 실무에서 쓰기 어려움
아직 stone 수준이지만, 앞으로 공식 인증도 받을 수 있을 것 같음. 형식적으로 검증된 OS는 보안 향상에 큰 진전임
Ada는 Wirth 계열 언어(Pascal 계열)에 속함. 지금까지 Wirth 계열 언어로 된 Unix 유사 커널은 TUNIS밖에 몰랐음
TUNIS는 Concurrent Euclid로 구현되었음
90년대 워싱턴대에서 개발된 SPIN도 있었음. Modula-3로 작성된 마이크로커널 기반 시스템으로, Digital UNIX 시스템 호출 인터페이스를 지원했음
또 80년대 INRIA의 Sol은 Pascal 방언으로 구현되어 Unix 호환 환경을 제공했고, 이후 Chorus로 이어졌음
Ironclad라는 이름의 NDA 관련 회사도 있음. 상표권 문제를 조심해야 함
그래도 이런 시도는 정말 반가움. 하지만 현실에서는 보안의 가장 약한 고리가 펌웨어 계층임
내 꿈은 Framework 컴퓨터 같은 하드웨어가 검증된 EFI 펌웨어와 구성요소별로 감사된 펌웨어를 갖추는 것임
Ironclad는 Common Lisp의 주요 암호화 라이브러리 이름이기도 함 (ironclad GitHub)
MNT Research도 살펴볼 만함. 수리 가능한 노트북을 만들고, 하드웨어와 소프트웨어를 모두 오픈소스로 공개함 (mnt.re)
펌웨어 검증에는 별도의 커널이 필요함. 이제는 이런 부분이 규제 수준으로 관리되어야 함
상표는 같은 이름이라도 다른 산업 분야면 문제 없음. 예를 들어 Apple Computer와 Beatles의 Apple Music 사례처럼 (xkcd 386)
새로운 OS를 만든다는 건 정말 야심찬 일임. 최근에 Radiant Computer도 올라왔는데, 비슷한 흥미로운 프로젝트가 또 있을까 궁금함
Hacker News 의견
흥미로운 프로젝트임. 최악 실행 시간(WCET) 의 형식적 검증 한계가 궁금함
seL4, atmosphere 같은 다른 검증된 커널도 있고, genode처럼 POSIX 호환 계층을 쌓을 수도 있음
QNX나 VxWorks처럼 완전 호환되고 성숙한 커널도 있어서, 완전한 검증이 큰 가치 추가가 아닐 수도 있음
하지만 WCET + 형식 검증 + POSIX 호환성을 모두 갖춘 사례는 거의 못 봤음
현재 단계에서는 문서에 나오는 실시간 용도에 바로 쓸 수 있을 정도로 성숙도가 높다고 보긴 어려움
seL4는 Linux보다 훨씬 빠르지만, 이건 느릴 것 같음. POSIX는 본질적으로 결함이 있고, MAC은 너무 복잡해서 실무에서 쓰기 어려움
Ada는 Wirth 계열 언어(Pascal 계열)에 속함. 지금까지 Wirth 계열 언어로 된 Unix 유사 커널은 TUNIS밖에 몰랐음
TUNIS는 Concurrent Euclid로 구현되었음
또 80년대 INRIA의 Sol은 Pascal 방언으로 구현되어 Unix 호환 환경을 제공했고, 이후 Chorus로 이어졌음
Ironclad라는 이름의 NDA 관련 회사도 있음. 상표권 문제를 조심해야 함
그래도 이런 시도는 정말 반가움. 하지만 현실에서는 보안의 가장 약한 고리가 펌웨어 계층임
내 꿈은 Framework 컴퓨터 같은 하드웨어가 검증된 EFI 펌웨어와 구성요소별로 감사된 펌웨어를 갖추는 것임
새로운 OS를 만든다는 건 정말 야심찬 일임. 최근에 Radiant Computer도 올라왔는데, 비슷한 흥미로운 프로젝트가 또 있을까 궁금함
완전히 형식 검증된 커널이 언젠가 대중화되길 바람
Linux 전체를 검증하는 건 불가능하겠지만, seL4는 스마트폰 같은 시장에서 기회를 잡을 수도 있을 것 같음
그들의 검증 로드맵을 보면, “형식 검증”이라 부르기엔 과함
핵심적인 커널 속성에 대한 증명이 없고, seL4나 Tock 같은 커널의 수준에는 미치지 못함
CuBit은 SPARK/Ada로 작성된 또 다른 OS임
소스는 GitHub에서 볼 수 있음
일반 사용자 입장에서는 커널만으로는 쓸모가 없음
Ironclad 커널을 사용하는 OS 예시는 Gloire임
MAC 관련 문서가 잘 정리되어 있음 (Mandatory Access Control)
SPARK의 “가격 문의” 문구를 보면, 이건 ‘자유 소프트웨어’ 라기보단 다른 의미의 ‘free’ 같음