seL4 보안 증명, AArch64에서 완성

SeL4 security proofs now complete on AArch64

Proofcraft가 seL4 마이크로커널이 AArch64에서 기밀성을 강제한다는 공식 수학적 증명을 완료했습니다. 이로써 기능적 정확성, 무결성, 기밀성을 포함한 보안 격리 증명이 AArch64에서 모두 완성되었습니다. NCSC의 지원으로 이루어진 이 성과는 비핵심 애플리케이션의 공격이 핵심 애플리케이션으로 전파되는 것을 방지합니다. 이 증명은 seL4 구현 코드가 애플리케이션 간 보안 격리를 보장한다는 것을 공식적으로 입증합니다.