Исходное сообщение
"Heartbeat-уязвимость в OpenSSL могла эксплуатироваться с ноя..." Отправлено vn971, 11-Апр-14 20:21
> А тут нам Тюринг объяснил что нет в жизни счастья. Одна программа не может анализировать другую произвольную программу и выносить какой либо определенный вердикт. FAIL. Это хорошая и приятная теорема, да. Но она на самом деле немного о другом. Теорема утверждает что не может существовать программы которая по любой другой скажет остановится ли она. Но у нас _одна_ программа анализ которой нужно сделать. В общем, я имею в виду вот эту технологию: https://en.wikipedia.org/wiki/L4_microkernel_family (Current research and development) Посмотрите, это может быть интересно.:) > It has been formally verified,[11] which means that there is a (machine-checked) mathematical proof that the implementation is consistent with the specification. This provides a guarantee that the kernel is free of implementation bugs such as deadlocks, livelocks, buffer overflows, arithmetic exceptions or use of uninitialised variables. seL4 is claimed to be the first-ever general-purpose operating-system kernel that has been verified.[11]