|
Change #2986
2010-05-21
14:45:58
|
create
Calagator::Event
1250458706
Galois Tech Talk: The L4.verified Project
Roll back
| description |
nil |
→ |
The L4.verified Project
Presented by Dr. Gerwin Klein.
Last year, the NICTA L4.verifed project produced a formal machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This talk will give an overview of the proof together with its main implications and assumptions, and will show in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security. |
| end_time |
nil |
→ |
2010-05-24 11:30:00 -0700 |
| id |
nil |
→ |
1250458706 |
| start_time |
nil |
→ |
2010-05-24 10:30:00 -0700 |
| title |
nil |
→ |
Galois Tech Talk: The L4.verified Project |
| url |
nil |
→ |
http://www.galois.com/blog/2010/05/21/tech-talk-the-l4-verified-project/ |
| venue_id |
nil |
→ |
202390439 |
|