چکیده فارسی :

امنیت در اكثر مبادلات مورد پذیرش جهان وب قرار گرفته است بخصوص از زمانیكه آسیب پذیر های قابل استخراج از راه دور را به باگهای برنامه كاربردی وب نسبت می دهد. اكثر برنامه های بررسی، آسیب پذیرهای از قبل ناشناحته در برنامه های C به ارث رسیده را كشف می كند، و این امید را افزایش می دهند كه با برنامه های كاربردی وب می توانند به موفقیت مشابهی دست یابند. در این مقاله، ما روش كلی و بی نقصی را در جخت تضمین امنیت برنامه كاربردی توصیف می نماییم. با ملاحظه آسیب پذیرهای برنامه كاربردی وب به صورت مسئله جریان اطلاعاتی ایمن،‌ ما الگوریتم تحلیل ایستا براساس شبكه را ایجاد نمودیم كه حاصل سیستم های نوع و قالب بندی نوع است و نقصی آنرا بیان می كند. در طول تحلیل،‌ بخشهای كدی كه آسیب پذیر می باشند به محافظه های زمان اجرا مجهز می شوند، بنابراین در غیاب دخالت كاربر از برنامه های كاربردی وب حفاظت می كنند. با توجه خاص نمودن به برنامه های اجرا برنامه، سربار زمان اجرا به صفر كاهش می یابد. همچنین ما ابزاری به نام Web SSARI را ایجاد نمودیم تا الگوریتم را تست نماییم و از آن جهت بررسی 230 برنامه كاربردی وب اُپن سورس بر روی SourceForge.net استفاده نمودیم كه جهت نمایش پژوهشهایی بامقیاس، معروفیت و تكامل متفاوت انتخاب شده اند. 69 برنامه درگیر آسیب پذیریهایی بودند و تنظیم كننده های آنها اخطار داده شد. 38 پروژه یافته های ما را تصدیق نمودند و طرح هایشان را برای ارائه پیچ ها بیان نمودند. آمارما نشان دهنده این مطلب است كه تحلیل ایستا باعث كاهش سربار در زمان اجرا و تا 4/98% شده است.

طبقات و توصیفگران موضوع:

D.2.4 [مهندسی نرم افزار]: بررسی برنامه/نرم افزار- ثابت های طبقه، روشهای رسمی D.4.6 [سیستم های عامل] امنیت و محافظت- كنترل جریان اطلاعات، آرگومانهای صحت، روشهای رسمی به K.6.5 [محاسبه میلوكس]، امنیت و محافظت- نرم افزار هجوم كننده، دسترسی غیر مجاز

كلمات كلید، امنیت برنامه كاربردی وب، امنیت در برابر آسیب پذیری ها، امنیت برنامه، بررسی، سیستم های نوع، جریان اطلاعات، عدم اختلال

چکیده انگلیسی‌ :

Security remains a major roadblock to universal acceptance of the Web for many kinds of transactions, especially since the recent, sharp increase in remotely exploitable vulnerabilities has been attributed to Web application bugs. Many verification tools are discovering previously unknown vulnerabilities in legacy C programs, raising hopes that the same success can be achieved with Web applications. In this paper, we describe a sound and holistic approach to ensuring Web application security. Viewing Web application vulnerabilities as a secure information flow problem, we created a lattice-based static analysis algorithm derived from type systems and typestate, and addressed its soundness. During the analysis, sections of code considered vulnerable are instrumented with runtime guards, thus securing Web applications in the absence of user intervention. With sufficient annotations, runtime overhead can be reduced to zero. We also created a tool named WebSSARI (Web application Security by Static Analysis and Runtime Inspection) to test our algorithm, and used it to verify 230 open-source Web application projects on SourceForge.net, which were selected to represent projects of different maturity, popularity, and scale. 69 contained vulnerabilities and their developers were notified. 38 projects acknowledged our findings and stated their plans to provide patches. Our statistics also show that static analysis reduced potential runtime overhead by 98.4%.

Categories and Subject Descriptors :

D.2.4 [Software Engineering]: Software / Program Verification – class invariants, formal methods; D.4.6 [Operating Systems]: Security and Protection – information flow controls, correctness proofs, formal methods; K.6.5 [Computing Milieux]: Security and Protection – invasive software, unauthorized access. General Terms Security, Verification.

Keywords :

Web application security, security vulnerabilities, program security, verification, type systems, information flow, noninterference.