veyepar: Flying autonomous aircraft: Mixed-criticality support in seL4

Hi user

Admin Login:

Name: Flying autonomous aircraft: Mixed-criticality support in seL4
--client lca --show lca2018 --room green 13549 --force
Prev: 14 Let's write a Debugger!
Next: 14 The State of Kernel Self-Protection

show more...

Author(s):	Gernot Heiser
Location	Green Theatre CB07.02.25
Date	jan Fri 26	Days Raw Files
Start	10:45	First Raw Start	10:10
Duration	0:45:0	Offset	0:34:16
End	11:30	Last Raw End	11:40
Chapters	00:00 0:25:36
Total cuts_time	45 min.

http://lca2018.linux.org.au/schedule/presentation/66/
raw-playlist raw-mp4-playlist encoded-files-playlist host archive public tweet mp4 svg png

final audio

assets release.pdf Flying_autonomous_aircraft_Mixedcriticality_support_in_seL4.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:	We have cracked the problem of safely combining real-time tasks of different criticality on a single system image, removing the main show-stopper for complex mixed-criticality systems as they are emerging in cyberphysical systems such as autonomous vehicles. Mixed-criticality systems (MCS) consolidate multiple functionalities of differing criticality (i.e. severity of failure). MCS are already a reality in avionics, although to date with severe restrictions. A core requirement of MCS is that the correct operation, including timeliness, of critical components must not depend on any less critical components. This requires enforcement of strong spatial and temporal isolation by the OS. Given that MCS are often life-critical, this isolation must be truly bullet-proof, and must be able to stop interference by less critical components that are potentially compromised by an attacker. The industry-standard approach, e.g. mandated by avionics standard ARIC 653, uses strict time-and-space partitioning (TSP), where each component is sandboxed in a fixed memory partition and executes according to a statically configured schedule. This approach is too limiting for emerging MCS, as it inherently leads to poor resource utilisation and inhibits sharing across criticalities. Such sharing is important; e.g. in an autonomous aircraft, the less critical ground-station communication component must be able to update waypoints used by the highly-critical flight-control component. The recently released MCS branch of the formally-verified seL4 microkernel is the first OS that truly matches the requirements of MCS. seL4 already provides provable spatial isolation, the MCS branch adds a scheduling model that provides the right temporal isolation. In particular, it provides time budget enforcement, that can prevent high-priority threads from monopolising the processor. In this talk I will first give a refresher on seL4 and its formal verification story. I will then discuss the requirements of MCS in detail, based on example use cases, and explain why they cannot be matched by existing systems. I will then present the seL4 MCS support and show how it meets the requirements. I will also present autonomous aerial vehicle (AAV) case studies. markdown
Comment:	production notes

recording sheet

recording sheet

2018-01-26/10_10_44.ts Apply: 10:10:44 - 10:40:43 ( 00:29:59 ) S: 10:10:44 - E: 10:40:43 D: 00:29:59 show more...

vlc ~/Videos/veyepar/lca/lca2018/dv/green/2018-01-26/10_10_44.ts :start-time=00.0 --audio-desync=0

	Raw File	Cut List
	10:10:44		seconds: 0.0 Wall: 10:10:44
Duration	00:29:59
	10:40:43		seconds: 0.0 Wall: 10:10:44
Comments:
mp4 mp4.m3u	dv.m3u	Split: Sequence:: delete

audio viz

2018-01-26/10_40_44.ts Apply: 10:40:44 - 10:45:07 ( 00:04:23 ) S: 10:40:44 - E: 11:10:43 D: 00:29:59 (End: 263.0) show more...

vlc ~/Videos/veyepar/lca/lca2018/dv/green/2018-01-26/10_40_44.ts :start-time=00.0 --audio-desync=0

	Raw File	Cut List
	10:40:44		seconds: 0.0 Wall: 10:40:44
Duration	00:29:59
	11:10:43		seconds: 263.0 Wall: 10:45:07
Comments:
mp4 mp4.m3u	dv.m3u	Split: Sequence:: delete

audio viz

2018-01-26/10_40_44.ts Apply: 10:45:07 - 11:10:43 ( 00:25:36 ) S: 10:40:44 - E: 11:10:43 D: 00:29:59 (Start: 263.0) show more...

vlc ~/Videos/veyepar/lca/lca2018/dv/green/2018-01-26/10_40_44.ts :start-time=0263.0 --audio-desync=0

	Raw File	Cut List
	10:40:44		seconds: 263.0 Wall: 10:45:07
Duration	00:29:59
	11:10:43		seconds: 0.0 Wall: 10:40:44
Comments:
mp4 mp4.m3u	dv.m3u	Split: Sequence:: delete

audio viz

2018-01-26/11_10_44.ts Apply: 11:10:44 - 11:30:45 ( 00:20:01 ) S: 11:10:44 - E: 11:40:43 D: 00:29:59 (End: 1201.0) show more...

vlc ~/Videos/veyepar/lca/lca2018/dv/green/2018-01-26/11_10_44.ts :start-time=00.0 --audio-desync=0

	Raw File	Cut List
	11:10:44		seconds: 0.0 Wall: 11:10:44
Duration	00:29:59
	11:40:43		seconds: 1201.0 Wall: 11:30:45
Comments:
mp4 mp4.m3u	dv.m3u	Split: Sequence:: delete

audio viz

2018-01-26/11_10_44.ts Apply: 11:30:45 - 11:40:22 ( 00:09:37 ) S: 11:10:44 - E: 11:40:43 D: 00:29:59 (Start: 1201.0) (End: 1778.0) show more...

vlc ~/Videos/veyepar/lca/lca2018/dv/green/2018-01-26/11_10_44.ts :start-time=01201.0 --audio-desync=0

	Raw File	Cut List
	11:10:44		seconds: 1201.0 Wall: 11:30:45
Duration	00:29:59
	11:40:43		seconds: 1778.0 Wall: 11:40:22
Comments:
mp4 mp4.m3u	dv.m3u	Split: Sequence:: delete

audio viz

2018-01-26/11_10_44.ts Apply: 11:40:22 - 11:40:43 ( 00:00:21 ) S: 11:10:44 - E: 11:40:43 D: 00:29:59 (Start: 1778.0) show more...

vlc ~/Videos/veyepar/lca/lca2018/dv/green/2018-01-26/11_10_44.ts :start-time=01778.0 --audio-desync=0

	Raw File	Cut List
	11:10:44		seconds: 1778.0 Wall: 11:40:22
Duration	00:29:59
	11:40:43		seconds: 0.0 Wall: 11:10:44
Comments:
mp4 mp4.m3u	dv.m3u	Split: Sequence:: delete

audio viz

Rf filename:	root is .../show/dv/location/, example: 2013-03-13/13:13:30.dv
Sequence:
get this:	check and save to add this

2018-01-26/10_10_44.ts
audio viz

audio viz

2018-01-26/10_40_44.ts
audio viz

audio viz

2018-01-26/11_10_44.ts
audio viz

audio viz

Veyepar Video Eyeball Processor and Review