What's new in the world of seL4

Video in TIB AV-Portal: What's new in the world of seL4

Formal Metadata

Title
What's new in the world of seL4
Title of Series
Author
License
CC Attribution 2.0 Belgium:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
2019
Language
English

Content Metadata

Subject Area
Abstract
This talk will cover the developments of and around seL4 over the past 4 years, covering new and improved functionality for supporting mixed-criticality real-time systems, status and future of its formal verification, an overview of past and future deployments, and an assessment of the state of seL4's open-source ecosystem. seL4 is the world's first (and still only real-world suitable) operating system (OS) kernel with a machine-checked, formal (mathematical) proof of implementation correctness. It has further proofs of security enforcement (the CIA properties of confidentiality, integrity and availability). It is also, the only protected-mode OS (as far as the open literature goes) with a complete and sound worst-case execution-time analysis, the key to supporting hard real-time applications. Much has happened since I last talked about seL4 at FOSDEM 4 years ago, half a year after it had been open-sourced (GPL). In the meantime it has flown a full-size helicopter in autonomous mode while withstanding a cyber-attack (which easily succeeded when the chopper was running on Linux), driven autonomous trucks, and flown in space. It's in commercially developed security-critical systems in use in multiple defence forces and is making its way into commercial safety-critical systems. Arguably, seL4's greatest weakness is a spartanic development environment and a paucity of components running on top, at the moment it's mostly BYO Ethernet driver and file system. We, the developers at Data61 have to accept some blame for that: we weren't sufficiently proactive in encouraging community contributions. Note that this was not because we don't want them, but simply because we were too busy. We're in the process of changing that, in collaboration with the DARPA-funded US seL4 Center of Excellence, which is focussed on providing open-source tools and components on top of se4, but also provide development services to commercial users. On our end we are working on better documenting what is there, and what is maintained and by whom. We hope to encourage people to adopt existing userland components/tools and contribute further ones. A major enabler of this is a device-driver framework that defines driver interfaces and protocols. We hope to release this soon. The DARPA-sponsored first seL4 Summit held in Washington in Nov'18 with 140 attendees demonstrated the growing ecosystem and user base, including companies building frameworks for medical devices and autonomous vehicles. I hope this talk will also help to build the community. On the research side, seL4 has made great progress in the past 4 years. It has been enhanced by a new scheduling model with capability-based control over time, arguably the first and only OS with a principled treatment of time as a resource, and the first able to support mixed-criticality real-time systems without sacrificing utilisation. This enhancement is presently undergoing verification, and lives in the MCS branch until verification is completed, after which it will become the mainline version. The kernel's correctness and security proofs have grown to about 1 million lines (all open source) and have been maintained over ten years of evolution of the code base, now also including functional correctness on the x86 architecture. A RISC-V port is available and is undergoing formal verification as well. This is by far the larges, maintained proof base in the world, and has led to the new discipline of proof engineering to manage maintenance and evolution. There is further work on pushing the mathematical guarantees into userland, especially the CAmkES component architecture and the Cogent language system, aimed at producing systems components (drivers, file systems, network stacks) that can be verified at a cost that is not far from that of traditional quality-assurance processes. Both frameworks are also open source (tools are GPLed while libraries are BSD). CAmkES is mature and in routine use for building secure systems, Cogent is still rapidly evolving, but is increasingly used by externals. Finally we are working on ways for preventing information leakage through timing channels, considered an unsolvable problem by most.
Loading...
Goodness of fit Touchscreen Open source Multiplication sign Shared memory Bit Game theory
Slide rule Hill differential equation
Point (geometry) Computer program Java applet Hacker (term) Gradient System programming System programming Denial-of-service attack Software testing
Software Robotics System programming Virtual machine System programming Control flow Existence Information security Computing platform ARPANET
Computer font Enterprise architecture Cellular automaton Mikrokernel Mikrokernel Mereology Computer font Number Mixed reality Kernel (computing) System programming Information security Scheduling (computing) Operating system
Slide rule Asynchronous Transfer Mode Implementation Open source Code INTEGRAL Multiplication sign Tape drive Mikrokernel Virtual machine Translation (relic) Real-time operating system Mathematical analysis Semantics (computer science) Portable communications device Power (physics) Formal language Revision control Chain Exclusive or Cache (computing) Kernel (computing) Formal verification System programming Best, worst and average case Information security Covering space Model theory Physical law Mathematical analysis Mikrokernel Translation (relic) Cognition Compiler Category of being Proof theory Kernel (computing) Logic Chain System programming Information security Functional (mathematics) Arithmetic progression Asynchronous Transfer Mode
Classical physics Token ring Data storage device Core dump Thread (computing) Mechanism design Type theory Pointer (computer programming) Forest System programming Cuboid Representation (politics) Spacetime Object (grammar) Musical ensemble H├╝llenbildung Operating system Address space
Mechanism design Slide rule Prime ideal Touchscreen Token ring Spacetime Core dump Thread (computing) Address space
Complex (psychology) Scheduling (computing) INTEGRAL Multiplication sign View (database) Disintegration 1 (number) Real-time operating system Simulated annealing Mixed reality Energy level System programming Spacetime Control theory Information Interrupt <Informatik> Control system Data integrity Scaling (geometry) Token ring Core dump Thread (computing) Mechanism design Data management Software Mixed reality Telecommunication Order (biology) System programming Control theory Quicksort Scheduling (computing) Address space
Thermodynamischer Prozess Multiplication sign Disintegration Data storage device 1 (number) Shared memory Insertion loss Mereology Software Mixed reality Hypermedia Befehlsprozessor Control theory System programming Control theory Interrupt <Informatik> Loop (music)
Server (computing) Context awareness Multiplication sign Execution unit Limit (category theory) Client (computing) Semantics (computer science) Revision control Frequency Term (mathematics) Operator (mathematics) Program slicing Authorization System programming Computer multitasking Control theory Control system Context awareness Boss Corporation Server (computing) Attribute grammar Thread (computing) Band matrix Befehlsprozessor Frequency Personal digital assistant Control theory Right angle Object (grammar) Scheduling (computing)
Point (geometry) Context awareness Server (computing) Enterprise architecture Service (economics) Concurrency (computer science) Weight Multiplication sign Real-time operating system Client (computing) System programming Information security Context awareness Thermodynamischer Prozess Enterprise architecture Server (computing) Forcing (mathematics) Client (computing) Mechanism design Process (computing) Befehlsprozessor Personal digital assistant System programming Information security Scheduling (computing)
Computer chess Point (geometry) Computer program Interface (computing) Mikrokernel Message passing Goodness of fit Kernel (computing) Object (grammar) Order (biology) System programming System programming Representation (politics) Backup Energy level Energy level Object (grammar) Table (information) Abstraction
Enterprise architecture Enterprise architecture Link (knot theory) View (database) Virtual machine Semaphore line Line (geometry) Type theory Optical disc drive Message passing Cryptography Personal digital assistant Core dump Interface (computing) Energy level Representation (politics) Cuboid System programming Quicksort Middleware Information security Middleware
Dataflow Computer program Implementation Functional (mathematics) Enterprise architecture Code State of matter View (database) Virtual machine Combinational logic Compiler Shape (magazine) Hardware description language Term (mathematics) Operator (mathematics) Formal verification System programming Energy level Cuboid Representation (politics) Diagram Address space Alpha (investment) Enterprise architecture Multiplication Electric generator Moment (mathematics) Data storage device Line (geometry) Cryptography Limit (category theory) Formal language Compiler Category of being Proof theory Message passing Linker (computing) Telecommunication Order (biology) Condition number Energy level Quicksort Object (grammar) Game theory Information security Operating system Library (computing)
Convolution Enterprise architecture Standard deviation Enterprise architecture Electric generator Open source Open source Mathematical analysis Code Mathematical analysis Markup language Binary file Formal language Hardware description language Kernel (computing) Personal digital assistant Formal verification System programming Maize Quicksort Spacetime
Convolution Functional programming Computer program Functional (mathematics) Implementation Abstract data type Observational study Code Translation (relic) Mereology Semantics (computer science) Product (business) Formal language Number Latent heat Read-only memory Semiconductor memory Personal digital assistant Formal verification File system Bus (computing) System programming Energy level Control theory Medizinische Informatik Software framework Data type Programming language Observational study Key (cryptography) Forcing (mathematics) Code Line (geometry) Formal language 10 (number) Compiler Type theory Proof theory Category of being Kernel (computing) Personal digital assistant Network topology Order (biology) System programming Linearization Compilation album Data type Reduction of order
Group action Code Interior (topology) Model theory Multiplication sign Stack (abstract data type) Disk read-and-write head Formal language Formal verification File system Cuboid Category of being Library (computing) Proof theory Electronic mailing list Mikrokernel Sound effect Bit Formal language Proof theory Category of being Software testing Automation Functional (mathematics) Arithmetic progression Writing Reduction of order Spacetime Classical physics Point (geometry) Functional (mathematics) Implementation Maxima and minima Similarity (geometry) Device driver Product (business) Power (physics) Number Revision control Latent heat Term (mathematics) Hierarchy System programming Software testing Theorem Form (programming) Expression Code Computer network Stack (abstract data type) Line (geometry) Loop (music) Model checking Software Personal digital assistant Universe (mathematics) Synchronization Game theory
Software developer Real number Core dump Information privacy Cartesian coordinate system Database normalization Database normalization Machine learning Personal digital assistant Autonomic computing System programming Medizinische Informatik Quicksort Gamma function
Building Group action State of matter Multiplication sign View (database) Mereology Proper map Information technology consulting Mathematics Oval Software framework Process (computing) Multiplication Area Email Mapping Software developer Moment (mathematics) Electronic mailing list Bit Staff (military) Student's t-test Process (computing) Order (biology) System programming Control theory Self-organization Quicksort Spacetime Reduced instruction set computing Service (economics) Open source Software developer Real number Student's t-test Number Local Group Latent heat Goodness of fit Performance appraisal Autonomic computing System programming Analytic continuation Computing platform Projective plane Core dump Computer network Stack (abstract data type) Performance appraisal Kernel (computing) Formal verification Table (information)
Enterprise architecture Thermodynamischer Prozess Implementation Email Software Mixed reality Computer hardware Expert system Control theory Right angle Object (grammar) Spacetime
well welcome good morning and apologies
for not being there in person and I suppose most nights okay can you see this like in as long as I don't hear anything I assume it's a yes even though not in person and thanks for getting up early to listen to this it's four years since I last gave a talk across there and at a time I see oh boy I trust in open source and a lot has happened in the meet I'm so give you a bit of an update and it talked about where the community side so this thing represents one of the more exciting things that has happened with SEO for you know this is a yeah no it's not Oh God okay okay for some reason stop sharing I'll share game your screen sharing you
should and now you should see the slide
yeah go straight okay so this is one of
the things that happened recently what you see here is a Boeing helicopter
flying and it's not just flying its
final Panama City this is pilot on board for safety reasons because they don't get FAA approval for flying it without it but it's actually fine called the autonomously this is say in around Arizona and of course the exciting thing
about it is flying on a CL for what's
even more interesting is some of the history here
so this is a military-grade system it's actually a defense system and you should think it's reasonably secure but turns out that professional pen testers took about two weeks to complete it and then they could completely control the flooding could have crashed into or divert it at whatever and this was the starting point in the Java hackers program which started which ran for about five years finished about a year ago and we did with our colleagues there is convert the system and to a sea of
formated secure so in total there were
four vehicles there were two ground vehicles and that to breathe air vehicles each of them had a research platform I've just thrown where we ripped out all the electronics and replaced all the software and this US Army robotics reference platform and
then the military vehicles which is following up on the selling of the Ottoman stocks and we did with our partners were real fitting these systems for security by putting them on SEO for and doing some of the architecting of the system then in the end we kept the echos hours they will say they know where they did a in-flight attack that in the past would have completely compromised the system and it was completely protected specifically we gave them with access to a virtual machine running Linux on the system the original system had everything running on Linux and the attacker could completely compromised the Linux VM but it couldn't break our deal affect the rest of the system so
that so much as motivation a rough outline of my talk is quick intro to a cell for a technical update on a number of the things that happened in the last few years and this is the part of the talk and then at the end I'll talk about the status of fear the community and ecosystem so for those who haven't heard
about SEO for its a microkernel and it's
arguably the world's most secure and safe operating system one is perfectly
unique a power that it has secured portable security enforcement and I'll talk about on the next slide what that means it's also at least as fast the open literature is concerned the only protective mode operating system with a complete and sound analysis of worst-case timing behavior so that super existed for doing hard real-time they need to take new McSweeney Kalinina real-time with us trusted and untrusted components insights all that it's the world's fastest microkernel we never compromise with performance and of course that's the reason I mean it's open source and it's been open source support for nine years ago so the security the story is summarized
in this slide where say proof here this means mathematical formal mathematical proof that is checked by a Miss machine tape so we have high-level security cognitive properties confidentiality integrity availability enforcement and we have proof that an abstract model of the kernel which is formulated in a mathematical logic is able to enforce these security properties and then we have a further proof that the C code that implements the kernel is a what's called a refinement of this abstract model so it's a correct implementation of this law so that specifically this means the under the semantics of the C language the kernel cannot behave in a way that's not captured by the model and then there's a further step that shows that the binary cover that buns on the actual silicon is a correct translation of the C so that means we don't have the trust of C compiler we can't just use standard untrusted and untrusted BTCC to compile and then run the tool chain that's dismissive translations quick for pretty good advertising there's a few exclusions all are work in progress we're working on fixing all of them colonel initialization is not verified that some privileged saved in particularly I mean user not yet to verify the de same degree of detail as everything else that's very close to being fixed we have a high performance Nordica version that's not verified and we don't have any stuff verification story about tiny channels that not like
any ice security-oriented operating system SEO forests uses capabilities as for to represent access lives in the system and so these are basically opaque pointers that reference an object and lights convey to it and any kernel operation you type in boldly store be authorized by having such a capability so these are capabilities in the classical object capability for master computing the tutor has known them for forty years they're quite different from the what the Linux box called capabilities which are chemical this and [Music]
strangest of them accidentally eat again
accidentally the power cool okay I just need nah okay okay hopefully
you can see the slides again full screen if not me yeah okay good okay so this is
say that the in a very high level called your face here for there's much more to it in particular its resource management more model which is quite unique but that's all the establish so if you don't know a summary of recent things we've
done with it and one of the most significant ones is support for mix criticality real-time scheduling what does that mean so in many particular
cyber-physical systems any sort of real-time system where you have non-trivial complexity you have this integration challenge of mix criticality that some components are highly critical and you need to be sure that they get toward that they operate correctly under all circumstances and then there's untrustworthy components so a very high obstructed view of this UAV as a control loop which is highly critical because that's what pieces they fly and stops it from crashing and then there's other components for example those networks and so there's a network driver that talks for the ground station for example or the communication and obviously that one is not critical if the communication stops working then this thing will just light relay or to a waypoint or hopefully has something safe not cheap to fly it home or something the challenge here is the controller will be very slow at once of the order advanced annealing time scale so would of Tindall under threats the network driver of course is really fast if networks like to be serviced within sort of microsecond time scales and that means that this network driver needs to be able to interrupt the controller witches can't wait for the
controller to finish its 20 millisecond execution because it lose lot of network packets so you have to be able for this less critical components to grant the critical ones but still guarantee enough time for the critical component store do it shop was from safety of your system so that that's the quality of next critical systems what makes it
challenging is active sharing involved so typically in our UAV there instead of the vehicle controlled it tells the deeper where the flight or so it has to access waypoints these waypoints they get updated by the navigation system for example based on what the media processing tells the system or updated from the ground station and so the true the trusted and young lets faster parts share this critical data and the legal control needs to be accessed please be able to access data that is consistent even while the navigation system they updated and you need to do that on on the same system a simple way
to even make something like that is by what's called a resource server so we have the the two components that use this and Waypoint data to control the critical controller and the less critical navigation system and the Waypoint data is EB B capsulated in a server which can be invoked from those spies and that we gain from system you might invoke the client to update my clients and the control system may invoke the server to beat the way pots so it's all fine and if long as to survive stable enough and fast enough that maybe not a big deal the problem is particularly this server has some longer running operations then we need to count the time properly because otherwise the navigation system which is argued before might be running at higher priority just boss the critical system by sending lots of requests for server so we need to ensure that if time is isn't handed
properly and in the new version of a C or four we do we use capabilities like for every access control that the system we introduced capabilities for the right to use OSS of time so a classical threat will have quality and a time slice in the new SEO for we have authority and the shielding context capability which is capability to a shave lean object which is encapsulate the rights to access the CPU so it has a period and a budget and the semantics is that over any time T you cannot use more than C of the policies or so the ratio of C 2 T is C the bandwidth of CPU this policies allowed to consume and there can be for example what terms one so in this case in three time units it may use up to two years of to turn to the bandwidth or something that runs for a longer time like our control loop has 14,000 time units it's allowed to use 250 and if things are right you can you can see that you can combine those in your fourth gate that time the system the
whole point is the system enforces that something is not allowed to run over to suction and that way we can guarantee time to lower priority processes which is exactly what we need for these things critically system so and the way this is done is by being able to oral shielding context so in the case of our resource silver if they decline invokes the server it prizes among its rippling context the service and running on the time jiggling context and the server and gets charge of the client when to serve our finish its job to shim the context occurrence of Clyde and it now has server time charge through it and therefore we can prevents this client to advance the server and force something else or miss its deadline there's a paper what's in here is this last year and took a lot of this makes a zero for the first ever real time system with capabilities for time there's concurrent work at Washington George Washington University but there hasn't been a system like that before so the first time we integrated CPU time with a capability system the second thing I
want to talk about is what we call security enforcement my architecture and there's a start speed used on this Boeing helicopter the idea here is that
in SEO for backup a microkernels they have a very low-level interface a CEO for its particular table and then you need to deal with a lot of these objects and capabilities in order to do anything this here is a representation of the second most trivial example you can buy or even to an SEO for so the most trivial one would be a hello world program that just says hello world and then stops the most the second most pre-built thing is you have to process and they communicate by sending messages between a chess or represents this really trivial example we have over 50 kernel objects that we need to worry about and that's just for this trivial example this is a simple system but no
longer quite as trivial each point represents an object and the capability and you can see there's hundreds of thousands of that just for a relatively simple system so that's not a good abstraction level to reason about in the system so instead we have any component
middleware or anchors that's not particularly unique for example T know there's a in many ways much more general component middleware but can get some assurance story which you don't pick with others so in this case we have in this campus world we have components that are represented by boxes and connectors that are represented by lines between those boxes and there's three different types the end whether you have sickness message-passing semaphore like signaling or shared data and sort of the the top two boxes and the RPC clinic they between basically represents this second most trivial example I talked about before so much more high level representation and the beauty of this
and the spanker system is that we can provably reason about the system behavior on this angus representation and it takes corrective mapped onto SEO for so the way it is that oddness demonstrate that it's a business example this is a highly abstracted view of our UAV architecture and it has some untrusted stuff in a Linux virtual machine and the one of the core security
properties of the system is that Linux is only able to talk to the rest of the system by using encrypted traffic so only by the scripta library and we can do that by saying ok it's not connected to anything else in the system except this one line that goes to crypto therefore we know that if you can't if we can trust this crypto component then we can ensure that Linux and interfere with the rest of this so this is our highly simplified package view of the
system and in order to build the actual system of course we have implementations of this component store each of these boxes as a implementation of Stevie clean C so there's a driver multiple drivers the virtual machine etc and of course I get some compiler linked together what is missing here is the so-called glue code which is the operating system calls that enable these combinations so where do the message passing specifically and what this blue code needs to look like it's completely specified by this architecture view so we can generate this glue code which is a game that's not particularly returned so of any idea of compiling us it's been around for centuries but in our ok we have proved that the glucose sk generator is correct in the sense that if you invoke a compound a function in the component then this is semantically equivalent to just directly involving this this function in the same address space so that's sort of a very strong correctness property of the school code but we also think is from this canvas representation we can generate the low level SEO for representation so they in terms of SEO for objects and capabilities that's represented in a formalism called Cathy Ellicott capable of description language and again we generate this automatically from the canvas you and again this generation is provably correct and that means when we have the system in this this low level if this low level rivers diagram represents the actual ASL flow system then we know that we can reason about the system according to the styling of their diagram by this boxes and lives for at the center of campus campus all of us and the final step is how do we get the system in the state we also generate the initialization code that gets the system into that shape so we have a automatically generated code which is the English it passed in the system which will create all these objects distributed capabilities and then we know the system is in a state that's correctly represented by this anchors representation on top and that means we can now do all the reasoning above the properties of the system in this cactus operation for some limitations at the moment not all the proof stories are completely complete yet but this is ongoing work that's funded by another alpha program and it will be finished within the next year's then it will be very interesting there was an articulated communication of the ACM to start October that describes that and then there's also tools
where this fixed height or a formalism called architecture analysis and description language which is an international standard and that's used a lot in the avionics industry and there's a clip space tools etc which - and the home language is designed for doing safety cases and there's analysis tools and all those stuff and you can use that framework and generate the canvas levitate patient from that one although that generation is not going to be correct and it's unlikely to happen in near future when these tools are provided by Rockwell Collins they're all open source so that was the second thing that's sort of relevant we're still for in recent developments and the third one is okay
we have the verified kernel but of course the whole system is more than a
kernel even the trusted computing base of the system is much more than the kernel so typically you have some critical components there may be some devices you need to where you need to trust the drivers you may need to have a trusted file system you have so your control code etc and all these if they need to be trusted ideally they really should be very hard and of course 11 person years of most what we invested in verifying the kernel I'm all these components of the order of thousands or tens of thousands of lines of code and 11 person years for 10,000 lines of code and it stands when traffic lis that doesn't sound like a particular attractive way of doing things it was okay for the kernel but for doing things on top you own better productivity and this is where we developing the coaching
framework so coaching stands for covered include cogeneration and it is a language framework for building high assurance components on top of a co 4 and it is a programming language it's a functional programming language that's either memory safe but not managed and it's called a linear type system synchros it's very similar to rust in many ways because I like rust it's got a formally well defined semantics and we compile it into C which is not particular exciting but the more interesting part is when we compile it to see the compiler spits out proof that the C is correct against a component stake which the compiler also generates and then we know okay we have a correct implementation translation of this coachin into C which means that as long as we trust compile like this can reason about the correctness of our code at the level of the cultured semantics and we know that the seed translation will will maintain that semantics like the bus the language is restricted that you can't program everything at it it's it's intentionally to really complete so we need to complement it without start datatypes so these are things like force file systems we have abstract data types or the mainly red black trees and sympa and the idea is these need to be manually verified so in the end you have an overall high-level abstract specification of the complete functionality of this component you have these abstract data types which can be verified independently and your years they are highly reusable and then you're left manually verifying the culture code which is much easier than verifying C code because of the properties of Coaching language the fact that its type and memory safe that it's pretty functional and so that's the key for increasing the productivity of verification and we've done some case studies a number of file systems and there's a PayPal account that's about three years old now but that describes it and what we found is that okay
productivity stories not too bad so we get a possible of verified code in terms of dollars per line of code that's a power defect of two next thing will be what our cost is your form the copy verification story for SEO for was about three or four times as expensive as the earlier pistachio microkernel which was earlier l4 microkernel that was developed in a very similar common thanks by people the university folks who sort of had experience with microkernel settle so it's quite a comparable system so I say before with its complete verification was about the fact that for more expensive than this earlier system that had no verification story at all so that means if we get the cost down by effect of true we are competitive with non assurance traditional engineered code and it seems like with our coaching of college we already got half of that gap we got effect of two and the fact that the reason it's not more has a lot to do with the way potion the initial version of coaching was done it was very restrictive that you get forced to do a lot of fun boring repetitive stuff etc and this is what we're working on at the
moment and so the with the ultimate game of having something that really allows you to write systems components and verify them at a cost that's comparable to classical unverified C code so another interesting aspect is that ok when you have this coach and implementation presumably ideally you want to verify that but you can actually play a trade-off of dependability versus cost we could for example say ok it's safe language and therefore that reduces the number of bucks already significantly and maybe for something that's not ultra vehicle that might actually be enough and then you have you just need to write the code and your I've already code that you know it is going to be paid out that beaker but C code if it was making do it then only couldn't do automatic testing in particular this called property based listing which is something that comes out of the Haskell world where you have a formal specification of your functionality and it generates a cases automatically from that and in particularly the exercises the interesting bits so all the cases it simple and it has been turns out is a very effective tool for any code pretty much correct very quickly and of course you can do model checking and then finally you can do the full functional correctness proof by theorem proving as we done it with SEO for so there's a hierarchy of increasing insurance but also increasing costs that you can pick your point but one of the interesting aspects of that is that this poverty based testing has an interesting compatibility with our full functional corinthis groups in the sense that it uses it requires a formal specification and a formal specification can be reused with a full-frontal correctness proof so that means you can use a checking for properties space tasting for actually developing and loop up in your spec who specs head boxes what and it's much easy to verify against the correct stake than an e correct one because any anybody in the spec will send you down some red hole which you need to take out out for a while so starting with a more or less correct spec is a big win but also very fine correct code is much easier than verifying buggy code and so eliminating most of the box with quality based testing before you start verification also reduces cost so there's a whole bunch of trade-offs that can be played and this is all only at the beginning but we've already made a lot of progress in the last two years particular of the last year in increasing the expressiveness of the language to make it easier to use reduce the number of times of code you need to write for the implementing some functionality we're putting some of this oil like code int or syntactic sugar in the leg language and we are applying it to other components so in the past we use it for the many file systems we know starting to use Cochin for device drivers and network stacks and that's by the way all supported by industry funding so I'm happy to see that there's a fair amount of interest in industry for using this technology they've got one particular
application Ares autonomous cars nothing to do with DARPA it's a california-based company doing autonomous driving heads and they're working with us for using this coaching technology to get in some of their critical components verified so they have pretty crumby system with a for a v8 course that run the machine learning and sensor fusion and all that stuff and then they have and that's running in that SMP Linux and then underneath with this SEO for and then the critical components are cooled out running natively on their co 4 and with a minimal trusted computing base with the idea of verifying that trusted computing base in particular verified providing the privacy coaching they verified them and of course the system has redundancy as well so this is some of the I think really exciting developments that are have been happening around or happening around SEO for it's sort of I guess that may take away here is SEO for really is the cutting edge of operating system design and development so it's really driving innovation and there's more and more deployments that help us supporting real world cases and driving innovation through dot okay now so what many of you
folks are probably quite interested is sort of what's the story about the ecosystem and they generalize your whole community there's some good and some bad
news so the good news is the community is growing the available mailing list is very active there's heavy support from US government they set up a u.s. SEO for center of excellence which is basically an organization where companies can go and get help with developing systems on polyphagia for obesity DARPA the services or support particular offense work but it's not the only defense is an SEO for based system has gone through high assurance evaluation and be it's been certified for defenders and is actually in use in the UK and Australia defense but it's also to me particularly important aspect there is we're getting out of the just a defense space into our safety critical systems and this is reflected in the amount of commercial funding we get in for SEO for so this one companies some big some small some very big putting real dollar on the table to help us develop the SEO for open source system and the framework surrounded and pretty much all this work that we take funding for is open source work occasionally we would fight for example a propriety driver or for specific purpose for a customer but the the bulk of fee money that comes to us goes straight into developing the open source system SEO for itself as well as things that are on top and it's really into none of areas so there's some some of the companies there talking to our building things for because your control system to stop protect them from cyberattacks autonomous cars already mentioned and there's people building frameworks for eye assurance medical devices so a lot of safety critical systems work so that's a good news the bad news is
really the present state of the ecosystem which is not where I would really like to see it and I really thought this would develop faster at the moment the whole system is very tiny you have not a lot of actually usable components so unlike l 4e for example which has a fairly mature and rich ecosystem the SEO for one is still very much in its beginning the components around that people are way out but it's only documented how to find some of them are supported most and this is something we really need to change there's definitely a shortage of tools so we would like to see people developing more tools the Center of Excellence is doing some of that but we really like to see a open source community doing this and part of that is really because we are to blame for that we are community engaged in it's just insufficient we generally very responsive to people putting issues asking questions on the mailing list but we're not really practical and the main reason is not ill-will it's just we've been too busy with we've been always very stretched without people hiring really good kernel OS developers it's hard and we've been recruiting for years and with varying success just recently it's been pretty good we hired a number of people but basically just getting enough people in as a bottleneck and it's creative taking an egg problem right if you have if if we can make more views of the community then obviously that solves all of these problems but in order to bootstrap that we need to invest and engage with the community etcetera and which has been too busy in the past Buddha but that's really changing so this is a high priority thing for us we just over the last two months added two full-time OS engineers and a bunch of student panels and you will see in the next few months a real change there happening with the way we engage for the community and there's a it becoming more activity the CEO is of course one important bit of the community because they are their job is to contribute tools etc but we want to have a real sort of open source developer community around that and we both takes takes to help that developing much better and that includes of course on our side really just about documenting much more what's there and you said as a way to encourage community members such as adopt components and support them except by a continuance of course and part of that of course is keeping the developers contributors more visibility etcetera so we're working all that and we hope the suggestions and we're definitely taking steps to improving the transparency of the whole thing I'm it's been noted a few times that the whole SEO for development is not very transparent and that's unfortunately true but we're really changing that so once that we've already taken a few probably developer mailing list you would have seen that we started an RFC project process so in future any major changes will be going through this community consultation process and it's a way for the community obviously to engage as well and make suggests so that's already in place and a few other things that are not yet in place but we are working on them it is opening up our JIRA for working on platform issues that's a bit of a tricky one because there's lots of stuff in here from some of them 10 years old so the staff thing there is we first or eight projects that are online yes yeah my last fight so yeah so that needs some cleanup because there's confidential stuff in there and some stuff that could be embarrassing it's a plus so that will take a bit to get go through but it's happening we also created a discourse group which will be opened up very soon it already exists but it's not yet had but a non-sustainable will announce it open in the next month or so and there is a public road map or this horribly outdated about about three years we'll update that and be more active in mechanicus so please talk to us if you interested and we really want engaging with the community much better in the future that we have the house and it's
the last I think if then let me punish al so I can hopefully see
yeah okay I got that 3500 it's not our space right we are software experience on Hardware experts obviously hardware is the thing that keeps me alive at night awake at night I we understand how the mix of persevere we don't we can't be no control of the hardware and we know the hard ways that there's a lot of activities happening in that space or take me around risk five which of course the open architecture encourages that and there is so probably three or four objects around the world that are working on verifying risk five processor implementations which is really exciting but it will take a while to get there but yeah I mean you're totally right harvester the big problem and for example stick that nail down demonstrate so overthink this hardware it's done so I hope people really get the activate on the hardware side if there's any more questions saying email
[Applause]
Loading...
Feedback

Timings

  400 ms - page object

Version

AV-Portal 3.20.2 (36f6df173ce4850b467c9cb7af359cf1cdaed247)
hidden