Editing Trusted computing base (section)

===Trusted vs. trustworthy===
As stated [[#A prerequisite to security|above]], [[Trusted system|trust]] in the trusted computing base is required to make any progress in ascertaining the security of the computer system. In other words, the trusted computing base is “trusted” first and foremost in the sense that it ''has'' to be trusted, and not necessarily that it is trustworthy. Real-world operating systems routinely have security-critical bugs discovered in them, which attests to the practical limits of such trust.<ref>[[Bruce Schneier]], [http://www.schneier.com/crypto-gram-0103.html#1 The security patch treadmill] (2001)</ref>

The alternative is formal [[software verification]], which uses mathematical proof techniques to show the absence of bugs. Researchers at [[NICTA]] and its spinout [[Open Kernel Labs]] have recently performed such a formal verification of seL4, a member of the [[L4 microkernel|L4 microkernel family]], proving functional correctness of the C implementation of the kernel.<ref Name="Klein_EHACDEEKNSTW_09">
{{ cite conference
 | first = Gerwin
 | last = Klein
 | first2 = Kevin
 | last2 = Elphinstone
 | first3 = Gernot
 | last3 = Heiser
 | author3-link = Gernot Heiser
 | first4 = June
 | last4 = Andronick
 | first5 = David
 | last5 = Cock
 | first6 = Philip
 | last6 = Derrin
 | first7 = Dhammika
 | last7 = Elkaduwe
 | first8 = Kai
 | last8 = Engelhardt
 | first9 = Rafal
 | last9 = Kolanski
 | first10 = Michael
 | last10 = Norrish
 | first11 = Thomas
 | last11 = Sewell
 | first12 = Harvey
 | last12 = Tuch
 | first13 = Simon
 | last13 = Winwood
 | title = seL4: Formal verification of an OS kernel
 | book-title = 22nd ACM Symposium on Operating System Principles
 | pages = 207–220
 |date=October 2009
 | location = Big Sky, Montana, US
 | url = http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
}}</ref>
This makes seL4 the first operating-system kernel which closes the gap between trust and trustworthiness, assuming the mathematical proof is free from error.