Anonymous 08/12/2017 (Sat) 19:07:06 No. 10698 del
(822.55 KB 900x900 1501580580130.jpg)

"Formal methods" are not a panacea. There is no guarantee that a formal specification takes into account all of the behaviors that could present a security risk. In addition, the software that is commonly used for these sorts of tasks--Isabelle/HOL, Coq, Agda, etc.--is _software_. It can contain bugs. There's no guarantee that the software correctly proves that a given piece of software correctly implements the specification, which, again, may be imperfect itself.

Even seL4, which you repeatedly shill on this board, even though it's useless to most of the people here (and 99.99999% (repeating) in the real world), comes with a trainload of caveats.

>What are the proof assumptions?
>The brief version is: we assume that in-kernel assembly code is correct,
>hardware behaves correctly,
>in-kernel hardware management (TLB and caches) is correct, and boot code is correct. The hardware model assumes DMA to be off or to be trusted.
>The security proofs additionally give a list of conditions how the system is configured.

So before the proof can even be considered, all of these assumptions have to be taken into account. To take just one, the part about no or trusted DMA is basically a killer for using seL4 on real hardware, as _any_ PCI device has DMA. Your video card, Ethernet card, wireless chip, SD card reader, etc. If your computer has any of those, the assumptions no longer hold, and you can toss out the proof.

Message too long. Click here to view full text.