seL4 보안 증명, AArch64에서 완성
SeL4 security proofs now complete on AArch64
Proofcraft가 seL4 마이크로커널이 AArch64에서 기밀성을 강제한다는 공식 수학적 증명을 완료했습니다. 이로써 기능적 정확성, 무결성, 기밀성을 포함한 보안 격리 증명이 AArch64에서 모두 완성되었습니다. NCSC의 지원으로 이루어진 이 성과는 비핵심 애플리케이션의 공격이 핵심 애플리케이션으로 전파되는 것을 방지합니다. 이 증명은 seL4 구현 코드가 애플리케이션 간 보안 격리를 보장한다는 것을 공식적으로 입증합니다.
이 격리는 비핵심 애플리케이션에 대한 공격이 핵심 애플리케이션으로 전파되어 손상시키는 것을 방지합니다.
HN 토론
52- StilesCrisis
곧 출시될 예정: 이 결과를 완전히 무효화하는 부채널 타이밍 공격
- i_am_a_peasant
세부 사항을 읽어보세요, "비-MCS(혼합 중요도 시스템), 단일 코어"
- kvuj
어떤 운영 체제가 seL4를 사용하나요? 제가 아는 것은 다음과 같습니다:
- GenodeOS
- LionsOS
- 중국 자동차 제조사가 자동차의 하이퍼바이저로 사용하고 있었습니다, 제가 기억하기로는
- 그 외에 무엇이 있나요? 아시는 사설 배포 사례가 있나요?
- avadodin
임베디드 및 군사 시장은 당분간 그들에게 자금을 지원할 수도 있지만, 그들의 역량 모델로 시스템 보안을 개선하고 있다고 정직하게 주장하려면 네이티브 seL4/Linux가 필요합니다.
보안 부팅 가상화 플랫폼은 요즘 흔합니다.