Исходное сообщение
"Выпуск VirtualBox 6.0.6" Отправлено Аноним84701, 17-Апр-19 13:22
> Дополню вопрос, существуют ли техники программирования, языки и инструменты, используя > которые можно свести наличие уязвимостей к нулю? Coq, B-Method, Event-B, Isabelle и еще вагон и маленькая тележка – полная формальная верификация постарше многих анонимов будет. Однако, есть одно "маленькое" НО: На примере seL4 c его формальной верификацией корректности: https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf > Abstract > complete formal verification is the only known way to guarantee that a system is free of programming errors. [...] > f L4 provenance, comprises 8,700 lines of C code and 600 lines of assembler. [...] > The overall size of the proof, including framework, libraries, and generated proofs (not shown in the table) is 200,000 lines of Isabelle script. >  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. for a total cost of 2.2 py Т.е. > 8,700 lines of C code and 600 lines of assembler. > 2.2 py Причем, эти совсем не 2 человеко-года "пэхапэшникус-вульгарисов" будут. Поэтому вопрос нужно ставить скорее так: Существуют ли желающие оплатить такую разработку?