تقرير
Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms (Extended Version)
العنوان: | Combining Classical and Probabilistic Independence Reasoning to Verify the Security of Oblivious Algorithms (Extended Version) |
---|---|
المؤلفون: | Yan, Pengbo, Murray, Toby, Ohrimenko, Olga, Pham, Van-Thuan, Sison, Robert |
سنة النشر: | 2024 |
المجموعة: | Computer Science |
مصطلحات موضوعية: | Computer Science - Programming Languages |
الوصف: | We consider the problem of how to verify the security of probabilistic oblivious algorithms formally and systematically. Unfortunately, prior program logics fail to support a number of complexities that feature in the semantics and invariant needed to verify the security of many practical probabilistic oblivious algorithms. We propose an approach based on reasoning over perfectly oblivious approximations, using a program logic that combines both classical Hoare logic reasoning and probabilistic independence reasoning to support all the needed features. We formalise and prove our new logic sound in Isabelle/HOL and apply our approach to formally verify the security of several challenging case studies beyond the reach of prior methods for proving obliviousness. |
نوع الوثيقة: | Working Paper |
URL الوصول: | http://arxiv.org/abs/2407.00514 |
رقم الأكسشن: | edsarx.2407.00514 |
قاعدة البيانات: | arXiv |
كن أول من يترك تعليقا!