Исходное сообщение
"Микроядро seL4 математически верифицировано для архитектуры ..." Отправлено erthink, 10-Июн-20 18:24
> > не решается (и возможно никогда не решится) сделать Kaspersky OS Open Source. > о какой вообще проверке может идти речь при отсутствии открытых исходников? Открыть исходники для проверки - это одно (у M$ в таком режиме они открыты >25 лет). А перейти на открытую лицензию и модель open source - это совсем другое. Но палка тут о двух концах - если модель (и DSL её описания) окажутся удачными (а похоже так и есть), то повторить уже проверенную концепцию относительно просто поверх любого подходящего ядра (даже натянуть на Linux, хотя будет масса проблем). Т.е. если Kasperky OS "взлетит" и при этом останется closed-source, то китайцы (или еще кто-то) повторят разработку за ~1-2 года.