▲

Ironclad – 실시간 대응 유닉스 계열 OS 커널

 (ironclad-os.org)
1P by GN⁺ 1일전 | ★ favorite | 댓글 1개
  • 아이언클래드(Ironclad) 는 일반용 및 임베디드 환경을 위한 형식 검증 기반 실시간 대응 유닉스 계열 커널
    • 형식 검증(Formal verification) : 런타임 오류 없음(AoRTE, Absence of Runtime Errors) 과 구성 요소의 정확성을 보장하기 위해 커널 코드가 거치는 일련의 프로세스와 검사
  • SPARK와 Ada로 작성되어 있으며, 100% 자유 소프트웨어로 구성
  • POSIX 호환 인터페이스, 선점형 멀티태스킹, 강제 접근 제어(MAC) , 하드 실시간 스케줄링 지원
  • GPLv3 라이선스로 배포되며, 펌웨어 블롭 없이 완전한 오픈소스 구조 유지
  • 여러 플랫폼으로 이식 가능하며, Gloire 등 배포판을 통해 생태계 확장 중

Ironclad 운영체제 커널 개요

  • Ironclad는 형식 검증(formal verification) 을 부분적으로 적용한 실시간 대응 UNIX 계열 커널
    • 일반 목적 및 임베디드 시스템 모두를 대상으로 설계
    • 형식 검증(Formal verification) : 런타임 오류 없음(AoRTE, Absence of Runtime Errors) 과 구성 요소의 정확성을 보장하기 위해 커널 코드가 거치는 일련의 프로세스와 검사
    • 이를 위해 Ada 의 서브셋인 ** SPARK** 를 이용
    • 전체 코드가 자유 소프트웨어로 구성
  • 커널은 POSIX 호환 인터페이스를 제공하며, 선점형 멀티태스킹과 강제 접근 제어(MAC) , 하드 실시간 스케줄링을 지원
    • 기존 UNIX 환경과 유사한 개발 경험 제공
    • 실시간 제어가 필요한 시스템에 적합한 구조

자유 소프트웨어로서의 특성

  • Ironclad는 GPLv3 라이선스 하에 완전한 오픈소스로 배포
    • 커널에 펌웨어 블롭(firmware blob) 이 포함되지 않음
    • 스택의 모든 구성 요소가 오픈소스 형태로 제공

형식 검증(Formal Verification)

  • SPARK 언어의 형식 검증 기능을 활용해 주요 구성 요소의 오류 부재와 정확성을 보장
  • SPARK는 Ada 코드에 사전 조건(Pre), 사후 조건(Post), 의존성(Depends) 등을 명세하여 코드의 논리적 일관성을 수학적으로 검증함
    • 검증 대상에는 암호화 모듈, MAC 시스템, 사용자 인터페이스 관련 기능 등이 포함

이식성과 개발 환경

  • Ironclad는 여러 플랫폼과 보드로 포팅되어 있으며, 추가 이식이 용이하도록 설계
    • GNU 툴체인만을 의존해 손쉬운 크로스 컴파일 가능
    • POSIX 호환성 덕분에 소프트웨어 포팅과 개발이 용이

배포판과 생태계

  • Ironclad 프로젝트는 다양한 아키텍처와 보드를 위한 배포판(distribution) 을 제공
    • 대표적인 자유 오픈소스 배포판은 Gloire
    • 다운로드 가능한 tarball 형태의 배포 이미지 제공

프로젝트 지원과 지속성

  • Ironclad는 사용, 연구, 수정이 자유로운 프로젝트로 유지
    • 프로젝트 운영은 기부와 보조금에 의존
    • 모든 기여가 프로젝트 확장과 발전에 직접적인 영향을 미침
▲
GN⁺ 1일전  [-]
Hacker News 의견

  • 흥미로운 프로젝트임. 최악 실행 시간(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도 올라왔는데, 비슷한 흥미로운 프로젝트가 또 있을까 궁금함

    • Asterinas (Linux 호환 커널)과 Redox OS가 유망함
    • SerenityOS도 있음
    • 오래된 대안이지만 Haiku OS도 여전히 흥미로움
    • 나도 OS 아이디어가 있음. 하드웨어, 커널, 사용자 프로그램까지 포함하는 여러 구성 요소를 구상 중임
    • ReactOS도 계속 발전 중임. 완전히 새 OS는 아니지만 여전히 새롭다고 생각함

  • 완전히 형식 검증된 커널이 언젠가 대중화되길 바람
    Linux 전체를 검증하는 건 불가능하겠지만, seL4는 스마트폰 같은 시장에서 기회를 잡을 수도 있을 것 같음

  • 그들의 검증 로드맵을 보면, “형식 검증”이라 부르기엔 과함
    핵심적인 커널 속성에 대한 증명이 없고, seL4나 Tock 같은 커널의 수준에는 미치지 못함

  • CuBit은 SPARK/Ada로 작성된 또 다른 OS임
    소스는 GitHub에서 볼 수 있음

  • 일반 사용자 입장에서는 커널만으로는 쓸모가 없음
    Ironclad 커널을 사용하는 OS 예시는 Gloire임

  • MAC 관련 문서가 잘 정리되어 있음 (Mandatory Access Control)

  • SPARK의 “가격 문의” 문구를 보면, 이건 ‘자유 소프트웨어’ 라기보단 다른 의미의 ‘free’ 같음

    • 위의 GitHub 링크들도 대부분 상업 지원은 유료임. 가격 문의는 일반적인 절차라 특별히 이상할 건 없음
    • 결국 개발자도 생계를 유지해야 함, 그건 당연한 일임
답변달기