veyepar: seL4 Is Free – What Does This Mean For You?

Author(s):	Gernot Heiser
Location	OGGB3
Date	jan Wed 14	Days Raw Files
Start	11:35	First Raw Start	11:34
Duration	0:45:00	Offset	0:00:36
End	12:20	Last Raw End	12:25
Chapters	00:00
Total cuts_time	49 min.

http://lca2015.linux.org.au/schedule/30011/view_talk
raw-playlist raw-mp4-playlist encoded-files-playlist host public tweet mp4 svg png

assets release.pdf seL4_Is_Free_What_Does_This_Mean_For_You.json
logs
Admin: episode episode list cut list raw files day marks day marks day image_files

State:

Locked:

clear this to unlock

Locked by:

user/process that locked.

Start:

initially scheduled time from master, adjusted to match reality

Duration:

length in hh:mm:ss

Name:

Video Title (shows in video search results)

Emails:

email(s) of the presenter(s)

Released:

has someone authorised pubication

Normalise:

Channelcopy:

m=mono, 01=copy left to right, 10=right to left, 00=ignore.

Thumbnail:

filename.png

Description:

markdown

seL4 is the world's most secure OS kernel, in a very strong sense: It has a mathematical proof of security that connects high-level security and safety properties with the binary code that is running on the processor, there is no other system that can make such clams. And it is 100% Australian-made.

seL4 runs on ARM and x86 processors and combines the properties of a general-purpose microkernel, a military-style separation kernel, a hypervisor able to run Linux, a protected-mode real-time OS and more. However, until recently it was locked up and basically inaccessible. But, as of 29 July 2014 it is open source.

In this talk I will briefly explain what seL4 is (and isn't), what it can do and where it can be deployed, and what its formal verification is all about, i.e. what it can and cannot guarantee.

Then I will focus on discussing what this means for the community. As seL4 defines the state of the art in trustworthy systems, I will make the point that it is the right platform for new designs of safety- or security-critical systems, where failure can lead to loss of life or may have massive financial impact. I will encourage the community to contribute to building the seL4 ecosystem, and use it to make everyday computer systems more dependable.

Comment:

production notes