BEGIN:VCALENDAR
METHOD:REQUEST
PRODID:Microsoft Exchange Server 2010
VERSION:2.0
BEGIN:VTIMEZONE
TZID:Pacific Standard Time
BEGIN:STANDARD
DTSTART:16010101T020000
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
RRULE:FREQ=YEARLY;INTERVAL=1;BYDAY=1SU;BYMONTH=11
END:STANDARD
BEGIN:DAYLIGHT
DTSTART:16010101T020000
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
RRULE:FREQ=YEARLY;INTERVAL=1;BYDAY=2SU;BYMONTH=3
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
ORGANIZER;CN=Nikhil Swamy:mailto:nswamy@microsoft.com
ATTENDEE;ROLE=REQ-PARTICIPANT;PARTSTAT=NEEDS-ACTION;RSVP=TRUE;CN=fstar-mail
 ing-list@googlegroups.com:mailto:fstar-mailing-list@googlegroups.com
DESCRIPTION;LANGUAGE=en-US:https://fstar-lang.org/popup/seminar.html\n\n\nJ
 oin online on Zoom: https://cmu.zoom.us/j/97804414550?pwd=Q3NQWjRxNWwwYnVL
 SDVSMllmb01jQT09\n\n\nModular Verification of Non-Leakage for Hardware Sec
 urity Modules with K2\n\n\nSpeaker: Anish Athalye https://anish.io/\n\n\nK
 2 is a framework for proving that an implementation of a hardware security
  module (HSM) leaks nothing more than what is mandated by its functional s
 pecification. K2's proof covers the software and the hardware of an HSM\, 
 which enables it to catch all bugs above the cycle-level digital circuit a
 bstraction\, including timing side channels. K2's key contribution is a no
 vel approach to proving non-leakage in a modular fashion\, using transitiv
 e information-preserving refinement. This enables K2 to use different tech
 niques for verifying different layers (software and hardware)\, reuse exis
 ting verified components\, and largely automate several parts of the proof
 \, while still providing a single top-to-bottom combined theorem. We use K
 2 to develop several HSMs\, including an ECDSA certificate-signing HSM and
  a password-hashing HSM\, on top of the OpenTitan Ibex and PicoRV32 proces
 sors. K2 provides a strong guarantee for these HSMs\; for instance\, it pr
 oves that the ECDSA-on-Ibex HSM implementation (2\,300 lines of code and 1
 3\,500 lines of Verilog) leaks nothing more than what is allowed by a 50-l
 ine specification of its behavior.\n\n
UID:040000008200E00074C5B7101A82E008000000003DD6722CB9B7DA01000000000000000
 010000000D40F41BD61D8FC4498857A2D42A6AD53
SUMMARY;LANGUAGE=en-US:F* PoP Up Seminar: Anish Athalye on K2
DTSTART;TZID=Pacific Standard Time:20240627T080000
DTEND;TZID=Pacific Standard Time:20240627T090000
CLASS:PUBLIC
PRIORITY:5
DTSTAMP:20240606T022811Z
TRANSP:OPAQUE
STATUS:CONFIRMED
SEQUENCE:0
LOCATION;LANGUAGE=en-US:
X-MICROSOFT-CDO-APPT-SEQUENCE:0
X-MICROSOFT-CDO-OWNERAPPTID:2122722109
X-MICROSOFT-CDO-BUSYSTATUS:TENTATIVE
X-MICROSOFT-CDO-INTENDEDSTATUS:BUSY
X-MICROSOFT-CDO-ALLDAYEVENT:FALSE
X-MICROSOFT-CDO-IMPORTANCE:1
X-MICROSOFT-CDO-INSTTYPE:0
X-MICROSOFT-DONOTFORWARDMEETING:FALSE
X-MICROSOFT-DISALLOW-COUNTER:FALSE
X-MICROSOFT-REQUESTEDATTENDANCEMODE:DEFAULT
X-MICROSOFT-ISRESPONSEREQUESTED:TRUE
X-MICROSOFT-LOCATIONS:[]
BEGIN:VALARM
DESCRIPTION:REMINDER
TRIGGER;RELATED=START:-PT15M
ACTION:DISPLAY
END:VALARM
END:VEVENT
END:VCALENDAR