[liberationtech] Chromebooks for Risky Situations?

Wed Feb 13 08:48:30 PST 2013

seL4 has had readily available code for quite some time now, although
it's under a tl;dr "Non-Commercial License Agreement" that
differentiates itself from open source.
http://ertos.nicta.com.au/software/seL4/home.pyl It's unfortunate, but
it's also par for the course with a lot of academic code. The article
does make it sound like a better license is coming, though.

I'm not surprised that DARPA was first in line for a productized
verified microkernel. Software verification has been a high priority
for DoD since there was software -- it's why the Ada programming
language was developed in the first place. Turns out nobody likes
programming in Ada if they can help it, so DoD is turning to academia
and industry to satisfy the need for verifiability. (Full disclosure:
one of my projects is currently funded under the DARPA Cyber Fast
Track program, and is GPLv2. The software I'm producing is related to
verifiability, and could in fact be used to help secure drones -- but
it can also be used to help secure web servers, end-user applications,
pretty much any software that talks to other software. seL4 is even
more generally useful than that.)

The good news about a verified microkernel, at least, is that you
*can* be assured of whether there's a backdoor in it. (Provided you,
or someone, are able to express that as a formal property and verify
it with a [machine-assisted] proof, that is. I think it's reasonable
to expect the developers of said kernel to provide that proof.)

Cheers,
--mlp

On Wed, Feb 13, 2013 at 9:38 AM, Gregory Foster
<gfoster at entersection.org> wrote:
> 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 b it does. Always. And the
>> developers can prove it to you b 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 || gfoster at entersection.org
> @gregoryfoster <> http://entersection.com/
>
>
> --
> Unsubscribe, change to digest, or change password at:
> https://mailman.stanford.edu/mailman/listinfo/liberationtech
--
Unsubscribe, change to digest, or change password at: https://mailman.stanford.edu/mailman/listinfo/liberationtech

----- End forwarded message -----
-- 
Eugen* Leitl <a href="http://leitl.org">leitl</a> http://leitl.org
______________________________________________________________
ICBM: 48.07100, 11.36820 http://www.ativel.com http://postbiota.org
8B29F6BE: 099D 78BA 2FD3 B014 B08A  7779 75B0 2443 8B29 F6BE