10575

10575

درستي‌يابي امنيتي برنامه‌هاي همروند از طريق بررسي مدل بدون حالت كد

كارشناسي ارشد

كامپيوتر- گرايش نرم‌افزار (سيستم‌هاي توزيعي)

مهر ماه 1391

مهر ماه 1391

دكتر محمد عبداللهي ازگمي

بررسي مدل بدون حالت يك فن مؤثر براي درستي‌يابي برنامه‌هاي بزرگ و پيچيده است كه از لحاظ كاربردپذيري نسبت به بررسي مدل حالت كامل، براي دنياي نرم‌افزار مناسب‌تر است. بررسي مدل بدون حالت كد يك گرايش جديد در بررسي مدل است كه به جاي تفسير و اجراي مدل توصيف شده از روي برنامه، كد برنامه را در محيط اجراي واقعي زبان برنامه‌نويسي درستي‌يابي مي‌كند. در اين پايان‌نامه يك ابزار توزيع‌شده و موازي براي درستي‌يابي كدهاي زبان‌هاي برنامه‌نويسي با استفاده از فن بررسي مدل بدون حالت طراحي و پياده‌سازي شده است. توجه ما به طور خاص معطوف به درستي‌يابي خصوصيات امنيتي برنامه‌هاي همروند (چندنخي) بوده است. از اين رو ابزار طراحي شده به صورت خودكار قادر به شناسايي بن‌بست، قفل زنده، شرايط مسابقه، نقض ادعا و درستي‌يابي امنيت جريان اطلاعات است. از طرف ديگر اين ابزار قادر به درستي‌يابي فرمول‌هاي منطق زماني خطي (LTL) نيز هست. نوآوري‌هاي اين پايان‌نامه در دو حوزه است. نخست، الگوريتم‌هايي طراحي شده‌اند كه توسط آنها براي اولين بار قادر شده‌ايم كه فرمول‌هاي LTL را در بررسي مدل بدون حالت درستي‌يابي كنيم. دوم، ما براي اولين بار با استفاده از بررسي مدل بدون حالت كد، درستي‌يابي خصوصيت امنيت جريان اطلاعات را انجام داده‌ايم. با روشي كه ارائه شده است، ما براي اولين بار، قادر به درستي‌يابي عملي جديدترين تعريف ارائه شده از عدم مداخله در برنامه‌هاي همروند هستيم. يك نمونه اوليه از يك ابزار را با زبان اِرلنگ براي درستي‌يابي برنامه‌هاي نوشته ‌شده به زبان C و كتابخانه چندنخي POSIX پياده‌سازي نموده‌ايم. ابزار با استفاده از مثال‌هايي آزمون شده و الگوريتم‌ها و مؤلفه‌هاي آن نيز ارزيابي و از طريق فن بررسي مدل به‌طور صوري درستي‌يابي شده‌اند. واژه‌هاي كليدي: بررسي مدل كد، بررسي مدل بدون حالت، درستي‌يابي برنامه‌هاي همروند، درستي‌يابي خصوصيات امنيتي.