Incidentally, NICTA are the same researchers hired by DARPA to make the
U.S. drone fleet safe from hackers. Looks like there might be some open
source tools emerging from the effort.
http://www.theregister.co.uk/2012/11/19/nicta_develops_drone_protection/
gf
On 2/13/13 6:54 AM, Eugen Leitl wrote:
On Tue, Feb 12, 2013 at 09:01:37AM +0100, Andreas Bader wrote:
So why not create a own OS that is really small because of its security?
Chrome OS is small because it's cheap. If you were right then Android
was the most secure system. Aren't there any Android viruses? RedHat
seems to have less security holes than Chrome OS.
http://ertos.nicta.com.au/research/l4.verified/
The L4.verified project
A Formally Correct Operating System Kernel
In current software practice it is widely accepted that software will always
have problems and that we will just have to live with the fact that it may
crash at the worst possible moment: You might be on a deadline. Or, much
scarier, you might be on a plane and there's a problem with the board computer.
Now think what we constantly want from software: more features, better
performance, cheaper prices. And we want it everywhere: in mobile phones, cars,
planes, critical infrastructure, defense systems.
What do we get? Mobile phones that can be hacked by SMS. Cars that have more software
problems than mechanical ones. Planes where computer problems have lead to serious
incidents. Computer viruses spreading through critical infrastructure control systems and
defense systems. And we think "See, it happens to everybody."
It does not have to be that way. Imagine your company is commissioning a new
vending software. Imagine you write down in a contract precisely what the
software is supposed to do. And then — it does. Always. And the developers can
prove it to you — with an actual mathematical machine-checked proof.
Of course, the issue of software security and reliability is bigger than just
the software itself and involves more than developers making implementation
mistakes. In the contract, you might have said something you didn't mean (if
you are in a relationship, you might have come across that problem). Or you
might have meant something you didn't say and the proof is therefore based on
assumptions that don't apply to your situation. Or you haven't thought of
everything you need (ever went shopping?). In these cases, there will still be
problems, but at least you know where the problem is not: with the developers.
Eliminating the whole issue of implementation mistakes would be a huge step
towards more reliable and more secure systems.
Sounds like science fiction?
The L4.verified project demonstrates that such contracts and proofs can be done
for real-world software. Software of limited size, but real and critical.
We chose an operating system kernel to demonstrate this: seL4. It is a small,
3rd generation high-performance microkernel with about 8,700 lines of C code.
Such microkernels are the critical core component of modern embedded systems
architectures. They are the piece of software that has the most privileged
access to hardware and regulates access to that hardware for the rest of the
system. If you have a modern smart-phone, your phone might be running a
microkernel quite similar to seL4: OKL4 from Open Kernel Labs.
We prove that seL4 implements its contract: an abstract, mathematical
specification of what it is supposed to do.
Current status: completed successfully.
Availablility
Binaries of seL4 on ARM and x86 architectures are available for academic
research and education use. The release additionally contains the seL4 formal
specification, user-level libraries and sample code, and a para-virtualised
Linux (x86)
Click here to download seL4
More information:
What we prove and what we assume (high level, some technical background assumed)
Statistics (sizes, numbers, lines of code)
Questions and answers (high-level, some technical background assumed)
Verification approach (for technical audience)
Scientific publications (for experts)
Acknowledgements and team
What does a formal proof look like? [pdf]
Contact
For further information, please contact Gerwin Klein (project leader):
gerwin.klein(at)nicta.com.au
--
Gregory Foster || [email protected]
@gregoryfoster <> http://entersection.com/
--
Unsubscribe, change to digest, or change password at:
https://mailman.stanford.edu/mailman/listinfo/liberationtech
