BEGIN:VCALENDAR PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN CALSCALE:GREGORIAN X-WR-CALNAME:Calagator METHOD:PUBLISH VERSION:2.0 BEGIN:VTIMEZONE TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles BEGIN:DAYLIGHT DTSTART:20120311T020000 RDATE:20120311T020000 RDATE:20130310T020000 TZOFFSETFROM:-0800 TZOFFSETTO:-0700 TZNAME:PDT END:DAYLIGHT BEGIN:STANDARD DTSTART:20121104T020000 RDATE:20121104T020000 TZOFFSETFROM:-0700 TZOFFSETTO:-0800 TZNAME:PST END:STANDARD END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20121009T165835Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20121016T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20121016T103000 DTSTAMP;VALUE=DATE-TIME:20121009T165835Z LAST-MODIFIED;VALUE=DATE-TIME:20121009T165835Z UID:http://calagator.org/events/1250462942 DESCRIPTION:Presented by Matthew Fernandez. \;\n \;\nIn safety- and security-critical environments software failures that are acceptable in other contexts may have expensive or even life-threatening consequences . Formal verification has the potential to provide high assurance for th is software\, but is regarded as being prohibitively expensive. Although significant advances have been made in this area\, verification of larg er systems still remains impractical. Component-based development has th e potential to lower the cost of system-wide verification\, bringing cor rectness proofs of these large scale systems within reach. This talk wil l discuss my work that aims to provide a component-based development env ironment for building systems with high assurance requirements. By provi ding a formal model of the platform with proven correctness properties t hat hold at the level of an abstract model right down to the implementat ion\, I hope to reduce the cost of full system verification by allowing reasoning about system components in isolation. \;\n\n\nTags: galois\ , formal methods\, tech talk\, l4\, OS design\, kernels\n\nImported from : http://calagator.org/events/1250462942 URL:https://corp.galois.com/blog/2012/10/9/tech-talk-towards-a-formally-v erified-component-platform.html SUMMARY:Galois Tech Talk: Towards a Formally Verified Component Platform LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20130607T010656Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130614T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130614T110000 DTSTAMP;VALUE=DATE-TIME:20130607T010656Z LAST-MODIFIED;VALUE=DATE-TIME:20130607T010656Z UID:http://calagator.org/events/1250464379 DESCRIPTION:Presented by Gerwin Klein and Thomas Sewell. \;\n \;\nT his talk introduces two new facets that have recently been added to the seL4 formal verification story: a proof the kernel does not leak informa tion between domains\, and a proof that the compiled binary matches the expected semantics of the C source code. \;\n \;\nThe first part o f the talk presents a new non-interference theorem for seL4\, which buil ds on the earlier function correctness verification. The theorem shows h ow seL4 can be configured as a static separation kernel with dynamic ker nel services within each domain. \;\n \;\nThe binary proof address es the compiler-correctness assumption of the earlier seL4 proofs by con necting the compiled binary to the refinement chain\, thus showing that the seL4 binary used in practice has all of the properties that have bee n shown of its models. We use the Cambridge ARM model and Magnus Myreen' s certifying decompiler\, together with a custom correspondence finder f or assembly-like programs powered by modern SMT solvers. We cover the pr eviously-verified parts of seL4 as compiled by gcc (4.5.1) at optimisati on level 1.\n\nTags: galois\, formal methods\, tech talk\, kernels\n\nIm ported from: http://calagator.org/events/1250464379 URL:http://corp.galois.com/blog/2013/6/6/tech-talk-non-interference-and-b inary-correctness-of-sel4.html SUMMARY:Galois Tech Talk: Non-interference and Binary Correctness of seL4 LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR