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:20140309T020000 RDATE:20140309T020000 TZOFFSETFROM:-0800 TZOFFSETTO:-0700 TZNAME:PDT END:DAYLIGHT END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140819T231559Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140822T120000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140822T110000 DTSTAMP;VALUE=DATE-TIME:20140819T231559Z LAST-MODIFIED;VALUE=DATE-TIME:20140819T231559Z UID:http://calagator.org/events/1250466862 DESCRIPTION:Galois is pleased to host the following tech talk. These talk s are free and open to the interested public--please join us! (There is no need to pre-register for the talk.) \;\n \;\n### Abstract ###&# 13\;\n \;\nEasyCrypt is a computer-assisted framework for proving the security of cryptographic constructions. However\, there is a significa nt 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 ong oing disaster areas in security. We have recently extended EasyCrypt wit h support for reasoning about C implementations\, and exploited the Comp Cert verified compiler to carry the security proof to executable code. Moreover\, we have developed verified type-based information flow analys es on assembly code to ensure that executable code is protected against cache-based side-channel attacks. \;\n \;\n### Bio ### \;\n \;\nGilles Barthe received a Ph.D. in Mathematics from the University of Manchester\, UK\, in 1993\, and an Habilitation à diriger les recherche s 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 Universit y 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 investigat or of many national and European projects\, and served as the scientific coordinator of the FP6 FET integrated project “MOBIUS: Mobility\, Ubiqu ity and Security” for enabling proof-carrying code for Java on mobile de vices (2005-2009). He has been a PC member of many conferences (CSF\, ES ORICS\, FM\, ICALP\, ITP…)\, and served as PC (co-)chair of VMCAI’10\, E SOP’11\, FAST’11\, and SEFM’11. He is a member of the editorial board of the Journal of Automated Reasoning. \;\n \;\nHis research interes ts include formal methods\, programming languages and program verificati on\, software and system security\, and cryptography\, and foundations o f mathematics and computer science.\n\nTags: formal-methods\, cryptograp hy\, verification\n\nImported from: http://calagator.org/events/12504668 62 URL:http://galois.com/blog/2014/08/tech-talk-verified-cryptographic-imple mentations/ SUMMARY:Tech Talk: Verified Cryptographic Implementations LOCATION:Galois\, Inc. Auxiliary Meeting Room: 421 SW 6th Ave\, 11th Floo r\, Portland OR 97204 US SEQUENCE:2 END:VEVENT BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20140820T175334Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140828T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140828T103000 DTSTAMP;VALUE=DATE-TIME:20140820T175334Z LAST-MODIFIED;VALUE=DATE-TIME:20140820T175334Z UID:http://calagator.org/events/1250466868 DESCRIPTION:Galois is pleased to host the following tech talk. These talk s are free and open to the interested public--please join us! (There is no need to pre-register for the talk.) \;\n \;\n### Abstract ###&# 13\;\n \;\nQuickCheck is a powerful library for automatic test-case g eneration. Because QuickCheck performs random testing\, some of the coun terexamples discovered are very large. QuickCheck provides an interface for the user to write shrink functions to attempt to reduce the size of counterexamples. Hand-written implementations of shrink can be complex\, inefficient\, and consist of significant boilerplate code. Furthermore\ , shrinking is only one aspect in debugging: counterexample generalizati on is the process of extrapolating from individual counterexamples to a class of counterexamples\, often requiring a flash of insight from the p rogrammer. To improve counterexample reduction and generalization\, we i ntroduce SmartCheck. SmartCheck is a debugging tool that reduces algebra ic data using generic search heuristics to efficiently find smaller coun terexamples. In addition to shrinking\, SmartCheck also automatically ge neralizes counterexamples to formulas representing classes of counterexa mples. SmartCheck has been implemented for Haskell and is freely availab le. \;\n \;\n### Bio ### \;\n \;\nLee Pike manages the Cyber -Physical Systems program at Galois\, a company specializing in software -intensive critical systems. He has been the Principal Investigator on a pproximately $10 million of R&\;D projects funded by NASA\, DARPA\, a nd other federal agencies. His research focuses on applying techniques f rom functional programming\, run-time verification\, and formal verifica tion to the areas of operating systems\, compilers\, cryptographic syste ms\, avionics\, and control systems. Previously\, he was a research scie ntist in the NASA Langley Formal Methods Group and has a Ph.D. in Comput er Science from Indiana University.\n\nTags: functional-programming\, te sting\n\nImported from: http://calagator.org/events/1250466868 URL:http://galois.com/blog/2014/08/tech-talk-smartcheck-automatic-efficie nt-counterexample-reduction-generalization/ SUMMARY:Tech Talk: SmartCheck – Automatic and Efficient Counterexample Re duction and Generalization LOCATION:Galois\, Inc. Auxiliary Meeting Room: 421 SW 6th Ave\, 11th Floo r\, Portland OR 97204 US SEQUENCE:2 END:VEVENT END:VCALENDAR