Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Galois Tech Talk: Non-interference and Binary Correctness of seL4</h1> <div class='date'><time class="dtstart dt-start" title="2013-06-14T11:00:00" datetime="2013-06-14T11:00:00">Friday, June 14, 2013 from 11am</time>–<time class="dtend dt-end" title="2013-06-14T12:00:00" datetime="2013-06-14T12:00:00">noon</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202390439'><span class='fn org p-name'>Galois, Inc</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">421 SW 6th Ave. Suite 300</div> <span class="locality p-locality">Portland</span> , <span class="region p-region">OR</span> <span class="postal-code p-postal-code">97204</span> <div class="country-name p-country-name">US</div> (<a href='https://maps.google.com/maps?q=421%20SW%206th%20Ave.%20Suite%20300,%20Portland%20OR%2097204%20US'>map</a>) </div> </div> <div class="description p-description"> <p>Presented by Gerwin Klein and Thomas Sewell.</p> <p>This talk introduces two new facets that have recently been added to the seL4 formal verification story: a proof the kernel does not leak information between domains, and a proof that the compiled binary matches the expected semantics of the C source code.</p> <p>The first part of the talk presents a new non-interference theorem for seL4, which builds on the earlier function correctness verification. The theorem shows how seL4 can be configured as a static separation kernel with dynamic kernel services within each domain.</p> <p>The binary proof addresses the compiler-correctness assumption of the earlier seL4 proofs by connecting the compiled binary to the refinement chain, thus showing that the seL4 binary used in practice has all of the properties that have been shown of its models. We use the Cambridge ARM model and Magnus Myreen's certifying decompiler, together with a custom correspondence finder for assembly-like programs powered by modern SMT solvers. We cover the previously-verified parts of seL4 as compiled by gcc (4.5.1) at optimisation level 1.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://corp.galois.com/blog/2013/6/6/tech-talk-non-interference-and-binary-correctness-of-sel4.html">Website</a></li> </ul> </div>