Export to

• Google Calendar
• iCalendar file
• hCalendar markup
  <div class="vevent h-event"> <h1 class="summary p-name">Tech Talk: Verified Cryptographic Implementations</h1> <div class='date'><time class="dtstart dt-start" title="2014-08-22T11:00:00" datetime="2014-08-22T11:00:00">Friday, August 22, 2014 from 11am</time>–<time class="dtend dt-end" title="2014-08-22T12:00:00" datetime="2014-08-22T12:00:00">noon</time></div> <div class="location vcard p-location h-card"> <a class="url" href='http://calagator.org/venues/202394616'><span class='fn org p-name'>Galois, Inc. Auxiliary Meeting Room</span></a> <div class="adr p-adr h-adr"> <div class="street-address p-street-address">421 SW 6th Ave, 11th Floor</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,%2011th%20Floor,%20Portland%20OR%2097204%20US'>map</a>) </div> </div> <div class="description p-description"> <p>Galois is pleased to host the following tech talk. These talks are free and open to the interested public--please join us! (There is no need to pre-register for the talk.)</p> <h3>Abstract</h3> <p>EasyCrypt is a computer-assisted framework for proving the security of cryptographic constructions. However, there is a significant gap between security proofs done in the usual provable security style and cryptographic implementations used in practice; as a consequence, real-world cryptography is sometimes considered as “one of the many ongoing disaster areas in security. We have recently extended EasyCrypt with support for reasoning about C implementations, and exploited the CompCert verified compiler to carry the security proof to executable code. Moreover, we have developed verified type-based information flow analyses on assembly code to ensure that executable code is protected against cache-based side-channel attacks.</p> <h3>Bio</h3> <p>Gilles Barthe received a Ph.D. in Mathematics from the University of Manchester, UK, in 1993, and an Habilitation à diriger les recherches in Computer Science from the University of Nice, France, in 2004. He joined the IMDEA Software Institute in April 2008. Previously, he was head of the Everest team on formal methods and security at INRIA Sophia-Antipolis Méditerranée, France. He also held positions at the University of Minho, Portugal; Chalmers University, Sweden; CWI, Netherlands; University of Nijmegen, Netherlands. He has published more than 100 refereed scientific papers. He has been coordinator/principal investigator of many national and European projects, and served as the scientific coordinator of the FP6 FET integrated project “MOBIUS: Mobility, Ubiquity and Security” for enabling proof-carrying code for Java on mobile devices (2005-2009). He has been a PC member of many conferences (CSF, ESORICS, FM, ICALP, ITP…), and served as PC (co-)chair of VMCAI’10, ESOP’11, FAST’11, and SEFM’11. He is a member of the editorial board of the Journal of Automated Reasoning.</p> <p>His research interests include formal methods, programming languages and program verification, software and system security, and cryptography, and foundations of mathematics and computer science.</p> </div> <h3>Links</h3> <ul> <li><a class="url u-url" href="http://galois.com/blog/2014/08/tech-talk-verified-cryptographic-implementations/">Website</a></li> </ul> </div>