The short answer is no, Isabelle’s correctness story is not via direct formal verification, and no higher-order logic prover fully has that yet.
Instead, there are two strong trust mechanisms that Isabelle uses:
- (primary) It is a so-called LCF-style prover (LCF=Logic of Computable Functions). This means, there is a small proof kernel, which is the only code that can produce new theorems. Everything else, UI, proof search, proof tactics, complex decision procedures, etc, must go through this kernel to produce theorems and can thereby only make valid derivations in higher-order logic. This is enforced by the type system of the underlying implementation language (ML), i.e. can’t be circumvented by accident.
- (secondary) Isabelle can in principle extract proof terms, which are an explicit representation of the internal proof. These proof terms can be checked by an independent small proof checker. I say “in principle”, because while this does work, the seL4 proofs are currently too large to be exported by the current mechanisms, it runs out of memory.
LCF provers have turned out in last 30 years to be extremely reliable, but of course, as always, we are aiming higher:
In the last few years there’s been a lot of research on verified theorem provers, and there now exists one for a different logic (first-order applicative lisp, the prover is called Milawa), and another one is almost there, which we think can be the basis of the ultimate assurance story in the future (this is the one in the HOL4 community, in the email discussion Harry references). It is called Candle, it is LCF-style, based on ML and higher-order logic like Isabelle, and runs on a verified ML implementation (to binary level, including compiler, runtime, garbage collector etc).
Ramana Kumar, its main developer, has joined our group, and we think we will be able to use it as high-powered proof checker for the seL4 proofs down the track. It’ll be some time, though, until that happens. There’s always more work to be done!
Cheers, Gerwin
On 20.03.2016, at 04:37, Steve VanderLeest Steve.VanderLeest@dornerworks.com wrote:
Since the formal verification of functional correctness of seL4 was performed using the Isabelle theorem prover, could someone tell me if Isabelle itself has been formally verified? If so, could you suggest some good references to that work?
Regards, Steve
Steven H. VanderLeest, Ph.D. Chief Operating Officer DornerWorks, Ltd. 3445 Lake Eastbrook Grand Rapids, MI 49546 www.dornerworks.com
<4DAF62D2-2BAA-43D8-AF48-CB44EF5D13EC[140].png>_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.