Исходное сообщение
"Удалённо эксплуатируемая уязвимость в драйвере NVMe-oF/TCP и..." Отправлено Аноним, 16-Окт-23 16:39
Не совсем правда. Вот есть seL4, не просто статистически проверено, но даже формально верифицировано. Оно на 73% написана на С, https://github.com/seL4/seL4 Правда есть 2 существенных НО: 1. оно маленькое - там оклоло 36к строк на С, из которых 11к это пустые и комментарии (что уже намекает на сложность). (с другой стороны микроядро и должно быть маленьким) 2. его писали руками, сразу думая о том как они будут его верифицировать. Пришлось потрудиться и использовать Isabelle и Haskell. Кол-во строк скриптов только первой было больше 200к строк. И это было довольно дорого The abstract spec took about 4 person months (pm) to develop. About 2 person years (py) went into the Haskell prototype (over all project phases), including design, documentation, coding, and testing. The executable spec only required setting up the translator; this took 3 pm. The initial C translation was done in 3 weeks, in total the C implementation took about 2 pm, for a total cost of 2.2 py including the Haskell effort. (статья https://cseweb.ucsd.edu/~dstefan/cse227-spring20/papers/sel4...)

Ваше сообщение
Имя*:
EMail:	Для отправки ответов на email укажите знак ! перед адресом, например, !user@host.ru (!! - не показывать email). Более тонкая настройка отправки ответов производится в профиле зарегистрированного участника форума.
Заголовок*:
Сообщение*:
	Введите код, изображенный на картинке: