۲۲۰۱۵پ
per
تحلیل کمی جریان اطلاعات امن در برنامه های کامپیوتری
Quantitative Analysis of Secure Information Flow in Computer Programs
/خیام صالحی قهفرخی
: علوم ریاضی
، ۱۳۹۸
، راشدی
۱۴۲ص
چاپی - الکترونیکی
دکتری
علوم کامپیوتر
۱۳۹۸/۰۶/۱۴
تبریز
سامانه‌های نرم‌افزاری امروزه جزئی جدانشدنی از زندگی روزمره هستند .یکی از مهم‌ترین دغدغه‌های سامانه‌های نرم‌افزاری حفظ محرمانگی داده‌های محرمانه و جلوگیری از نشت آن‌ها است .استنتاج داده‌های محرمانه از روی داده‌های قابل مشاهده به‌دست مهاجم نشت اطلاعات نامیده می‌شود .رویکردهای مختلفی جهت جلوگیری از نشت اطلاعات ارائه شده است .از جمله این رویکردها می‌توان به تحلیل کمی جریان اطلاعات امن اشاره کرد که میزان نشت اطلاعات را محاسبه می‌کند .مهاجم از روی متغیرهای عمومی سعی در حدس متغیرهای محرمانه در برنامه‌های کامپیوتری دارد .به‌دلیل کاربرد زیاد برنامه‌های احتمالاتی همروند، نشت اطلاعاتی آنان بسیار دارای اهمیت است .در این برنامه‌ها نشت در حالت‌های میانی برای مقادیر عمومی و نیز اثر زمان‌بند خاص به‌دست مهاجم بایستی درنظرگرفته می‌شود .روش‌های زیادی جهت تحلیل کمی جریان اطلاعات ارائه شده است .بیشتر این روش‌ها مناسب تحلیل برنامه‌های همروند نیستند و نشت را در حالت‌های میانی درنظرنمی‌گیرند .همچنین به‌طور خودکار قابل به‌کارگیری نبوده و نیاز به خبرگی است .در این رساله، دو راهکار جهت تحلیل کمی جریان اطلاعات از متغیرهای محرمانه به متغیرهای عمومی برنامه‌های احتمالاتی همروند پیشنهاد می‌شوند .این دو راهکار خودکار هستند و نشت در حالت‌های میانی و اثر زمان‌بند خاص را درنظرمی‌گیرند .در این دو راهکار، برنامه‌های احتمالاتی همروند نوشته‌شده در زبان PRISM به مدل‌های مارکوف ترجمه می‌شوند .در راهکار اول، دید مهاجم از برنامه با معرفی رابطه شبیه‌سازی هم‌پای پس‌رو به‌دست می‌آید .دو الگوریتم پالایش افراز جهت به‌کارگیری رابطه گفته‌شده ارائه می‌شوند تا زنجیره مارکوف خارج‌قسمت به‌دست آید .از روی زنجیره مارکوف حاصل روشی برای محاسبه امید ریاضی نشت پیشنهاد می‌گردد .به‌منظور بررسی کارایی راهکار پیشنهادی، دو پروتکل گمنامی مشهور) شام رمزنگاران و رای‌دهی (به‌عنوان مطالعه موردی تحلیل می‌شوند .سپس راهکار پیشنهادی با ابزارهای موجود تحلیل نشت هم به‌صورت کیفی و هم کمی مقایسه می‌گردد .در راهکار دوم ظرفیت کانال برنامه‌های احتمالاتی همروند برمبنای نشت بیشینه و امید ریاضی نشت معرفی می‌شود .ظرفیت کانال برابر بیشترین میزان نشت روی همه مهاجم‌ها با قدرت مشاهداتی یکسان اما با دانش متفاوت روی متغیرهای محرمانه است .محاسبه ظرفیت کانال به یک مساله بهینه‌سازی غیرخطی مقید کاهش می‌یابد .به‌دلیل پیچیدگی زیاد تابع هدف مساله بهینه‌سازی و نیز نبود الزام به تقعر تابع هدف، روش‌های ریاضیاتی ازجمله ضرایب لاگرانژ و شرایط KKT قابل استفاده نیستند .به‌همین‌منظور رویکردی تکاملی برای محاسبه ظرفیت کانال ارائه می‌شود .تا جایی که می‌دانیم، این اولین کار در کاربرد الگوریتم‌های تکاملی در تحلیل کمی جریان اطلاعات امن است .جهت نشان‌دادن کاربردپذیری راهکار پیشنهادی، ظرفیت کانال دو پروتکل شام رمزنگاران و رای‌دهی محاسبه می‌شود .درادامه روش محاسبه مستقیم ظرفیت کانال پروتکل رای‌دهی فرموله‌بندی می‌شود .درنهایت، با استفاده از آزمون تی‌تست پایداری نتایج تایید می‌گردد .راهکارهای پیشنهادی در این رساله در ابزارLeak - PRISMپیاده‌سازی شده است
Software systems are an inevitable part of people's everyday life. One of the most important challenges in these systems is to preserve the confidentiality of secret data and to prevent leakage of them. Leakage is referred to the act of inferring secret data from publicly-observable data by the attacker. There are various mechanisms to avoid information leakages. Quantitative information flow is a rigorous mechanism to compute the information leaked. In this mechanism, the attacker tries to guess secret values from public ones. Due to the high applicability of concurrent probabilistic programs, quantifying leakage of them is of vital importance. In these programs, the analysis should consider leakage in intermediate state of public values and effect of scheduler. Many methods have been presented for quantitative information flow analysis. However, most of these methods are not suitable for analyzing concurrent programs, as they do not consider leakage in intermediate state and are not fully-automated. In this thesis, two approaches are proposed for quantitative analysis of information flow in concurrent probabilistic programs. These two approaches are fully-automated and consider leakage in intermediate state and scheduler effects. They model concurrent programs written in the PRISM language using Markovian processes. In the first approach, a back-bisimulation equivalence is proposed to capture the attacker's view of the program behavior. Two partition refinement algorithms are developed to construct the back-bisimulation quotient of the program model and then a quantification method is given for computing the information leakage using the quotient. Then, two common anonymity protocols, dining cryptographers and voting protocol, are analyzed as case studies to show the applicability of the approach. It is compared, qualitatively and quantitatively, with other available leakage analysis tools. In the second approach, channel capacity of concurrent probabilistic programs is computed. Channel capacity is the maximum amount of leakage over all attackers with the same observational power but different knowledge on the secret. In this approach, two notions of capacity are defined for concurrent probabilistic programs using information theory. These definitions consider intermediate leakage and scheduler effect. Computing these capacities are a constrained non-linear optimization problem. The objective function in the optimization problem is highly complex and concavity of it is not necessarily satisfied. Therefore, it is not possible to use well-known mathematical techniques such as Lagrange multipliers and KKT conditions. In this research, an evolutionary algorithm is proposed to compute the capacities. The voting and the dining cryptographers protocols are analyzed as case studies to show how the proposed approach can automatically compute the capacities. We also formulate the capacities of the voting protocol. To the best of our knowledge, this is the first work in quantitative information flow that uses an evolutionary algorithm to compute the channel capacity and the first work that measures channel capacity for the voting protocol. Finally, a T-test is performed to validate the stability of results produced by multiple runs of the evolutionary algorithm. Both proposed approaches have been implemented in a leakage quantification tool PRISIM-Leak, which is built on PRISM, a probabilistic model checker
Quantitative Analysis of Secure Information Flow in Computer Programs
صالحی قهفرخی، خیام
Salehi, Khayyam
کریم‌پورینگجه، جابر، استاد راهنما
عیسی زاده، آیاز، استاد راهنما
ایزدخواه، حبیب، استاد مشاور
سیاه و سفید
نمایه‌سازی قبلی
