Kojarzy mi się cytat Donalda Knutha: "Beware of bugs in the above code; I have only proved it correct, not tried it". W przeciwieństwie do abstrakcji jaką jest matematyka, kod działa w rzeczywistym, z definicji niedoskonałym świecie. Najprostszy nawet program pokroju sprawdzenia, czy x jest większe od 10 może zawieść. Musimy poczynić po drodze wiele założeń i zaufać wielu elementom - tak kompilatorowi (że poprawnie przetłumaczy kod na instrukcje procesora) jak i hardware'owi (że je faktycznie poprawnie wykona). Co jeżeli sprzęt po prostu zużyje się po X latach użytkowania lub zostanie uszkodzony nagłym skokiem napięcia? Co jeżeli jakaś losowa wiązka promieniowania kosmicznego akurat trafi w hardware i spowoduje, że zgubi się jakiś bit...? (to wbrew pozorom rzeczywisty problem). Nawet zatem gdyby można było przetestować kod dla każdej możliwej kombinacji danych dalej może nastąpić sytuacja, że z przyczyn zewnętrznych kod zawiedzie. Może również zawieść ponieważ jakiś hacker podsunie celowo tak spreparowane dane, żeby dokonać różnych szkód - słynna jest tu historia uszkodzenia irańskich reaktorów wirusem komputerowym (Stuxnet). Tak że nie, nie da się uzyskać 100% poprawności, można jedynie do niej dążyć.
Ale to nie są bugi programu. W takim Sel4 też masz wyjustowane, że program będzie działał poprawnie jeżeli instrukcje procesora działają tak jak w dokumentacji, hardware jest nieuszkodzony etc.
https://sel4.systems/Info/FAQ/proof.pml
What we assume
With a proof in formal logic, it is important to understand what its basic assumptions are, because this is where fault can still occur. Our proof about the seL4 microkernel goes down to the level of the binary code.
Assembly: the seL4 kernel, like all operating system kernels, contains some assembly code, about 340 lines of ARM assembly in our case. For seL4, this concerns mainly entry to and exit from the kernel, as well as direct hardware accesses. For the proof, we assume this code is correct.
Hardware: we assume the hardware works correctly. In practice, this means the hardware is assumed not to be tampered with, and working according to specification. It also means, it must be run within its operating conditions.
Hardware management: the proof makes only the most minimal assumptions on the underlying hardware. It abstracts from cache consistency, cache colouring and TLB (translation lookaside buffer) management. The proof assumes these functions are implemented correctly in the assembly layer mentioned above and that the hardware works as advertised. The proof also assumes that especially these three hardware management functions do not have any effect on the behaviour of the kernel. This is true if they are used correctly.
Boot code: the proof currently is about the operation of the kernel after it has been loaded correctly into memory and brought into a consistent, minimal initial state. This leaves out about 1,200 lines of the code base that a kernel programmer would usually consider to be part of the kernel.
Virtual memory: under the standard of 'normal' formal verification projects, virtual memory does not need to be considered an assumption of this proof. However, the degree of assurance is lower than for other parts of our proof where we reason from first principle. In more detail, virtual memory is the hardware mechanism that the kernel uses to protect itself from user programs and user programs from each other. This part is fully verified. However, virtual memory introduces a complication, because it can affect how the kernel itself accesses memory. Our execution model assumes a certain standard behaviour of memory while the kernel executes, and we justify this assumption by proving the necessary conditions on kernel behaviour. The thing is: you have to trust us that we got all necessary conditions and that we got them right. Our machine-checked proof doesn't force us to be complete at this point. In short, in this part of the proof, unlike the other parts, there is potential for human error.
DMA: we assume that the CPU and MMU are the only devices that access memory directly. The proof can correctly ignore memory-mapped registers of devices, but has to assume that DMA devices are either not present or do not misbehave, for instance by overwriting the kernel. In practise this means, that while normal user-level drivers cannot break kernel security, drivers for DMA enabled devices can and must be formally verified for the proof to carry over. We have current work underway to eliminate this assumption using the SystemMMU on ARM.
Information side-channels: this assumption applies to the confidentiality proof only and is not present for functional correctness or integrity. The assumption is that the binary-level model of the hardware captures all relevant information channels. We know this not to be the case. This is not a problem for the validity of the confidentiality proof, but means that its conclusion (that secrets do not leak) holds only for the channels visible in the model. This is a standard situation in information flow proofs: they can never be absolute. As mentioned above, in practice the proof covers all in-kernel storage channels but does not cover timing channels
