Prev: Math/CompSci Interview Question - Thoughts?
Next: JSH: Authority from Google search results?
From: Paul E. Black on 23 Nov 2009 13:54
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.black(a)acm.org)
 | 
Pages: 1
Prev: Math/CompSci Interview Question - Thoughts?
Next: JSH: Authority from Google search results?