A platform-evidence mapping for DAL-B certification planning on an AMD64 multi-core processor with Xen temporal isolation

현대 항공기는 비행 제어부터 항법 및 임무 계획에 이르기까지 모든 것을 관리하기 위해 강력한 컴퓨터에 의존하며 점점 더 복잡해지고 있습니다. 안전을 보장하기 위해 항공 산업은 모든 소프트웨어가 특정 수준의 신뢰도를 갖추도록 테스트되고 검증되어야 한다는 엄격한 규칙을 사용합니다. 비행을 유지하는 것과 같이 가장 중요한 시스템의 경우, 이 신뢰 수준은 가능한 최고 수준입니다. 그러나 이러한 컴퓨터가 현대의 노트북이나 서버에서 볼 수 있는 강력한 프로세서와 유사한 멀티코어 칩으로 진화함에 따라 새로운 과제가 등장했습니다. 여러 프로그램이 동일한 칩의 서로 다른 코어에서 동시에 실행될 때, 이들은 공유 자원, 특히 마지막 레벨 캐시(last-level cache)라고 불리는 고속 메모리 영역에 접근하기 위해 경쟁하게 됩니다. 이러한 경쟁은 한 프로그램이 다른 프로그램을 예측 불가능하게 느려지게 만들 수 있으며, 이는 안전이 중요한 항공 소프트웨어에 위험한 타이밍 불확실성을 초외합니다.

이를 해결하기 위해 연구자들은 이러한 프로그램들을 서로 간섭하지 않도록 격리하는 방법들을 개발해 왔습니다. 유망한 접근 방식 중 하나는 하드웨어와 애플리케이션 사이에 위치하여 컴퓨터 자원을 별도의 보안 구획으로 나누는 하이퍼바이저(hypervisor)라고 알려진 유형의 소프트웨어 관리자를 사용하는 것입니다. 그러나 이 격리가 상업용 항공 분야에서 요구되는 엄격한 기준을 충족할 만큼 강력한지에 대한 의문은 여전히 남아 있습니다. AMD와 뮌헨 공과대학교의 연구팀은 항공기에 사용될 특정 유형의 멀렉코어 컴퓨터를 인증하기 위한 상세한 계획을 수립함으로써 이 문제를 탐구했습니다. 그들의 연구는 AMD 프로세서에서 Xen이라는 하이퍼바이저와 캐시 컬러링(cache coloring)이라는 기술을 결합하여, 서로 다른 소프트웨어 파티션이 실수로 서로의 영역을 침범하지 못하도록 보장하는 구성에 초점을 맞추고 있습니다.

연구진은 구체적인 문제부터 식별했습니다. 멀티코어 프로세서에서는 공유 메모리 캐시가 간섭이 발생하는 주요 지점입니다. 만약 한 프로그램이 캐시를 가득 채우면 다른 프로그램이 대기해야 할 수도 있으며, 이는 중요한 마감 시간을 놓치는 지연을 초래할 수 있습니다. 이를 방지하기 위해 팀은 데이터가 존재하는 위치를 기반으로 컴퓨터 메모리를 별도의 그룹, 즉 "색상(colors)"으로 나누는 방법을 제안했습니다. 각 소프트웨어 프로그램에는 고유한 색상 세트가 할당되며, 시스템은 한 프로그램의 데이터가 다른 프로그램의 데이터를 교체할 수 없도록 구성됩니다. 결정적으로, 이 규칙은 하이퍼바이저 자체에도 적용됩니다. 연구진은 소프트웨어 관리자 자신의 데이터 또한 독점적인 색상 세트에 잠기도록 보장하여, 관리 중인 안전 필수 프로그램의 데이터를 실수로 밀어내는 것을 방지했습니다. 이는 간섭이 단순히 일어나지 않기를 바라는 것이 아니라, 수학적으로 제한되고 예측 가능한 상태인 '경계가 있는(bounded)' 상태임을 보장하는 건설적인 보증을 만들어냅니다.

이 논문은 이러한 기술적 설정을 미국과 유럽의 항공 당국에서 사용하는 공식 인증 규칙에 매핑하여 제시합니다. DO-178C 및 AC 20-193으로 알려진 이 규칙들은 신청자가 공유 자원이 안전하게 관리되고 있음을 증명할 것을 요구합니다. 저자들은 캐시 컬러링 메커니즘이 마지막 레벨 캐시를 효과적으로 격리한다는 것을 보여줌으로써 자신들의 특정 구성이 이러한 요구 사항을 어떻게 충족하는지 입증합니다. 또한, 오픈 소스 커뮤니티에 의해 별도로 문서화된 하이퍼바이저 자체의 안전 사례(safety case)를 항공 제조사가 증거로 재사용할 수 있음을 보여줍니다. 이를 통해 제조사는 기초적인 컴퓨터 하드웨어의 안전성을 처음부터 증명하는 대신, 격리된 환경 내에서 자신들의 특정 애플리케이션이 올바르게 작동하는지 증명하는 데 집중할 수 있습니다. 연구진은 항공 제조업체가 많은 중요하지만 생명 직결적이지는 않은 기능에 적합한 중간 단계의 안전 인증인 DAL-B를 달성하기 위해 이 설정을 사용할 수 있는 명확한 경로를 개략적으로 설명합니다.

그러나 저자들은 자신들의 작업 범위를 정의하는 데 주의를 기울였습니다. 그들은 이 계획이 아직 가장 중요한 비행 제어에 필요한 최고 수준의 인증인 DAL-A를 위한 시스템이 안전하다는 것을 증명하는 것은 아니라고 명시적으로 밝힙니다. 그 높은 수준에 도달하려면 메모리 할당 도구가 절대 실수를 하지 않는다는 것을 수학적으로 공식 증명하고, 특정 프로세서에 대한 더 광범위한 실무 경험을 수집하는 등의 추가 단계가 필요합니다. 또한, 논문은 인공지능 워크로드나 그래픽 프로세싱을 다루지 않는다는 점을 명확히 합니다. 이들은 서로 다른 솔루션이 필요한 신흥 분야이기 때문입니다. 나아가 저자들은 이것이 최종 인증이 아닌 방법론 논문임을 강조합니다. 즉, 구조화된 논거와 도구 세트를 제공하는 것이며, 실제 승인은 각 항공 프로그램의 세부 사항을 검토하는 항공 규제 기관으로부터 얻어야 합니다.

이 연구의 핵심은 이러한 추상적인 안전 규칙들이 어떻게 실제 세계의 컴퓨팅 플랫폼에 적용될 수 있는지에 대한 실질적인 시연입니다. 연구팀은 4개의 코어를 가진 컴퓨터가 비행 제어, 인지, 임무 관리와 같은 서로 다른 작업을 위한 별도의 파티션으로 나뉘는 특정 구성을 설명했습니다. 그들은 각 파티션에 전용 코어와 특정 메모리 캐스 슬라이스를 할당하여, 비행 제어 소프트웨어가 다른 작업들에 의해 느려지지 않고 필요한 자원을 항상 확보할 수 있도록 하는 방법을 보여주었습니다. 또한, 항공기가 이륙하기 전에 메모리 격리가 제대로 작동하는지 확인하기 위해 시스템이 시작 시점에 오류를 점검하는 방법도 상세히 설명했습니다. 이 접근 방식은 항공 산업이 요구하는 예측 가능성과 안전성을 희생하지 않으면서도 강력하고 상용화된 컴퓨터 칩을 사용할 수 있는 방법을 제시합니다.

결론적으로, 이 논문은 상업용 컴퓨팅 하드웨어의 급격한 진화와 항공 안전 인증의 느리고 신중한 속도 사이의 가교 역할을 합니다. 캐시 컬러링과 정적 파티셔닝 하이퍼바이저를 사용하면 간섭이 통제되고 예측 가능한 컴퓨팅 환경을 구축할 수 있음을 보여줍니다. 최고 수준의 인증으로 가는 길에는 여전히 추가적인 작업이 필요하지만, 이 연구는 제조업체가 이러한 고급 프로세서를 항공기에 통합하기 시작할 수 있는 견고한 토대를 제공합니다. 이 작업은 기술적 메커니즘이 존재함을 입증하는 청사진 역할을 하며, 규제 기관이 요구하는 특정 규칙과 증거가 신중하게 준수되고 검증되는 한 멀티코어 통합을 지원할 수 있음을 보여줍니다.