SPARK 에이다(Ada) 언어로 개발된 마이크로커널(Microkernel) '드래곤(Dragon)'이 최근 공개되어 주목받고 있습니다. 드래곤은 GNATprove 도구를 활용해 정형 검증(formally verified)을 거쳤다는 점이 가장 큰 특징입니다. 이는 커널의 핵심 기능들이 수학적으로 오류 없음을 증명하여, 시스템의 보안성과 안정성을 극대화했다는 의미입니다.
드래곤 마이크로커널은 역량 기반(capability-based) 설계를 채택하고 있습니다. 이는 스레드 생성, 페이지 매핑, 프로세스 간 통신(IPC) 등 모든 특권 작업이 유효한 역량(capability)과 올바른 권한 비트를 요구하며, 작업 실행 전에 이를 철저히 확인한다는 것을 뜻합니다. 역량은 소유자를 가지며, 해당 소유자만이 역량을 폐기하거나 파생시킬 수 있어 '주변 권한 없음(No ambient authority)' 원칙을 엄격히 준수합니다. 또한, C 언어 개발자를 위해 'libdragon.so'라는 C SDK를 제공하여, 에이다를 직접 다루지 않고도 드래곤 커널 위에서 서비스나 배포 구성 요소를 개발할 수 있도록 지원합니다.
이러한 정형 검증된 마이크로커널의 등장은 고신뢰 시스템 개발 분야에 중요한 시사점을 던집니다. 특히 자동차, 항공우주, 의료 기기 등 안전이 최우선시되는 임베디드 시스템이나 국방 분야에서 드래곤과 같은 커널은 치명적인 버그나 보안 취약점을 원천적으로 방지하는 데 기여할 수 있습니다. 개발자들은 C SDK를 통해 드래곤의 강력한 보안 기능을 활용하면서도 익숙한 C 언어로 개발할 수 있어, 고신뢰 시스템 구축의 진입 장벽을 낮추는 효과를 기대할 수 있습니다.