BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Decoding Nets: A Formal Take on Address Translation - Ben Fiedler\
 , ETH
DTSTART:20220728T150000Z
DTEND:20220728T160000Z
UID:TALK177266@talks.cam.ac.uk
CONTACT:Jamie Vicary
DESCRIPTION:Modern computing hardware is enormously complicated: a single 
 memory request\ntraverses multiple hardware translation and caching steps 
 until it reaches its\nintended destination\, which often appears at differ
 ent physical addresses\nfor different requesters.\n\nCorrectly capturing t
 he complexity of this process is essential for correct\nsystem operation a
 nd system verification. We introduce decoding nets\, a formal\ndescription
  for memory and interrupt systems\, which we have successfully used in\npr
 actice for page table generation\, memory management and interrupt control
 ler\nconfiguration.\n\nFurthermore\, we are actively using them to verify 
 isolation guarantees of the\nARM confidential compute architecture.
LOCATION:FW26
END:VEVENT
END:VCALENDAR