Re: recent formal proof re: seL4 microkernel
David Bernier
> I read about this in some computer security forum or magazine:
[ comp.theory removed, sci.crypt added ].
> "seL4: Formal verification of an OS kernel" presented at
> Proceedings of the 22nd ACM Symposium on Operating Systems Principles,
> Big Sky, MT, USA, October, 2009
>
> Authors:
> Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David
> Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski,
> Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood.
>
> This is a project at the NICTA Institute in Australia.
>
> Cf.:
> < http://ertos.nicta.com.au/research/sel4/ > .
>
> ---
>
> This is my own summary: There's a detailed specification for how the
> micro-kernel should behave. Then there's the C language source code
> which, when compiled, linked, etc. gives the micro-kernel.
> A proof assistant was used to give a formal proof that the
> micro-kernel behaves as in the specification.
>
> ---
>
> Having a secure system/environment has many components:
> - no tampering
> - trusted sys admins
> - users that don't use weak passwords
> - an operating system with as few bugs as possible.
>
> So, could seL4 be harnessed in some way to mitigate cyber-attacks?
>
> Linux can be used to run Windows programs with _wine_ .
>
> So could someday seL4 and its descendants be used to run Linux
> programs?
>
> David Bernier
Mok-Kong Shen
>> < http://ertos.nicta.com.au/research/sel4/ > .
>> This is my own summary: There's a detailed specification for how the
>> micro-kernel should behave. Then there's the C language source code
>> which, when compiled, linked, etc. gives the micro-kernel.
>> A proof assistant was used to give a formal proof that the
>> micro-kernel behaves as in the specification.
I have some layman's questions. Doesn't a 'normal' user have to 'trust'
that the proof has been correctly done by the designers? If the source
code is o.k. and one compiles it on one's computer, wouldn't the
correctness be dependent on whether the computer and the compiler at
that moment is o.k., i.e. free of viruses, trojans, etc.? I don't
doubt the extremely high value of a formally proved kernel but simply
want to say that, if one were 'pedantic' enough, one probably could
still find some arguments to say that it is not 'perfect'.
M. K. Shen
David Bernier
I've read a bit about formal proofs, and how the
output of a "Hol"-prover
proof (The Proof) can be checked on another machine with
another architecture and OS which has "Hol".
As for trusting a system who produces the Proof or verifies it
(you mention viruses and trojans), I don't think these concerns can
be dismissed, even if the Proof is produced on one system
and verified on another.
Also, as I understand it, what is verified is the
(usually) C source code for the kernel. They
have to trust the compiler who will compile that C code
and give a working kernel.
There's an interesting article from 2005 by Bell, known for
the Bell-La Padula Model. Bell looks back on thirty years
of work on making operating systems more secure:
< http://www.acsac.org/2005/papers/Bell.pdf >
David Bernier
Mok-Kong Shen
> Mok-Kong Shen wrote:
>> I have some layman's questions. Doesn't a 'normal' user have to 'trust'
>> that the proof has been correctly done by the designers? If the source
>> code is o.k. and one compiles it on one's computer, wouldn't the
>> correctness be dependent on whether the computer and the compiler at
>> that moment is o.k., i.e. free of viruses, trojans, etc.? I don't
>> doubt the extremely high value of a formally proved kernel but simply
>> want to say that, if one were 'pedantic' enough, one probably could
>> still find some arguments to say that it is not 'perfect'.
> I've read a bit about formal proofs, and how the
> output of a "Hol"-prover
> proof (The Proof) can be checked on another machine with
> another architecture and OS which has "Hol".
>
> As for trusting a system who produces the Proof or verifies it
> (you mention viruses and trojans), I don't think these concerns can
> be dismissed, even if the Proof is produced on one system
> and verified on another.
>
> Also, as I understand it, what is verified is the
> (usually) C source code for the kernel. They
> have to trust the compiler who will compile that C code
> and give a working kernel.
>
> There's an interesting article from 2005 by Bell, known for
> the Bell-La Padula Model. Bell looks back on thirty years
> of work on making operating systems more secure:
>
> < http://www.acsac.org/2005/papers/Bell.pdf >
Some time ago, I knew that compilers of some programming languages
can be tested and certified by standardization bodies as conforming
to the standards. So perhaps such provably correct kernels could also
obtain similar certificates somewhere and be distributed by an
authorized institution to the end users in a safe manner. This way,
provided the computer of a user is not bugged, the kernel installed
would be o.k. in practice.
M. K. Shen