SPLASH 2022 (series) / Doctoral Symposium / Proving Obliviousness of Probabilistic Algorithms with Formal Verification
Proving Obliviousness of Probabilistic Algorithms with Formal VerificationIn Person
Tue 6 Dec 2022 11:30 - 12:00 at Seminar Room G145 - Morning Session B
Obliviousness is a security feature to protect sensitive information from an algorithm’s observable behaviours. For better run-time performance, many oblivious algorithms published recently are probabilistic instead of deterministic, but this also brings difficulties to reason about them. We introduce some challenges, works and further ideas in this paper, including the concrete contribution of extending PSL for verifying one of the random oblivious algorithms. We also present my further PhD research plan on this topic.
Tue 6 DecDisplayed time zone: Auckland, Wellington change
Tue 6 Dec
Displayed time zone: Auckland, Wellington change
10:30 - 12:00 | |||
10:30 30mTalk | Towards a Verified Cost Model for Call-by-Push-ValueIn Person Doctoral Symposium Zhuo Chen University of Melbourne DOI | ||
11:00 30mTalk | Formally Verified Resource Bounds through Implicit Computational ComplexityIn Person Doctoral Symposium Neea Rusch Augusta University DOI | ||
11:30 30mTalk | Proving Obliviousness of Probabilistic Algorithms with Formal VerificationIn Person Doctoral Symposium Pengbo Yan University of Melbourne DOI |