Исходное сообщение
"Google открыл код защищённой операционной системы KataOS" Отправлено anonymous, 16-Окт-22 13:29
Примерно те же люди, которые сделали проект seL4, сделали проект CakeML - a functional programming language and an ecosystem of proofs and tools built around the language. The ecosystem includes a proven-correct compiler that can bootstrap itself. А что сделали инженеры Google? Пока что просто написали неверифицированный код на Rust, но бахвалятся безопасностью проекта. Да ещё только под RISC-V и ARM64. И запускают это на своих вендорлокнутых железяках. А всем остальным предлагают веровать в безопасность этих решений. Спасибо, пусть оставят внутри своей корпорации как и Zircon, который в пару шагов эксплуатировали реята из Positive Technologies.