[Cryptography] Yet more formal methods news: seL4 to go open source

[Phillip Hallam-Baker]

On Mon, Jun 9, 2014 at 12:25 PM, Perry E. Metzger <perry at piermont.com> wrote:
> On Mon, 9 Jun 2014 11:35:31 -0400 Jerry Leichter <leichter at lrw.com>
> wrote:
>> Workable formal verification is going to have significant effects
>> on the whole programming ecosystem.
>>
>> Consider the interaction between verification and open source. If
>> you make *any* changes to a verified piece of code, you lose the
>> verification.
>
> Yes, so one has to make sure changes re-verify.
>
> Note if one uses a system like Coq to write the verified
> code in the same system that is doing the verification, there is no
> meaningful distinction between the proof and the source code to the
> system.
>
> If, on the other hand, one writes the code in a separate language and
> merely uses Coq (or Isabelle or what have you) as a proof system,
> then one needs to distribute both the code for the system and the
> formal specification/verification code.
>
>> So just what does having access to the source buy you?
>
> The same thing it does now.
>
>> Perhaps we can get to a world in which anyone who changes the code
>> is expected to update the verification. With the state of the tools
>> we have now, that seems unworkable - it's just too hard and
>> specialized.
>
> Have you tried? Indeed, if you write your code in a dependently typed
> style within Coq or what have you, how does one meaningfully update
> the code *without* updating the proof? (There are quite interesting
> artifacts written with Coq itself -- CompCert, for example.)

Folk should remember that for the purposes of security, the most
important concern is not whether the algorithm is 'correct', it is
whether the code has buffer overrun, memory leak or access to
unallocated memory.

So we are solving a problem that is much easier than the 'Turing
complete' or 'AI complete' problems that people like to use as 'proof'
formal methods don't work. We don't have to prove every aspect of
every program to make advances.

But equally, a managed language such as C# provides the above concerns
for free. Which is why I switched from C as soon as the managed
languages became good enough and the IPR issues were clarified.