View Single Post
  #2   (View Single Post)  
Old 11th January 2017
e1-531g e1-531g is offline
VPN Cryptographer
Join Date: Mar 2014
Posts: 448

Formal verification is a very time consuming process. Designing something that can be formally verified is very consuming process. seL4 is just few thousand lines of code, so it can be designed (microkernel) and formally verified. Something the size of OpenBSD kernel with all the drivers is beyond resources such as work hours.
Even then formal verification it does not tells you that you can be sure this system is secure. It only proves that code is doing everything that is written in description of code. If assumptions of description are incomplete or wrong, the code probably have bugs.
Of course formal verification improves code quality by orders by magnitude.

You also should keep in mind that world changes. Hardware changes. Protocols are changing. Your project must be flexible enough to adapt to this changes and incorporate new features at reasonable pace.

Signature: Furthermore, I consider that systemd must be destroyed.
Based on Latin oratorical phrase
Reply With Quote