아이언클래드 – 형식 검증된 실시간 대응 유닉스 계열 OS 커널

• 아이언클래드(Ironclad) 는 일반용 및 임베디드 환경을 위한 형식 검증 기반 실시간 대응 유닉스 계열 커널
• SPARK와 Ada로 작성되어 있으며, 100% 자유 소프트웨어로 구성
• POSIX 호환 인터페이스, 선점형 멀티태스킹, 강제 접근 제어(MAC) , 하드 실시간 스케줄링 지원
• GPLv3 라이선스로 배포되며, 펌웨어 블롭 없이 완전한 오픈소스 구조 유지
• 여러 플랫폼으로 이식 가능하며, Gloire 등 배포판을 통해 생태계 확장 중

Ironclad 운영체제 커널 개요

• Ironclad는 형식 검증(formal verification) 을 부분적으로 적용한 실시간 대응 UNIX 계열 커널

  • 일반 목적 및 임베디드 시스템 모두를 대상으로 설계
  • SPARK와 Ada 언어로 작성
  • 전체 코드가 자유 소프트웨어로 구성

• 커널은 POSIX 호환 인터페이스를 제공하며, 선점형 멀티태스킹과 강제 접근 제어(MAC) , 하드 실시간 스케줄링을 지원

  • 기존 UNIX 환경과 유사한 개발 경험 제공
  • 실시간 제어가 필요한 시스템에 적합한 구조

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

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

형식 검증(Formal Verification)

• SPARK 언어의 형식 검증 기능을 활용해 주요 구성 요소의 오류 부재와 정확성을 보장
  • 검증 대상에는 암호화 모듈, MAC 시스템, 사용자 인터페이스 관련 기능 등이 포함

이식성과 개발 환경

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

배포판과 생태계

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

프로젝트 지원과 지속성

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