recent formal proof re: seL4 microkernel

[David Bernier]

I read about this in some computer security forum or magazine:

"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

[Paul E. Black]

On Sunday 22 November 2009 13:38, David Bernier wrote:
> "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
>

> ... [PEB]
>
> < http://ertos.nicta.com.au/research/sel4/ > .

>
> ---
>
> 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?

Yes. Using seL4 may reduce the number of bugs that might be
exploitable. Also one can build formally verified components,
including an operating system, on a formally verified kernel.

A secure system has another components: a comprehensive, enforced
security policy. Suppose the above four items were the only
guarantees. Say I write a payroll program that needs to (and is
authorized to) read a file of social security numbers, which should be
kept confidential. Suppose every February 29th it shares those
numbers with the world. Clearly a security breach. The OS did what
it should. The difficulty is that some applications must enforce some
security policies.

Can anything be done? The OS might track permissions at a finer
grain. For instance, if a program reads the social security number
file, it is tagged as "tainted" and no longer allowed to broadcast on
the internet. This wouldn't prevent all problems, but it might catch
more.

> So could someday seL4 and its descendants be used to run Linux
> programs?

Yes it could. I believe that someday they will.

-paul-
--
Paul E. Black (p.b...@acm.org)