Towards Formally Verified Path ORAM in Coq (CoqPL 2023 - The Ninth International Workshop on Coq for Programming Languages)

Sun 15 - Sat 21 January 2023 Boston, Massachusetts, United States

Who

Hannah Leung, Talia Ringer, Christopher W. Fletcher

Track

CoqPL 2023

Time Zone

The program is currently displayed in (GMT-05:00) Eastern Time (US & Canada).

Use conference time zone: (GMT-05:00) Eastern Time (US & Canada)Select other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Sat 21 Jan 2023 12:00 - 12:30 at Scollay - Session 2

Abstract

Oblivious RAM is a class of randomized algorithms that break the association between a program’s memory access pattern and that program’s data. Path Oblivious RAM is a specific ORAM algorithm that is both theoretically interesting and practically efficient. This abstract describes our plans to verify Path ORAM in Coq, and discusses the design decisions and tradeoffs involved.

File attachments

Extended abstract (Towards_Formally_Verified_Path_ORAM__in_Coq_camera_ready.pdf)	246KiB

Hannah Leung

University of Illinois Urbana-Champaign

United States

Talia Ringer

University of Illinois at Urbana-Champaign