포어사이트뉴스(Foresight News) 에 따르면, 웹3 보안 기업 CertiK와 알리바바 그룹 산하 알리페이의 알리 보안 연구소가 차세대 오픈소스 범용 운영체제 '아스테리나스(Asterinas)'의 핵심 구성 요소에 대한 형식적 검증을 공동으로 발표했습니다. 아스테리나스는 Rust로 개발되어 Linux 애플리케이션과 호환됩니다. 이번 작업은 Rust 운영 체제에 대한 형식적 검증의 중요한 진전을 보여주며, 이를 통해 '수학적 증명 수준'의 보안 표준을 달성하고 차세대 범용 운영 체제의 보안성 향상을 위한 새로운 접근법을 제시했습니다.

이전에 CertiK는 알리 보안 연구소의 TEE 플랫폼 HyperEnclave에 대한 형식적 검증을 성공적으로 수행한 바 있습니다.